TerminalConeUniversal.lean`

75 declarations, 0 contain sorry, 0 declared as axioms

Actual full initial faces without atom-generation assumptions

def OAI.Thomason.Construction.SimplexComplex.constructedInitialFaceIso line 20
Source documentation
The explicit initial ordinal face is an isomorphism onto the full subcategory on its vertices, proved directly from positive chain support.
```
noncomputable def constructedInitialFaceIso (h : NormalizedSimplexIdentities)
    {q m : ℕ} (hqm : q ≤ m) :
    h.object q ≅ vertexFullSubcategory h (Set.range (initialFace hqm)) :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.vertexFullSubcategory, OAI.Thomason.Construction.SimplexComplex.initialFace
theorem OAI.Thomason.Construction.SimplexComplex.constructedInitialFaceIso_hom_inclusion line 36
Source documentation
The isomorphism is the original ordinal face on all cells.
```
theorem constructedInitialFaceIso_hom_inclusion (h : NormalizedSimplexIdentities)
    {q m : ℕ} (hqm : q ≤ m) :
    (constructedInitialFaceIso h hqm).hom ≫
      (h.object m).fullInclusion {x | objectIndex h false x ∈ Set.range (initialFace hqm)} =
        h.map (initialFace hqm).toOrderHom := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.constructedInitialFaceIso, OAI.Thomason.Construction.SimplexComplex.objectIndex, OAI.Thomason.Construction.SimplexComplex.initialFace
theorem OAI.Thomason.Construction.SimplexComplex.constructedInitialSegment line 45
Source documentation
Every nonempty lower set of vertices is its actual smaller oriental.
```
theorem constructedInitialSegment (h : NormalizedSimplexIdentities)
    {m : ℕ} {I : Set (Fin (m+1))} (hI : IsLowerSet I) (hne : I.Nonempty) :
    ∃ q : Fin (m+1), Nonempty (h.object q.val ≅ vertexFullSubcategory h I) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.vertexFullSubcategory
theorem OAI.Thomason.Construction.SimplexComplex.constructedZeroFiberOriental line 56
Source documentation
The actual nonempty zero fibre of every binary oriental label is a smaller oriental. No published composition-generation input is used.
```
theorem constructedZeroFiberOriental (h : NormalizedSimplexIdentities)
    {m : ℕ} (b : Fin (m+1) →o Fin 2) (hne : Set.Nonempty {i | b i = 0}) :
    ∃ q : Fin (m+1), Nonempty (h.object q.val ≅ labelFiber (binaryLabel h b) 0) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.binaryLabel
def OAI.Thomason.Construction.NormalizedSimplexIdentities.labelledSimplexDiagram line 84
Source documentation
Lift the oriental presentation along a fixed actual binary label.
```
noncomputable def labelledSimplexDiagram {K : SSet.{0}}
    (p : h.categorification.obj K ⟶ StrictPoset.category (Fin 2)) :
    CostructuredArrow SSet.stdSimplex K ⥤ Over (StrictPoset.category (Fin 2)) :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
def OAI.Thomason.Construction.NormalizedSimplexIdentities.labelledSimplexCocone line 91
Source documentation
The corresponding colimit cocone in the actual slice category.
```
noncomputable def labelledSimplexCocone {K : SSet.{0}}
    (p : h.categorification.obj K ⟶ StrictPoset.category (Fin 2)) :
    Cocone (h.labelledSimplexDiagram p) := Over.liftCocone (h.simplexCocone K) p
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
def OAI.Thomason.Construction.NormalizedSimplexIdentities.labelledSimplexCocone_isColimit line 97
Source documentation
Forgetting labels recovers the original simplex colimit, so the lifted cocone is itself a colimit.
```
noncomputable def labelledSimplexCocone_isColimit {K : SSet.{0}}
    (p : h.categorification.obj K ⟶ StrictPoset.category (Fin 2)) :
    IsColimit (h.labelledSimplexCocone p) :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
def OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexFiberCocone line 103
Source documentation
Take one full endpoint fibre of every labelled oriental piece.
```
noncomputable def simplexFiberCocone {K : SSet.{0}}
    (p : h.categorification.obj K ⟶ StrictPoset.category (Fin 2)) (e : Fin 2) :
    Cocone (h.labelledSimplexDiagram p ⋙ labelFiberFunctor (Fin 2) e) :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
def OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexFiberCocone_isColimit line 109
Source documentation
The actual full fibre is the colimit of the actual full simplex fibres.
```
noncomputable def simplexFiberCocone_isColimit (f : PublishedLabelFiberInput) {K : SSet.{0}}
    (p : h.categorification.obj K ⟶ StrictPoset.category (Fin 2)) (e : Fin 2) :
    IsColimit (h.simplexFiberCocone p e) := by
