SieveFiberPresentation.lean`

51 declarations, 0 contain sorry, 0 declared as axioms

Target-fibre colimits in every positive finite dimension

All constructions are internal to the original category of truncated strict categories. No preservation by its inclusion into omega is used.

def OAI.Thomason.Construction.StrictOmegaCategory.FiniteOppositeLabels.object line 23
def OAI.Thomason.Construction.StrictOmegaCategory.FiniteOppositeLabels.functor line 26
def OAI.Thomason.Construction.StrictOmegaCategory.FiniteOppositeLabels.doubleIso line 32
def OAI.Thomason.Construction.StrictOmegaCategory.FiniteOppositeLabels.equivalence line 38
def OAI.Thomason.Construction.StrictOmegaCategory.FiniteOppositeLabels.overFunctor line 51
def OAI.Thomason.Construction.StrictOmegaCategory.FiniteOppositeLabels.overDoubleIso line 60
def OAI.Thomason.Construction.StrictOmegaCategory.FiniteOppositeLabels.overEquivalence line 67
def OAI.Thomason.Construction.StrictOmegaCategory.FiniteOppositeLabels.fiberIso line 85
def OAI.Thomason.Construction.StrictOmegaCategory.FiniteOppositeLabels.fiberNatIso line 93
theorem OAI.Thomason.Construction.StrictOmegaCategory.FiniteOppositeLabels.oneFiber_preservesColimits line 104
Source documentation
Formation of the full target fibre preserves all colimits in the specified positive finite dimension.
```
theorem oneFiber_preservesColimits :
    PreservesColimitsOfSize.{0,0} (finiteLabelFiberFunctor n 1) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.finiteLabelFiberFunctor
theorem OAI.Thomason.Construction.constructedLabelFiberInput line 127
Source documentation
The complete endpoint-fibre interface is supplied by actual adjunctions and explicit opposite equivalences, in all the required dimensions.
```
theorem constructedLabelFiberInput : PublishedLabelFiberInput where
…
```
Mentions: OAI.Thomason.Construction.PublishedLabelFiberInput
def OAI.Thomason.Construction.StrictOmegaCategory.minLabel line 152
Source documentation
Minimum combines membership in two full one fibres.
```
def minLabel (p q : C ⟶ StrictPoset.category (Fin 2)) :
    C ⟶ StrictPoset.category (Fin 2) where
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.StrictOmegaCategory.minLabel_one_iff line 174
theorem OAI.Thomason.Construction.StrictOmegaCategory.minLabel_precomp line 209
theorem OAI.Thomason.Construction.cosieveCharacteristic_inter line 220

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.cosieveMembershipLabel_inter line 244

Source documentation

The minimum label cuts out the actual intersection of upper subsets.

theorem cosieveMembershipLabel_inter {E : Type} [PartialOrder E]
    (A B : Set E) (hA : IsUpperSet A) (hB : IsUpperSet B) :
    minLabel (h.membershipLabel Aᶜ hA.compl) (h.membershipLabel Bᶜ hB.compl) =
      h.membershipLabel (A ∩ B)ᶜ (hA.inter hB).compl := by
…

def OAI.Thomason.Construction.StrictOmegaCategory.InitialCone.overFunctor line 271
def OAI.Thomason.Construction.StrictOmegaCategory.InitialCone.category line 274
def OAI.Thomason.Construction.StrictOmegaCategory.InitialCone.label line 277
def OAI.Thomason.Construction.StrictOmegaCategory.InitialCone.adjunction line 280
def OAI.Thomason.Construction.StrictOmegaCategory.InitialCone.finiteOverFunctor line 284
def OAI.Thomason.Construction.StrictOmegaCategory.InitialCone.finiteCategory line 288
def OAI.Thomason.Construction.StrictOmegaCategory.InitialCone.finiteAdjunction line 291
theorem OAI.Thomason.Construction.StrictOmegaCategory.InitialCone.finite_homEquiv_underlying line 299
Source documentation
The finite adjunction uses the very same strict extension on cells.
```
theorem finite_homEquiv_underlying (n : ℕ) (X : Over (finiteInterval n))
    (D : Truncated.{0} (n+1)) (f : (finiteLabelFiberFunctor n 1).obj X ⟶ D) :
    ((finiteAdjunction n).homEquiv X D f).left =
      (adjunction.homEquiv (Over.mk (show X.left.val ⟶ StrictPoset.category (Fin 2) from X.hom))
        D.val (show labelFiber X.hom 1 ⟶ D.val from f)).left := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.finiteInterval, OAI.Thomason.Construction.StrictOmegaCategory.finiteLabelFiberFunctor, OAI.Thomason.Construction.StrictOmegaCategory.InitialCone.finiteAdjunction, OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.labelFiber
