Phase bounds attached to an owner slicing

This module defines the four phase-cut object properties used to construct the t-structure associated to a slicing. The definitions are intrinsic to the repository-owned HN filtration API and have no retained-library dependency.

def CategoryTheory.Triangulated.HNFiltration.phiPlus (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ℝ → ObjectProperty C} {E : C} (F : HNFiltration C P E) (h : 0 < F.n) : ℝ

The highest phase in a nonempty HN filtration.

Equations

• CategoryTheory.Triangulated.HNFiltration.phiPlus C F h = F.φ ⟨0, h⟩

def CategoryTheory.Triangulated.HNFiltration.phiMinus (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ℝ → ObjectProperty C} {E : C} (F : HNFiltration C P E) (h : 0 < F.n) : ℝ

The lowest phase in a nonempty HN filtration.

Equations

• CategoryTheory.Triangulated.HNFiltration.phiMinus C F h = F.φ ⟨F.n - 1, ⋯⟩

theorem CategoryTheory.Triangulated.HNFiltration.phase_mem_range (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ℝ → ObjectProperty C} {E : C} (F : HNFiltration C P E) (h : 0 < F.n) (i : Fin F.n) : phiMinus C F h ≤ F.φ i ∧ F.φ i ≤ phiPlus C F h

Every phase lies between the extremal phases.

theorem CategoryTheory.Triangulated.HNFiltration.phiMinus_le_phiPlus (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ℝ → ObjectProperty C} {E : C} (F : HNFiltration C P E) (h : 0 < F.n) : phiMinus C F h ≤ phiPlus C F h

The lowest phase is no greater than the highest phase.

def CategoryTheory.Triangulated.HNFiltration.ofIso (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ℝ → ObjectProperty C} {E E' : C} (F : HNFiltration C P E) (e : E ≅ E') : HNFiltration C P E'

Transport an owner HN filtration across an isomorphism of its target.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Triangulated.Slicing.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 : ℝ) : ObjectProperty C

Objects all of whose HN phases are at most t.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Triangulated.Slicing.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 : ℝ) : ObjectProperty C

Objects all of whose HN phases are strictly greater than t.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Triangulated.Slicing.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 : ℝ) : ObjectProperty C

Objects all of whose HN phases are strictly less than t.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Triangulated.Slicing.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 : ℝ) : ObjectProperty C

Objects all of whose HN phases are at least t.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Triangulated.Slicing.leProp_isClosedUnderIsomorphisms (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 : ℝ) : (leProp C s t).IsClosedUnderIsomorphisms

instance CategoryTheory.Triangulated.Slicing.gtProp_isClosedUnderIsomorphisms (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 : ℝ) : (gtProp C s t).IsClosedUnderIsomorphisms

instance CategoryTheory.Triangulated.Slicing.ltProp_isClosedUnderIsomorphisms (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 : ℝ) : (ltProp C s t).IsClosedUnderIsomorphisms

instance CategoryTheory.Triangulated.Slicing.geProp_isClosedUnderIsomorphisms (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 : ℝ) : (geProp C s t).IsClosedUnderIsomorphisms

theorem CategoryTheory.Triangulated.Slicing.leProp_of_isZero (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} (hE : Limits.IsZero E) (t : ℝ) : leProp C s t E

theorem CategoryTheory.Triangulated.Slicing.gtProp_of_isZero (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} (hE : Limits.IsZero E) (t : ℝ) : gtProp C s t E

theorem CategoryTheory.Triangulated.Slicing.ltProp_of_isZero (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} (hE : Limits.IsZero E) (t : ℝ) : ltProp C s t E

theorem CategoryTheory.Triangulated.Slicing.geProp_of_isZero (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} (hE : Limits.IsZero E) (t : ℝ) : geProp C s t E

theorem CategoryTheory.Triangulated.Slicing.leProp_mono (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₁ t₂ : ℝ} (h : t₁ ≤ t₂) : leProp C s t₁ ≤ leProp C s t₂

Upper phase cuts are monotone in their endpoint.

theorem CategoryTheory.Triangulated.Slicing.gtProp_anti (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₁ t₂ : ℝ} (h : t₁ ≤ t₂) : gtProp C s t₂ ≤ gtProp C s t₁

Strict lower phase cuts are antitone in their endpoint.

theorem CategoryTheory.Triangulated.Slicing.ltProp_mono (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₁ t₂ : ℝ} (h : t₁ ≤ t₂) : ltProp C s t₁ ≤ ltProp C s t₂

Strict upper phase cuts are monotone in their endpoint.

theorem CategoryTheory.Triangulated.Slicing.geProp_anti (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₁ t₂ : ℝ} (h : t₁ ≤ t₂) : geProp C s t₂ ≤ geProp C s t₁

Lower phase cuts are antitone in their endpoint.

theorem CategoryTheory.Triangulated.Slicing.leProp_of_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 : ℝ} : ltProp C s t ≤ leProp C s t

theorem CategoryTheory.Triangulated.Slicing.geProp_of_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 : ℝ} : gtProp C s t ≤ geProp C s t

theorem CategoryTheory.Triangulated.Slicing.ltProp_of_intervalProp (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {a b : ℝ} {E : C} (hE : intervalProp C s a b E) : ltProp C s b E

Membership in an open phase interval implies the corresponding strict upper bound.

theorem CategoryTheory.Triangulated.Slicing.gtProp_of_intervalProp (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {a b : ℝ} {E : C} (hE : intervalProp C s a b E) : gtProp C s a E

Membership in an open phase interval implies the corresponding strict lower bound.

Hom-vanishing across phase cuts

theorem CategoryTheory.Triangulated.Slicing.hom_eq_zero_of_phase_gap (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {X Y : C} (FX : HNFiltration C s.P X) (FY : HNFiltration C s.P Y) (hgap : ∀ (i : Fin FX.n) (j : Fin FY.n), FY.φ j < FX.φ i) (f : X ⟶ Y) : f = 0

Morphisms between HN-filtered objects separated by a strict phase gap vanish.

theorem CategoryTheory.Triangulated.Slicing.intervalHom_eq_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) {A B : C} {a₁ b₁ a₂ b₂ : ℝ} (hA : intervalProp C s a₁ b₁ A) (hB : intervalProp C s a₂ b₂ B) (hgap : b₂ ≤ a₁) (f : A ⟶ B) : f = 0

Morphisms from an open interval strictly above another open interval vanish.

theorem CategoryTheory.Triangulated.Slicing.zero_of_gtProp_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) {X Y : C} (hX : gtProp C s 0 X) (hY : leProp C s 0 Y) (f : X ⟶ Y) : f = 0

The hom-vanishing statement for the (> 0, ≤ 0) phase cut.

theorem CategoryTheory.Triangulated.Slicing.zero_of_geProp_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) {X Y : C} (hX : geProp C s 0 X) (hY : ltProp C s 0 Y) (f : X ⟶ Y) : f = 0

The hom-vanishing statement for the (≥ 0, < 0) phase cut.

theorem CategoryTheory.Triangulated.Slicing.zero_of_geProp_ltProp_at (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 : ℝ) {X Y : C} (hX : geProp C s t X) (hY : ltProp C s t Y) (f : X ⟶ Y) : f = 0

The hom-vanishing statement for an arbitrary (≥ t, < t) phase cut.