ThickEvaluation.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

inductive OAI.LittleFinitistic.ThickEvaluation.Thick line 13

Source documentation

The actual thick closure: zero, isomorphisms, shifts, extensions, and retracts.

inductive Thick (S : ObjectProperty C) : C → Prop
  | generator {X : C} : S X → Thick S X
  | zero : Thick S 0
  | iso {X Y : C} : (X ≅ Y) → Thick S X → Thick S Y
  | shift {X : C} (n : ℤ) : Thick S X → Thick S (X⟦n⟧)
  | extension (T : Triangle C) : T ∈ distTriang C → Thick S T.obj₁ → Thick S T.obj₃ → Thick S T.obj₂
  | retract {X Y : C} : Retract X Y → Thick S Y → Thick S X

variable (S : ObjectProperty C)

instance OAI.LittleFinitistic.ThickEvaluation.thickRetracts line 23
instance OAI.LittleFinitistic.ThickEvaluation.thickZero line 26
instance OAI.LittleFinitistic.ThickEvaluation.thickShift line 29
instance OAI.LittleFinitistic.ThickEvaluation.thickTriangulated line 32
theorem OAI.LittleFinitistic.ThickEvaluation.thick_minimal line 36
Source documentation
Minimality proves that this is the thick subcategory generated by S.
```
theorem thick_minimal (P : ObjectProperty C) [P.IsTriangulated] [P.IsStableUnderRetracts]
    (h : S ≤ P) : Thick S ≤ P := by
…
```
Mentions: OAI.LittleFinitistic.ThickEvaluation.Thick
theorem OAI.LittleFinitistic.ThickEvaluation.kills_thick line 53
Source documentation
Exact evaluation kills the whole thick closure once it kills the generators.
```
theorem kills_thick (hS : ∀ X, S X → IsZero (F.obj X)) :
    ∀ X, Thick S X → IsZero (F.obj X) := by
…
```
Mentions: OAI.LittleFinitistic.ThickEvaluation.Thick
theorem OAI.LittleFinitistic.ThickEvaluation.inverts_thick line 72
Source documentation
Every morphism whose cone lies in the generated thick subcategory evaluates to an isomorphism.
```
theorem inverts_thick (hS : ∀ X, S X → IsZero (F.obj X)) :
    (ObjectProperty.trW (Thick S)).IsInvertedBy F := by
…
```
Mentions: OAI.LittleFinitistic.ThickEvaluation.Thick
def OAI.LittleFinitistic.ThickEvaluation.quotientEvaluation line 79
Source documentation
Evaluation on the actual localization at cones in the thick closure.
```
def quotientEvaluation (hS : ∀ X, S X → IsZero (F.obj X)) :
    (ObjectProperty.trW (Thick S)).Localization ⥤ D :=
…
```
Mentions: OAI.LittleFinitistic.ThickEvaluation.Thick
def OAI.LittleFinitistic.ThickEvaluation.quotientEvaluationFactors line 83