def OAI.Thomason.Construction.FiniteReflectionInput.reflectedOneLabelFiber line 330
Source documentation
The full one fibre, kept inside the positive finite category.
```
def reflectedOneLabelFiber : Truncated (n + 1) :=
…
```
def OAI.Thomason.Construction.FiniteReflectionInput.oneFiberUnit line 335
Source documentation
Restriction of the original reflection unit to its one fibre.
```
def oneFiberUnit : labelFiber p 1 ⟶ (r.reflectedOneLabelFiber q).val :=
…
```

def OAI.Thomason.Construction.FiniteReflectionInput.oneFiberOverEquiv line 339

Source documentation

Reflection descends maps to the initial cone while retaining the label.

noncomputable def oneFiberOverEquiv (D : Truncated (n + 1)) :
    ((Over.mk (show r.reflect.obj X ⟶ finiteInterval n from q)) ⟶
        (InitialCone.finiteOverFunctor n).obj D) ≃
      ((Over.mk p) ⟶ InitialCone.overFunctor.obj D.val) where
…

def OAI.Thomason.Construction.FiniteReflectionInput.oneFiberHomEquiv line 377
Source documentation
The universal bijection of the reflected one fibre.
```
noncomputable def oneFiberHomEquiv (D : Truncated (n + 1)) :
    (r.reflectedOneLabelFiber q ⟶ D) ≃ (labelFiber p 1 ⟶ D.val) :=
…
```

theorem OAI.Thomason.Construction.FiniteReflectionInput.oneFiberHomEquiv_apply line 385

Source documentation

The bijection is actual precomposition with the restricted unit.

theorem oneFiberHomEquiv_apply (D : Truncated (n + 1))
    (f : r.reflectedOneLabelFiber q ⟶ D) :
    r.oneFiberHomEquiv p q hq D f = r.oneFiberUnit p q hq ≫ f := by
…

def OAI.Thomason.Construction.FiniteReflectionInput.reflectedLabelFiber line 428
Source documentation
The full zero fibre, kept inside the positive finite category.
```
def reflectedLabelFiber : Truncated (n + 1) :=
…
```
def OAI.Thomason.Construction.FiniteReflectionInput.zeroFiberUnit line 433
Source documentation
Restriction of the original reflection unit to its zero fibre.
```
def zeroFiberUnit : labelFiber p 0 ⟶ (r.reflectedLabelFiber q).val :=
…
```

def OAI.Thomason.Construction.FiniteReflectionInput.zeroFiberOverEquiv line 437

Source documentation

Reflection descends maps to the terminal cone while retaining the label.

noncomputable def zeroFiberOverEquiv (D : Truncated (n + 1)) :
    ((Over.mk (show r.reflect.obj X ⟶ finiteInterval n from q)) ⟶
        (TerminalCone.finiteOverFunctor n).obj D) ≃
      ((Over.mk p) ⟶ TerminalCone.overFunctor.obj D.val) where
…

def OAI.Thomason.Construction.FiniteReflectionInput.zeroFiberHomEquiv line 475
Source documentation
The universal bijection of the reflected zero fibre.
```
noncomputable def zeroFiberHomEquiv (D : Truncated (n + 1)) :
    (r.reflectedLabelFiber q ⟶ D) ≃ (labelFiber p 0 ⟶ D.val) :=
…
```

theorem OAI.Thomason.Construction.FiniteReflectionInput.zeroFiberHomEquiv_apply line 483

Source documentation

The bijection is actual precomposition with the restricted unit.

theorem zeroFiberHomEquiv_apply (D : Truncated (n + 1))
    (f : r.reflectedLabelFiber q ⟶ D) :
    r.zeroFiberHomEquiv p q hq D f = r.zeroFiberUnit p q hq ≫ f := by
…