…
```
Mentions: OAI.Thomason.Construction.PublishedLabelFiberInput, OAI.Thomason.Construction.StrictPoset.category

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.labelledSimplexDiagram_obj_hom line 116

Source documentation

These are the actual labels on the pieces of the lifted presentation.

theorem labelledSimplexDiagram_obj_hom {K : SSet.{0}}
    (p : h.categorification.obj K ⟶ StrictPoset.category (Fin 2))
    (s : CostructuredArrow SSet.stdSimplex K) :
    ((h.labelledSimplexDiagram p).obj s).hom = h.simplexLeg s.hom ≫ p := rfl

Mentions: OAI.Thomason.Construction.StrictPoset.category

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.membership_simplex_label line 122
Source documentation
On a poset simplex the membership label is exactly its monotone binary vertex label.
```
theorem membership_simplex_label {E : Type} [PartialOrder E]
    (A : Set E) (hA : IsLowerSet A) {m : SimplexCategory}
    (s : SSet.stdSimplex.obj m ⟶ nerve E) :
    h.simplexLeg s ≫ h.membershipLabel A hA =
      SimplexComplex.binaryLabel h
        ((sieveCharacteristic A hA).comp (simplexOrder (SSet.yonedaEquiv s))) := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.binaryLabel, OAI.Thomason.Construction.sieveCharacteristic, OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexOrder

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.membership_simplex_fiber_nonempty line 139

Source documentation

Every nonempty zero-fibre of a simplex piece is a smaller oriental.

theorem membership_simplex_fiber_nonempty {E : Type} [PartialOrder E]
    (a : SimplexAtomsInput h) (A : Set E) (hA : IsLowerSet A) {m : SimplexCategory}
    (s : SSet.stdSimplex.obj m ⟶ nerve E)
    (hne : Set.Nonempty {i | simplexOrder (SSet.yonedaEquiv s) i ∈ A}) :
    ∃ q : Fin (m.len + 1), Nonempty (h.object q.val ≅
      labelFiber (h.simplexLeg s ≫ h.membershipLabel A hA) 0) := by
…

Mentions: OAI.Thomason.Construction.SimplexAtomsInput, OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexOrder

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexFiberCocone_pt line 156
Source documentation
The cocone point is exactly the full fibre of the original label.
```
theorem simplexFiberCocone_pt {K : SSet.{0}}
    (p : h.categorification.obj K ⟶ StrictPoset.category (Fin 2)) (e : Fin 2) :
    (h.simplexFiberCocone p e).pt = labelFiber p e := rfl
```
Mentions: OAI.Thomason.Construction.StrictPoset.category

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.membership_simplex_fiber_empty line 161

Source documentation

An empty vertex intersection gives an empty actual simplex fibre.

theorem membership_simplex_fiber_empty {E : Type} [PartialOrder E]
    (A : Set E) (hA : IsLowerSet A) {m : SimplexCategory}
    (s : SSet.stdSimplex.obj m ⟶ nerve E)
    (hne : ¬Set.Nonempty {i | simplexOrder (SSet.yonedaEquiv s) i ∈ A}) :
    IsEmpty (labelFiber (h.simplexLeg s ≫ h.membershipLabel A hA) 0) := by
…

Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexOrder

theorem OAI.Thomason.Construction.realization_delta_one_weak line 194
Source documentation
Both endpoint inclusions into the simplicial interval are weak.
```
theorem realization_delta_one_weak (j : Fin 2) :
    realizationWeakEquivalences (SSet.stdSimplex.δ j : (Δ[0] : SSet.{0}) ⟶ Δ[1]) :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.realization_horn_one_weak line 200
Source documentation
The two one-dimensional horn inclusions satisfy the prescribed actual realization weak-equivalence test.
```
theorem realization_horn_one_weak (i : Fin 2) :
    realizationWeakEquivalences (Λ[1, i].ι : _ ⟶ (Δ[1] : SSet.{0})) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
