PosetSieveNaturality.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The canonical categorified sieve is its actual full zero fibre

The inverse is descended from clamped simplex maps. Both inverse identities follow from the actual simplex colimits, with empty pieces included.

theorem OAI.Thomason.Construction.SieveSimplex.inverse_inclusion line 25
Source documentation
Forgetting the descended inverse recovers the original fibre inclusion.
```
theorem inverse_inclusion :
    inverse A hA h ≫ h.posetMap (subposetInclusion A) =
      labelFiberInclusion (h.membershipLabel A hA) 0 := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.inverse, OAI.Thomason.Construction.subposetInclusion
theorem OAI.Thomason.Construction.SieveSimplex.inverse_posetFiberMap line 41
Source documentation
The descended inverse is a right inverse of the canonical sieve map.
```
theorem inverse_posetFiberMap :
    inverse A hA h ≫ h.posetFiberMap A hA = 𝟙 _ := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.inverse
theorem OAI.Thomason.Construction.SieveSimplex.whole_fiberLeg line 47
Source documentation
The whole sieve simplex maps to the original colimit leg after forgetting.
```
theorem whole_fiberLeg {m : ℕ} (s : Fin (m+1) →o A) :
    whole A hA h s ≫ (fiberCocone A hA h).ι.app
        (CostructuredArrow.mk (SSet.yonedaEquiv.symm
          (orderSimplex ((subposetInclusion A).comp s)))) =
      h.posetLeg s ≫ h.posetFiberMap A hA := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.whole, OAI.Thomason.Construction.SieveSimplex.fiberCocone, OAI.Thomason.Construction.subposetInclusion
theorem OAI.Thomason.Construction.SieveSimplex.posetFiberMap_inverse_on_leg line 57
Source documentation
The inverse identity on an arbitrary simplex of the original sieve.
```
theorem posetFiberMap_inverse_on_leg {m : ℕ} (s : Fin (m+1) →o A) :
    h.posetLeg s ≫ (h.posetFiberMap A hA ≫ inverse A hA h) = h.posetLeg s := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.inverse
theorem OAI.Thomason.Construction.SieveSimplex.posetFiberMap_inverse line 82
Source documentation
The descended inverse is also a left inverse, on the original sieve colimit.
```
theorem posetFiberMap_inverse :
    h.posetFiberMap A hA ≫ inverse A hA h = 𝟙 _ := by
…
```
Mentions: OAI.Thomason.Construction.SieveSimplex.inverse
def OAI.Thomason.Construction.NormalizedSimplexIdentities.posetSieveIso line 100
Source documentation
A poset sieve categorifies to exactly the full zero fibre of membership.
```
noncomputable def posetSieveIso (h : NormalizedSimplexIdentities) [StrictColimitsInput]
    {P : Type} [PartialOrder P] (A : Set P) (hA : IsLowerSet A) :
    h.categorification.obj (nerve A) ≅ labelFiber (h.membershipLabel A hA) 0 where
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictColimitsInput
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.constructedOmegaPosetSieveInput line 109
Source documentation
The simplex construction gives the full-sieve comparison in omega dimension.
```
theorem constructedOmegaPosetSieveInput (h : NormalizedSimplexIdentities)
    [StrictColimitsInput] : PublishedOmegaPosetSieveInput h where
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictColimitsInput, OAI.Thomason.Construction.PublishedOmegaPosetSieveInput

theorem OAI.Thomason.Construction.FiniteReflectionInput.oneFiberComparison_inclusion line 129

Source documentation

The one-fibre comparison commutes with the original full inclusion.

theorem oneFiberComparison_inclusion {X : StrictOmegaCategory.{0}}
    (p : X ⟶ StrictPoset.category (Fin 2))
    (q : (r.reflect.obj X).val ⟶ StrictPoset.category (Fin 2))
    (hq : r.adjunction.unit.app X ≫ q = p) :
    r.oneFiberComparison p q hq ≫
      (show r.reflectedOneLabelFiber q ⟶ r.reflect.obj X from labelFiberInclusion q 1) =
      r.reflect.map (labelFiberInclusion p 1) := by
…

Mentions: OAI.Thomason.Construction.StrictPoset.category

def OAI.Thomason.Construction.FiniteReflectionInput.posetCosieveIso line 159

Source documentation

A finite cosieve is its actual full one fibre, not merely an equivalent replacement category.

noncomputable def posetCosieveIso {P : Type} [PartialOrder P]
    (A : Set P) (hA : IsUpperSet A) :
    (r.categorification h).obj (nerve A) ≅
      r.reflectedOneLabelFiber (r.membershipLabel h Aᶜ hA.compl) := by
…

theorem OAI.Thomason.Construction.FiniteReflectionInput.posetCosieveIso_inclusion line 170

Source documentation

The isomorphism factors the literal reflected poset inclusion.

theorem posetCosieveIso_inclusion {P : Type} [PartialOrder P]
    (A : Set P) (hA : IsUpperSet A) :
    (r.posetCosieveIso h A hA).hom ≫
      (show r.reflectedOneLabelFiber (r.membershipLabel h Aᶜ hA.compl) ⟶
        (r.categorification h).obj (nerve P) from
          labelFiberInclusion (r.membershipLabel h Aᶜ hA.compl) 1) =
      r.reflect.map (h.posetMap (subposetInclusion A)) := by
…

Mentions: OAI.Thomason.Construction.subposetInclusion

def OAI.Thomason.Construction.SieveMap.restriction line 219
Source documentation
The ordinary restriction to the two sieves.
```
def restriction : A →o B where
…
```
theorem OAI.Thomason.Construction.SieveMap.restriction_inclusion line 224
Source documentation
Restriction commutes with the original full-subposet inclusions.
```
theorem restriction_inclusion :
    (subposetInclusion B).comp (restriction A B f hf) = f.comp (subposetInclusion A) := rfl
…
```
Mentions: OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.SieveMap.restriction
theorem OAI.Thomason.Construction.SieveMap.characteristic line 230
Source documentation
Pullback equality of sieves is exactly equality of binary characteristic labels.
```
theorem characteristic (hA : IsLowerSet A) (hB : IsLowerSet B) :
    (sieveCharacteristic B hB).comp f = sieveCharacteristic A hA := by
…
```
Mentions: OAI.Thomason.Construction.sieveCharacteristic
theorem OAI.Thomason.Construction.SieveMap.membership line 242
Source documentation
The actual categorified map respects the original membership labels.
```
theorem membership :
    h.posetMap f ≫ h.membershipLabel B hB = h.membershipLabel A hA := by
…
```
def OAI.Thomason.Construction.SieveMap.fiberMap line 258
Source documentation
The full-fibre map is the restriction of the original strict functor.
```
noncomputable def fiberMap :
    labelFiber (h.membershipLabel A hA) 0 ⟶ labelFiber (h.membershipLabel B hB) 0 :=
…
```
theorem OAI.Thomason.Construction.SieveMap.naturality line 263
Source documentation
The constructed sieve isomorphisms commute with every pullback-preserving map.
```
theorem naturality :
    h.posetFiberMap A hA ≫ fiberMap A B f hf h hA hB =
      h.posetMap (restriction A B f hf) ≫ h.posetFiberMap B hB := by
…
```
Mentions: OAI.Thomason.Construction.SieveMap.fiberMap, OAI.Thomason.Construction.SieveMap.restriction