theorem OAI.Thomason.Construction.FiniteReflectionInput.zeroFiberUnit_hom_ext line 517
def OAI.Thomason.Construction.FiniteReflectionInput.zeroFiberComparison line 525
Source documentation
The canonical map from the reflected original fibre to the reflected label's fibre.
```
noncomputable def zeroFiberComparison :
    r.reflect.obj (labelFiber p 0) ⟶ r.reflectedLabelFiber q :=
…
```
theorem OAI.Thomason.Construction.FiniteReflectionInput.zeroFiberComparison_fac line 531
Source documentation
Compatibility on every original zero-fibre cell.
```
theorem zeroFiberComparison_fac :
    r.adjunction.unit.app (labelFiber p 0) ≫ r.zeroFiberComparison p q hq =
      r.zeroFiberUnit p q hq :=
…
```
theorem OAI.Thomason.Construction.FiniteReflectionInput.zeroFiberComparison_isIso line 538
Source documentation
The terminal-cone bijection identifies the two reflection universal properties.
```
theorem zeroFiberComparison_isIso : IsIso (r.zeroFiberComparison p q hq) := by
…
```
theorem OAI.Thomason.Construction.FiniteReflectionInput.oneFiberUnit_hom_ext line 587
def OAI.Thomason.Construction.FiniteReflectionInput.oneFiberComparison line 595
Source documentation
The canonical map from the reflected original fibre to the reflected label's fibre.
```
noncomputable def oneFiberComparison :
    r.reflect.obj (labelFiber p 1) ⟶ r.reflectedOneLabelFiber q :=
…
```
theorem OAI.Thomason.Construction.FiniteReflectionInput.oneFiberComparison_fac line 601
Source documentation
Compatibility on every original one-fibre cell.
```
theorem oneFiberComparison_fac :
    r.adjunction.unit.app (labelFiber p 1) ≫ r.oneFiberComparison p q hq =
      r.oneFiberUnit p q hq :=
…
```
theorem OAI.Thomason.Construction.FiniteReflectionInput.oneFiberComparison_isIso line 608
Source documentation
The initial-cone bijection identifies the two reflection universal properties.
```
theorem oneFiberComparison_isIso : IsIso (r.oneFiberComparison p q hq) := by
…
```
def OAI.Thomason.Construction.SieveSimplex.labels line 661
Source documentation
The binary labels of all simplices form a natural transformation.
```
noncomputable def labels :
    (CostructuredArrow.proj SSet.stdSimplex (nerve P) ⋙ h.cosimplicial) ⟶
      (Functor.const _).obj (StrictPoset.category (Fin 2)) where
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
abbrev OAI.Thomason.Construction.SieveSimplex.diagram line 672
Source documentation
The labelled diagram has the original orientals as underlying objects.
```
noncomputable abbrev diagram :
    CostructuredArrow SSet.stdSimplex (nerve P) ⥤ Over (StrictPoset.category (Fin 2)) :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
abbrev OAI.Thomason.Construction.SieveSimplex.cocone line 677
Source documentation
The colimit point is the original categorification with its membership label.
```
noncomputable abbrev cocone : Cocone (diagram A hA h) where
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.diagram
def OAI.Thomason.Construction.SieveSimplex.coconeIsColimit line 687
Source documentation
Forgetting the labels recovers exactly the original simplex colimit.
```
noncomputable def coconeIsColimit : IsColimit (cocone A hA h) := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.cocone
abbrev OAI.Thomason.Construction.SieveSimplex.fiberCocone line 692
Source documentation
Its full zero fibre is therefore the colimit of the full simplex fibres.
```
noncomputable abbrev fiberCocone : Cocone (diagram A hA h ⋙ labelFiberFunctor (Fin 2) 0) :=
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.diagram
def OAI.Thomason.Construction.SieveSimplex.fiberCoconeIsColimit line 696
Source documentation
This uses the proved adjunction, with no published fibre-colimit input.
```
noncomputable def fiberCoconeIsColimit : IsColimit (fiberCocone A hA h) := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.fiberCocone
def OAI.Thomason.Construction.SieveSimplex.backCocone line 701
Source documentation
The clamping inverses form a cocone on the same full simplex fibres.
```
noncomputable def backCocone : Cocone (diagram A hA h ⋙ labelFiberFunctor (Fin 2) 0) where
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.diagram
def OAI.Thomason.Construction.SieveSimplex.inverse line 718
Source documentation
Descending the compatible clamping maps gives the inverse of the sieve map.
```
noncomputable def inverse :
    labelFiber (h.membershipLabel A hA) 0 ⟶ h.categorification.obj (nerve A) :=
…
```
theorem OAI.Thomason.Construction.SieveSimplex.inverse_fac line 723
Source documentation
The descended map restricts to the explicit inverse on every simplex fibre.
```
theorem inverse_fac (s : CostructuredArrow SSet.stdSimplex (nerve P)) :
    (fiberCocone A hA h).ι.app s ≫ inverse A hA h =
      back A hA h (simplexOrder (SSet.yonedaEquiv s.hom)) :=
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.fiberCocone, OAI.Thomason.Construction.SieveSimplex.inverse, OAI.Thomason.Construction.SieveSimplex.back