structure OAI.Thomason.Construction.SieveSimplex.Cut line 232
Source documentation
The zero-labelled vertices of a poset simplex form one initial segment.
```
structure Cut where
…
```
def OAI.Thomason.Construction.SieveSimplex.cut line 237
Source documentation
Construct the last vertex of the nonempty initial segment.
```
noncomputable def cut (hne : ∃ i, s i ∈ A) : Cut A s := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.Cut
instance OAI.Thomason.Construction.SieveSimplex.(instance at line 245) line 245
def OAI.Thomason.Construction.SieveSimplex.Cut.clamp line 256
Source documentation
Clamp all later vertices to the last sieve vertex.
```
def Cut.clamp (c : Cut A s) : Fin (m+1) →o A where
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.Cut
theorem OAI.Thomason.Construction.SieveSimplex.Cut.clamp_of_mem line 260

theorem OAI.Thomason.Construction.SieveSimplex.Cut.clamp_naturality line 266

Source documentation

Different cut choices, or precomposed simplices, agree on all sieve vertices.

theorem Cut.clamp_naturality {k : ℕ} {t : Fin (k+1) →o P}
    (c : Cut A s) (d : Cut A t) (u : Fin (m+1) →o Fin (k+1))
    (hu : ∀ i, t (u i) = s i) (i : Fin (m+1)) (hi : s i ∈ A) :
    c.clamp i = d.clamp (u i) := by
…

Mentions: OAI.Thomason.Construction.SieveSimplex.Cut

def OAI.Thomason.Construction.SieveSimplex.label line 274
Source documentation
The binary strict label carried by this actual oriental.
```
noncomputable def label (A : Set P) (hA : IsLowerSet A) {m : ℕ}
    (s : Fin (m+1) →o P) (h : NormalizedSimplexIdentities) :
    h.object m ⟶ StrictPoset.category (Fin 2) :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.SieveSimplex.Cut.fiber_in_initial_face line 280
Source documentation
Every cell of the zero fibre is in the actual initial face determined by the cut.
```
theorem Cut.fiber_in_initial_face (h : NormalizedSimplexIdentities) (c : Cut A s)
    (x : labelFiber (label A hA s h) 0) :
    x.val ∈ Set.range
      (h.map (SimplexComplex.initialFace (Nat.le_of_lt_succ c.last.isLt)).toOrderHom).toFun := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SieveSimplex.Cut, OAI.Thomason.Construction.SieveSimplex.label, OAI.Thomason.Construction.SimplexComplex.initialFace
abbrev OAI.Thomason.Construction.cosieveCharacteristic line 305
theorem OAI.Thomason.Construction.cosieveCharacteristic_one_iff line 308
structure OAI.Thomason.Construction.CosieveSimplex.Cut line 318
def OAI.Thomason.Construction.CosieveSimplex.cut line 322
instance OAI.Thomason.Construction.CosieveSimplex.(instance at line 330) line 330
def OAI.Thomason.Construction.CosieveSimplex.Cut.clamp line 340
theorem OAI.Thomason.Construction.CosieveSimplex.Cut.clamp_of_mem line 344
theorem OAI.Thomason.Construction.CosieveSimplex.Cut.clamp_naturality line 349
abbrev OAI.Thomason.Construction.CosieveSimplex.label line 356
theorem OAI.Thomason.Construction.CosieveSimplex.Cut.fiber_in_final_face line 361

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetLeg_eq_on_initial line 393

Source documentation

Agreement on an initial set of vertices gives agreement on every cell of that full initial face.

theorem posetLeg_eq_on_initial {E : Type} [PartialOrder E] {m q : ℕ}
    (hqm : q ≤ m) (s t : Fin (m+1) →o E)
    (hst : ∀ i, i.val ≤ q → s i = t i) (x : h.object m)
    (hx : x ∈ Set.range (h.map (SimplexComplex.initialFace hqm).toOrderHom).toFun) :
    (h.posetLeg s).toFun x = (h.posetLeg t).toFun x := by
…

Mentions: OAI.Thomason.Construction.SimplexComplex.initialFace

