Real phase shifts of owner slicings

Real phase translation sends the slice at ψ to the old slice at ψ + t. This module owns the construction and identifies all four phase-cut predicates after translation.

def CategoryTheory.Triangulated.HNFiltration.phaseShift (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {s : Slicing C} {E : C} (F : HNFiltration C s.P E) (t : ℝ) : HNFiltration C (fun (ψ : ℝ) => s.P (ψ + t)) E

Translate the phases of an owner HN filtration by a real amount.

Equations

• CategoryTheory.Triangulated.HNFiltration.phaseShift C F t = { toPostnikovTower := F.toPostnikovTower, φ := fun (i : Fin F.n) => F.φ i - t, hφ := ⋯, semistable := ⋯ }

def CategoryTheory.Triangulated.Slicing.phaseShift (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (t : ℝ) : Slicing C

Phase-shifted owner slicing: (s.phaseShift t).P ψ = s.P (ψ + t).

Equations

• CategoryTheory.Triangulated.Slicing.phaseShift C s t = { P := fun (ψ : ℝ) => s.P (ψ + t), closedUnderIso := ⋯, zero_mem := ⋯, shift_iff := ⋯, hom_vanishing := ⋯, hn_exists := ⋯ }

theorem CategoryTheory.Triangulated.Slicing.phaseShift_gtProp_zero (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (t : ℝ) (E : C) : gtProp C (phaseShift C s t) 0 E ↔ gtProp C s t E

The strict lower cut at zero of a shifted slicing is the old cut at the translation parameter.

theorem CategoryTheory.Triangulated.Slicing.phaseShift_gtProp (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (t u : ℝ) (E : C) : gtProp C (phaseShift C s t) u E ↔ gtProp C s (u + t) E

A strict lower cut of a shifted slicing is the old cut translated by the same amount.

theorem CategoryTheory.Triangulated.Slicing.phaseShift_leProp_zero (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (t : ℝ) (E : C) : leProp C (phaseShift C s t) 0 E ↔ leProp C s t E

The weak upper cut at zero of a shifted slicing is the old cut at the translation parameter.

theorem CategoryTheory.Triangulated.Slicing.phaseShift_leProp (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (t u : ℝ) (E : C) : leProp C (phaseShift C s t) u E ↔ leProp C s (u + t) E

A weak upper cut of a shifted slicing is the old cut translated by the same amount.

theorem CategoryTheory.Triangulated.Slicing.phaseShift_ltProp_zero (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (t : ℝ) (E : C) : ltProp C (phaseShift C s t) 0 E ↔ ltProp C s t E

The strict upper cut at zero of a shifted slicing is the old cut at the translation parameter.

theorem CategoryTheory.Triangulated.Slicing.phaseShift_ltProp (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (t u : ℝ) (E : C) : ltProp C (phaseShift C s t) u E ↔ ltProp C s (u + t) E

A strict upper cut of a shifted slicing is the old cut translated by the same amount.

theorem CategoryTheory.Triangulated.Slicing.phaseShift_geProp_zero (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (t : ℝ) (E : C) : geProp C (phaseShift C s t) 0 E ↔ geProp C s t E

The weak lower cut at zero of a shifted slicing is the old cut at the translation parameter.

theorem CategoryTheory.Triangulated.Slicing.phaseShift_geProp (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (t u : ℝ) (E : C) : geProp C (phaseShift C s t) u E ↔ geProp C s (u + t) E

A weak lower cut of a shifted slicing is the old cut translated by the same amount.