TwoConeVerdier.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.LittleFinitistic.TwoConeVerdier.ConePair line 14

Source documentation

Two specified cone triangles, with the first maps the denominators to invert.

structure ConePair (C : Type*) [Category* C] [HasShift C ℤ] [Preadditive C]
    [HasZeroObject C] [∀ n : ℤ, (shiftFunctor C n).Additive] [Pretriangulated C] where
…

def OAI.LittleFinitistic.TwoConeVerdier.ConePair.generators line 25
Source documentation
Only the two cone objects are generators.
```
def generators : ObjectProperty C := fun X => X = T.first.obj₃ ∨ X = T.second.obj₃
```
instance OAI.LittleFinitistic.TwoConeVerdier.ConePair.(instance at line 26) line 26
abbrev OAI.LittleFinitistic.TwoConeVerdier.ConePair.S line 29
Source documentation
The least thick subcategory containing these two cones.
```
abbrev S : ObjectProperty C := T.generators.triangEnvelope
```
abbrev OAI.LittleFinitistic.TwoConeVerdier.ConePair.Sigma line 32
Source documentation
Exactly the maps whose cone lies in S.
```
abbrev Sigma : MorphismProperty C := T.S.trW
```
abbrev OAI.LittleFinitistic.TwoConeVerdier.ConePair.Q line 35
Source documentation
The Verdier localization at the cone class.
```
abbrev Q := T.Sigma.Localization
```
abbrev OAI.LittleFinitistic.TwoConeVerdier.ConePair.q line 36
theorem OAI.LittleFinitistic.TwoConeVerdier.ConePair.rightFractions line 39
Source documentation
This is a proved fraction calculus, inherited from the triangle axioms.
```
theorem rightFractions [IsTriangulated C] : T.Sigma.HasRightCalculusOfFractions := inferInstance
```
theorem OAI.LittleFinitistic.TwoConeVerdier.ConePair.quotient_triangulated line 41
theorem OAI.LittleFinitistic.TwoConeVerdier.ConePair.source_localization line 43
theorem OAI.LittleFinitistic.TwoConeVerdier.ConePair.first_cone_mem line 45
theorem OAI.LittleFinitistic.TwoConeVerdier.ConePair.second_cone_mem line 46
theorem OAI.LittleFinitistic.TwoConeVerdier.ConePair.first_mem line 48
theorem OAI.LittleFinitistic.TwoConeVerdier.ConePair.second_mem line 51
instance OAI.LittleFinitistic.TwoConeVerdier.ConePair.(instance at line 54) line 54
instance OAI.LittleFinitistic.TwoConeVerdier.ConePair.(instance at line 55) line 55
theorem OAI.LittleFinitistic.TwoConeVerdier.ConePair.sigma_iff line 58
Source documentation
The cone criterion agrees with any distinguished cone triangle.
```
theorem sigma_iff (U : Triangle C) (hU : U ∈ distTriang C) :
    T.Sigma U.mor₁ ↔ T.S U.obj₃ := T.S.trW_iff_of_distinguished U hU
```

theorem OAI.LittleFinitistic.TwoConeVerdier.ConePair.thick_minimal line 62

Source documentation

Exact minimality, including closure under retracts.

theorem thick_minimal (P : ObjectProperty C) [P.IsTriangulated] [P.IsStableUnderRetracts]
    (h₁ : P T.first.obj₃) (h₂ : P T.second.obj₃) : T.S ≤ P := by
…

theorem OAI.LittleFinitistic.TwoConeVerdier.ConePair.roof line 70

Source documentation

Every morphism is a roof with a source denominator.

theorem roof [IsTriangulated C] {X Y : C} (f : T.q.obj X ⟶ T.q.obj Y) :
    ∃ (r : T.Sigma.RightFraction X Y), f = r.map T.q (Localization.inverts _ _) :=
…

theorem OAI.LittleFinitistic.TwoConeVerdier.ConePair.zero_fraction line 75
Source documentation
The manuscript's zero-fraction rule, with a genuine denominator.
```
theorem zero_fraction [IsTriangulated C] {X Y : C} (f : X ⟶ Y) (hf : T.q.map f = 0) :
    ∃ (Z : C) (v : Z ⟶ X), T.Sigma v ∧ v ≫ f = 0 := by
…
```
instance OAI.LittleFinitistic.TwoConeVerdier.ConePair.zeroRetracts line 84
instance OAI.LittleFinitistic.TwoConeVerdier.ConePair.zeroShift line 88
instance OAI.LittleFinitistic.TwoConeVerdier.ConePair.zeroTriangulated line 91
instance OAI.LittleFinitistic.TwoConeVerdier.ConePair.kernelRetracts line 97
theorem OAI.LittleFinitistic.TwoConeVerdier.ConePair.evaluation_kills line 102
Source documentation
An exact functor inverting the two displayed arrows kills both required generating cones, hence their entire thick closure.
```
theorem evaluation_kills : T.S ≤ F.kernel := by
…
```
theorem OAI.LittleFinitistic.TwoConeVerdier.ConePair.evaluation_inverts line 111
def OAI.LittleFinitistic.TwoConeVerdier.ConePair.evaluation line 118
Source documentation
The induced functor from the actual quotient.
```
def evaluation : T.Q ⥤ D := Localization.lift F (T.evaluation_inverts F) T.q
```
def OAI.LittleFinitistic.TwoConeVerdier.ConePair.evaluation_fac line 120