theorem OAI.Thomason.Construction.SieveSimplex.label_precomp line 419
Source documentation
Pulling an oriental label back along an ordinal operator pulls back its vertex list.
```
theorem label_precomp {l m : ℕ} (t : Fin (m+1) →o P)
    (u : Fin (l+1) →o Fin (m+1)) :
    h.map u ≫ label A hA t h = label A hA (t.comp u) h := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.label
def OAI.Thomason.Construction.SieveSimplex.Cut.back line 429
Source documentation
The inverse on the zero-labelled piece uses the clamped simplex in A.
```
noncomputable def Cut.back {m : ℕ} {s : Fin (m+1) →o P} (c : Cut A s) :
    labelFiber (label A hA s h) 0 ⟶ h.categorification.obj (nerve A) :=
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.Cut, OAI.Thomason.Construction.SieveSimplex.label
theorem OAI.Thomason.Construction.SieveSimplex.Cut.back_inclusion line 434
Source documentation
After the original sieve inclusion, the inverse is the original presentation leg.
```
theorem Cut.back_inclusion {m : ℕ} {s : Fin (m+1) →o P} (c : Cut A s) :
    c.back hA h ≫ h.posetMap (subposetInclusion A) =
      labelFiberInclusion (label A hA s h) 0 ≫ h.posetLeg s := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.Cut, OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.SieveSimplex.label
theorem OAI.Thomason.Construction.SieveSimplex.Cut.back_naturality line 450
Source documentation
The inverse maps commute with every face and degeneracy operator.
```
theorem Cut.back_naturality {l m : ℕ} (t : Fin (m+1) →o P)
    (u : Fin (l+1) →o Fin (m+1)) (c : Cut A (t.comp u)) (d : Cut A t) :
    labelFiberMap (label A hA (t.comp u) h) (label A hA t h) 0 (h.map u)
      (label_precomp hA h t u) ≫ d.back hA h = c.back hA h := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.Cut, OAI.Thomason.Construction.SieveSimplex.label, OAI.Thomason.Construction.SieveSimplex.label_precomp
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetLeg_eq_on_final line 483
theorem OAI.Thomason.Construction.CosieveSimplex.label_precomp line 508
def OAI.Thomason.Construction.CosieveSimplex.Cut.back line 513
theorem OAI.Thomason.Construction.CosieveSimplex.Cut.back_inclusion line 517
theorem OAI.Thomason.Construction.CosieveSimplex.Cut.back_naturality line 532
theorem OAI.Thomason.Construction.CosieveSimplex.emptyFiber line 568
Source documentation
A simplex without a cosieve vertex has an empty full one fibre.
```
theorem emptyFiber {m : ℕ} (s : Fin (m+1) →o P) (hs : ¬∃ i, s i ∈ A) :
    IsEmpty (labelFiber (label A hA s h) 1) := by
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.label
def OAI.Thomason.Construction.CosieveSimplex.emptyBack line 576
Source documentation
Empty fibres have the unique map into the categorified cosieve.
```
noncomputable def emptyBack {m : ℕ} (s : Fin (m+1) →o P) (hs : ¬∃ i, s i ∈ A) :
    labelFiber (label A hA s h) 1 ⟶ h.categorification.obj (nerve A) := by
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.label
def OAI.Thomason.Construction.CosieveSimplex.back line 585
Source documentation
The inverse is defined on every simplex, including the empty-suffix case.
```
noncomputable def back {m : ℕ} (s : Fin (m+1) →o P) :
    labelFiber (label A hA s h) 1 ⟶ h.categorification.obj (nerve A) := by
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.label
theorem OAI.Thomason.Construction.CosieveSimplex.back_eq_cut line 591
Source documentation
On a nonempty suffix the inverse is independent of its chosen cut.
```
theorem back_eq_cut {m : ℕ} (s : Fin (m+1) →o P) (c : Cut A s) :
    back A hA h s = c.back hA h := by
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.Cut, OAI.Thomason.Construction.CosieveSimplex.back
theorem OAI.Thomason.Construction.CosieveSimplex.back_inclusion line 597
Source documentation
The inverse is compatible with the original cosieve inclusion.
```
theorem back_inclusion {m : ℕ} (s : Fin (m+1) →o P) :
    back A hA h s ≫ h.posetMap (subposetInclusion A) =
      labelFiberInclusion (label A hA s h) 1 ≫ h.posetLeg s := by
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.back, OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.CosieveSimplex.label
theorem OAI.Thomason.Construction.CosieveSimplex.back_naturality line 610
Source documentation
All inverse maps commute with all ordinal operators.
```
theorem back_naturality {l m : ℕ} (t : Fin (m+1) →o P)
    (u : Fin (l+1) →o Fin (m+1)) :
    labelFiberMap (label A hA (t.comp u) h) (label A hA t h) 1 (h.map u)
      (label_precomp hA h t u) ≫ back A hA h t = back A hA h (t.comp u) := by
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.label, OAI.Thomason.Construction.CosieveSimplex.label_precomp, OAI.Thomason.Construction.CosieveSimplex.back
theorem OAI.Thomason.Construction.CosieveSimplex.back_apply_congr line 626
Source documentation
Equal vertex maps give equal inverse values on the same underlying cell.
```
theorem back_apply_congr {m : ℕ} {s t : Fin (m+1) →o P} (he : s = t)
    (x : labelFiber (label A hA s h) 1) (y : labelFiber (label A hA t h) 1)
    (hxy : x.val = y.val) :
    (back A hA h s).toFun x = (back A hA h t).toFun y := by
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.label, OAI.Thomason.Construction.CosieveSimplex.back
theorem OAI.Thomason.Construction.SieveSimplex.emptyFiber line 650
Source documentation
A simplex without a sieve vertex has an empty full zero fibre.
```
theorem emptyFiber {m : ℕ} (s : Fin (m+1) →o P) (hs : ¬∃ i, s i ∈ A) :
    IsEmpty (labelFiber (label A hA s h) 0) := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.label
def OAI.Thomason.Construction.SieveSimplex.emptyBack line 658
Source documentation
Empty fibres have the unique map into the categorified sieve.
```
noncomputable def emptyBack {m : ℕ} (s : Fin (m+1) →o P) (hs : ¬∃ i, s i ∈ A) :
    labelFiber (label A hA s h) 0 ⟶ h.categorification.obj (nerve A) := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.label
def OAI.Thomason.Construction.SieveSimplex.back line 667
Source documentation
The inverse is defined on every simplex, including the empty-prefix case.
```
noncomputable def back {m : ℕ} (s : Fin (m+1) →o P) :
    labelFiber (label A hA s h) 0 ⟶ h.categorification.obj (nerve A) := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.label
theorem OAI.Thomason.Construction.SieveSimplex.back_eq_cut line 673
Source documentation
On a nonempty prefix the inverse is independent of its chosen cut.
```
theorem back_eq_cut {m : ℕ} (s : Fin (m+1) →o P) (c : Cut A s) :
    back A hA h s = c.back hA h := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.Cut, OAI.Thomason.Construction.SieveSimplex.back
theorem OAI.Thomason.Construction.SieveSimplex.back_inclusion line 679
Source documentation
The inverse is compatible with the original sieve inclusion.
```
theorem back_inclusion {m : ℕ} (s : Fin (m+1) →o P) :
    back A hA h s ≫ h.posetMap (subposetInclusion A) =
      labelFiberInclusion (label A hA s h) 0 ≫ h.posetLeg s := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.back, OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.SieveSimplex.label
theorem OAI.Thomason.Construction.SieveSimplex.back_naturality line 692
Source documentation
All inverse maps commute with all ordinal operators.
```
theorem back_naturality {l m : ℕ} (t : Fin (m+1) →o P)
    (u : Fin (l+1) →o Fin (m+1)) :
    labelFiberMap (label A hA (t.comp u) h) (label A hA t h) 0 (h.map u)
      (label_precomp hA h t u) ≫ back A hA h t = back A hA h (t.comp u) := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.label, OAI.Thomason.Construction.SieveSimplex.label_precomp, OAI.Thomason.Construction.SieveSimplex.back
theorem OAI.Thomason.Construction.SieveSimplex.back_apply_congr line 708
Source documentation
Equal vertex maps give equal inverse values on the same underlying cell.
```
theorem back_apply_congr {m : ℕ} {s t : Fin (m+1) →o P} (he : s = t)
    (x : labelFiber (label A hA s h) 0) (y : labelFiber (label A hA t h) 0)
    (hxy : x.val = y.val) :
    (back A hA h s).toFun x = (back A hA h t).toFun y := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.label, OAI.Thomason.Construction.SieveSimplex.back
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.extendCell line 730
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.extendCell_zero line 735
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.extendCell_cross line 739
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.extendCell_one line 743
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.zeroCell_face line 747
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.zeroSource_face_succ line 752
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.extendCell_face line 759
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.zeroCell_comp line 807
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.zeroSource_comp line 813
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.map_zeroSource line 822
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.extendCell_comp line 826
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.extend line 899
Source documentation
The strict extension of a functor from the actual zero fibre.
```
def extend : X ⟶ category C where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.category
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.extend_label line 919
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.restrict line 943
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.old_restrict line 947
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.restrict_extend line 954
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.extend_restrict line 964