ConstructedPosetCosieves.lean`

57 declarations, 0 contain sorry, 0 declared as axioms

Acyclic singular fibrations lift paths with both endpoints prescribed

theorem OAI.Thomason.Construction.singular_fibration_lift_path_endpoints line 32
Source documentation
A weak continuous map whose singular map is Kan lifts paths with arbitrary prescribed endpoints in their fibres. The projection of the lift is exactly the given path, not just its homotopy class.
```
theorem singular_fibration_lift_path_endpoints {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom) {x₀ x₁ : X}
    (γ : Path (p.hom x₀) (p.hom x₁)) :
    ∃ q : Path x₀ x₁, ∀ t, p.hom (q t) = γ t := by
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

theorem OAI.Thomason.Construction.singular_acyclic_lift_path_endpoints line 75

Source documentation

The endpoint-preserving lift applies directly to the actual simplicial weak-equivalence hypothesis on a singular Kan fibration.

theorem singular_acyclic_lift_path_endpoints {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : realizationWeakEquivalences (TopCat.toSSet.map p)) {x₀ x₁ : X}
    (γ : Path (p.hom x₀) (p.hom x₁)) :
    ∃ q : Path x₀ x₁, ∀ t, p.hom (q t) = γ t :=
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.singular_fibration_lift_based_cube line 107

Source documentation

A weak continuous map with singular Kan lifting lifts every based cube exactly, keeping the entire boundary at the prescribed point.

theorem singular_fibration_lift_based_cube {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom) (x : X) (n : ℕ)
    (γ : GenLoop (Fin (n+1)) Y (p.hom x)) :
    ∃ q : GenLoop (Fin (n+1)) X x, ∀ t, p.hom (q t) = γ t := by
…

Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

theorem OAI.Thomason.Construction.singular_acyclic_lift_based_cube line 140

Source documentation

The actual realization weak-equivalence test on a singular Kan fibration already suffices for exact based cube lifting in every dimension.

theorem singular_acyclic_lift_based_cube {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : realizationWeakEquivalences (TopCat.toSSet.map p)) (x : X) (n : ℕ)
    (γ : GenLoop (Fin (n+1)) Y (p.hom x)) :
    ∃ q : GenLoop (Fin (n+1)) X x, ∀ t, p.hom (q t) = γ t :=
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.RealizedCube.singularMap_boundary_comp line 168

theorem OAI.Thomason.Construction.RealizedCube.singular_fibration_constant_boundary_lift line 184

Source documentation

A singular Kan fibration which is an actual topological weak equivalence fills every cubical boundary diagram whose top map is the specified constant.

theorem singular_fibration_constant_boundary_lift {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom) (x : X) (n : ℕ)
    (b : obj (n+1) ⟶ TopCat.toSSet.obj Y)
    (hb : (boundary n).ι ≫ b = SSet.const (TopCat.toSSetObj₀Equiv.symm (p.hom x))) :
    ∃ l : obj (n+1) ⟶ TopCat.toSSet.obj X,
      (boundary n).ι ≫ l = SSet.const (TopCat.toSSetObj₀Equiv.symm x) ∧
      l ≫ TopCat.toSSet.map p = b := by
…

Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.RealizedCube.boundary

theorem OAI.Thomason.Construction.RealizedCube.singular_acyclic_constant_boundary_lift line 218

Source documentation

The same all-dimensional boundary lift from the actual simplicial weak test.

theorem singular_acyclic_constant_boundary_lift {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : realizationWeakEquivalences (TopCat.toSSet.map p)) (x : X) (n : ℕ)
    (b : obj (n+1) ⟶ TopCat.toSSet.obj Y)
    (hb : (boundary n).ι ≫ b = SSet.const (TopCat.toSSetObj₀Equiv.symm (p.hom x))) :
    ∃ l : obj (n+1) ⟶ TopCat.toSSet.obj X,
      (boundary n).ι ≫ l = SSet.const (TopCat.toSSetObj₀Equiv.symm x) ∧
      l ≫ TopCat.toSSet.map p = b :=
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.RealizedCube.boundary

theorem OAI.Thomason.Construction.singular_fibration_interval_boundary_lifting line 248
Source documentation
A weak map with singular Kan lifting solves every lifting problem for the ordinary interval and its two endpoints.
```
theorem singular_fibration_interval_boundary_lifting {X Y : TopCat.{0}}
    (p : X ⟶ Y) [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom) :
    HasLiftingProperty (RealizedCube.boundaryInclusion 0) p := by
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.RealizedCube.boundaryInclusion
theorem OAI.Thomason.Construction.singular_acyclic_interval_boundary_lifting line 297
Source documentation
The same boundary lift under the actual realization weak-equivalence hypothesis on the singular map.
```
theorem singular_acyclic_interval_boundary_lifting {X Y : TopCat.{0}}
    (p : X ⟶ Y) [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : realizationWeakEquivalences (TopCat.toSSet.map p)) :
    HasLiftingProperty (RealizedCube.boundaryInclusion 0) p :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.RealizedCube.boundaryInclusion
def OAI.Thomason.Construction.intervalOneCube line 320
def OAI.Thomason.Construction.simplexOneCube line 328
theorem OAI.Thomason.Construction.simplexOneCube_boundary line 331
def OAI.Thomason.Construction.simplexOneBoundaryArrowIso line 359
theorem OAI.Thomason.Construction.singular_acyclic_boundary_one line 368
Source documentation
This is the entire simplicial ∂Δ[1] lifting problem, with arbitrary specified endpoints, for an actual singular Kan fibration satisfying W.
```
theorem singular_acyclic_boundary_one {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : realizationWeakEquivalences (TopCat.toSSet.map p)) :
    HasLiftingProperty (SSet.boundary 1).ι (TopCat.toSSet.map p) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.fundamentalGroup_map_injective line 392

theorem OAI.Thomason.Construction.weak_path_homotopy_reflects line 404

Source documentation

Equality of fixed-endpoint path classes is reflected by the actual weak homotopy-equivalence test.

theorem weak_path_homotopy_reflects {X Y : Type} [TopologicalSpace X]
    [TopologicalSpace Y] (f : C(X, Y)) (hf : IsWeakHomotopyEquivalence f)
    {x₀ x₁ : X} {α β : Path x₀ x₁}
    (h : (α.map f.continuous).Homotopic (β.map f.continuous)) : α.Homotopic β := by
…

Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

def OAI.Thomason.Construction.PathSpace.homotopyPath line 448
Source documentation
A path homotopy is a continuous path in the compact-open path space.
```
def homotopyPath {x y : X} {α β : Path x y} (H : α.Homotopy β) : Path α β where
…
```
def OAI.Thomason.Construction.PathSpace.pathHomotopy line 455
Source documentation
Conversely a path in a fixed-endpoint path space is a relative homotopy.
```
def pathHomotopy {x y : X} {α β : Path x y} (H : Path α β) : α.Homotopy β where
…
```
theorem OAI.Thomason.Construction.PathSpace.map_components_bijective line 465
theorem OAI.Thomason.Construction.PathSpace.rightAppend_naturality line 482
theorem OAI.Thomason.Construction.PathSpace.map_group_bijective line 491
Source documentation
Every positive homotopy group of the fixed-endpoint path map is a bijection, at an arbitrary path as basepoint.
```
theorem map_group_bijective (f : C(X, Y)) (hf : IsWeakHomotopyEquivalence f)
    {x y : X} (α : Path x y) (n : ℕ) :
    Function.Bijective (HomotopyMaps.groupMap (map f) (n+1) α) := by
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.HomotopyMaps.groupMap, OAI.Thomason.Construction.PathSpace.map
theorem OAI.Thomason.Construction.PathSpace.map_weak line 513
Source documentation
The actual weak-equivalence test is preserved by passing to paths between any two specified source points, including when the path space is empty.
```
theorem map_weak (f : C(X, Y)) (hf : IsWeakHomotopyEquivalence f) (x y : X) :
    IsWeakHomotopyEquivalence (map f (x := x) (y := y)) :=
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.PathSpace.map
theorem OAI.Thomason.Construction.RealizationPrism.compact_path_family_factors line 537

theorem OAI.Thomason.Construction.RealizationPrism.compact_fixed_path_family_factors line 548

Source documentation

A compact family of paths with common endpoints has a finite-subcomplex factorization with common lifted endpoints and the same exact evaluation.

theorem compact_fixed_path_family_factors {P : Type} [TopologicalSpace P]
    [CompactSpace P] [Nonempty P] (K : SSet.{0})
    {x y : SSet.toTop.obj K} (f : C(P, Path x y)) :
    ∃ (A : K.Subcomplex), SSet.Finite (A : SSet) ∧
      ∃ (a b : SSet.toTop.obj (A : SSet)),
        (SSet.toTop.map A.ι).hom a = x ∧ (SSet.toTop.map A.ι).hom b = y ∧
        ∃ g : C(P, Path a b), ∀ p t, (SSet.toTop.map A.ι).hom (g p t) = f p t := by
…

def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.homEquiv line 595
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.adjunction line 604
Source documentation
The actual zero-fibre / terminal-cone adjunction.
```
noncomputable def adjunction : labelFiberFunctor (Fin 2) 0 ⊣ overFunctor :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.labelFiberFunctor, OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.overFunctor
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.zeroFiber_preservesColimits line 631
Source documentation
Formation of the actual full zero fibre preserves all small colimits.
```
theorem zeroFiber_preservesColimits :
    PreservesColimitsOfSize.{0,0} (labelFiberFunctor (Fin 2) 0) :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.labelFiberFunctor
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.finiteCategory line 647
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.finiteOverFunctor line 651
Source documentation
The terminal cone stays in the given positive finite dimension.
```
def finiteOverFunctor (n : ℕ) : Truncated.{0} (n+1) ⥤ Over (finiteInterval n) where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.finiteInterval
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.finiteHomEquiv line 657
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.finiteAdjunction line 666
Source documentation
Finite fibre formation is a left adjoint inside the finite category itself.
```
noncomputable def finiteAdjunction (n : ℕ) :
    finiteLabelFiberFunctor n 0 ⊣ finiteOverFunctor n :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.finiteLabelFiberFunctor, OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.finiteOverFunctor
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.finiteZeroFiber_preservesColimits line 694
Source documentation
This preserves finite-dimensional colimits, without replacing them by omega colimits.
```
theorem finiteZeroFiber_preservesColimits (n : ℕ) :
    PreservesColimitsOfSize.{0,0} (finiteLabelFiberFunctor n 0) :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.finiteLabelFiberFunctor
def OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.reverseCell line 716
def OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.intervalIso line 720
Source documentation
Reverse the strict interval together with all its directions.
```
def intervalIso : opposite (StrictPoset.category (Fin 2)) ≅ StrictPoset.category (Fin 2) where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.opposite, OAI.Thomason.Construction.StrictPoset.category
def OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.label line 747
Source documentation
The reversed label sends the original value one to zero.
```
def label {C : StrictOmegaCategory.{0}} (p : C ⟶ StrictPoset.category (Fin 2)) :
    opposite C ⟶ StrictPoset.category (Fin 2) := oppositeMap p ≫ intervalIso.hom
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.opposite, OAI.Thomason.Construction.StrictOmegaCategory.oppositeMap
def OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.overFunctor line 750
def OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.doubleIso line 760
Source documentation
Reversing twice recovers the original object in the slice.
```
def doubleIso (X : Over (StrictPoset.category (Fin 2))) :
    overFunctor.obj (overFunctor.obj X) ≅ X :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
def OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.equivalence line 768
Source documentation
Opposite interval labelling is an involutive slice equivalence.
```
def equivalence : Over (StrictPoset.category (Fin 2)) ≌ Over (StrictPoset.category (Fin 2)) where
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.label_zero_iff line 787
Source documentation
The condition on all cells is exactly transported by interval reversal.
```
theorem label_zero_iff {C : StrictOmegaCategory.{0}}
    (p : C ⟶ StrictPoset.category (Fin 2)) (x : C) :
    (label p).toFun x = StrictPoset.identity 0 ↔ p.toFun x = StrictPoset.identity 1 := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.label, OAI.Thomason.Construction.StrictPoset.identity
def OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.fiberIso line 806
Source documentation
The opposite of the reversed zero fibre is the original one fibre.
```
def fiberIso (X : Over (StrictPoset.category (Fin 2))) :
    opposite (labelFiber (label X.hom) 0) ≅ labelFiber X.hom 1 where
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.opposite, OAI.Thomason.Construction.StrictOmegaCategory.labelFiber, OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.label
def OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.fiberNatIso line 822
Source documentation
The actual one-fibre functor is conjugate to the zero-fibre functor.
```
def fiberNatIso : overFunctor ⋙ labelFiberFunctor (Fin 2) 0 ⋙ oppositeFunctor ≅
    labelFiberFunctor (Fin 2) 1 :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.overFunctor, OAI.Thomason.Construction.StrictOmegaCategory.labelFiberFunctor, OAI.Thomason.Construction.StrictOmegaCategory.oppositeFunctor
theorem OAI.Thomason.Construction.StrictOmegaCategory.OppositeLabels.oneFiber_preservesColimits line 832
Source documentation
Full one fibres, as well as zero fibres, preserve all small colimits.
```
theorem oneFiber_preservesColimits :
    PreservesColimitsOfSize.{0,0} (labelFiberFunctor (Fin 2) 1) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.labelFiberFunctor
def OAI.Thomason.Construction.CosieveSimplex.labels line 863
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.CosieveSimplex.diagram line 874
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.CosieveSimplex.cocone line 879
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.CosieveSimplex.diagram
def OAI.Thomason.Construction.CosieveSimplex.coconeIsColimit line 889
Source documentation
Forgetting the labels recovers exactly the original simplex colimit.
```
noncomputable def coconeIsColimit : IsColimit (cocone A hA h) := by
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.cocone
abbrev OAI.Thomason.Construction.CosieveSimplex.fiberCocone line 894
Source documentation
Its full one fibre is therefore the colimit of the full simplex fibres.
```
noncomputable abbrev fiberCocone : Cocone (diagram A hA h ⋙ labelFiberFunctor (Fin 2) 1) :=
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.diagram
def OAI.Thomason.Construction.CosieveSimplex.fiberCoconeIsColimit line 898
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.CosieveSimplex.fiberCocone
def OAI.Thomason.Construction.CosieveSimplex.backCocone line 903
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) 1) where
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.diagram
def OAI.Thomason.Construction.CosieveSimplex.inverse line 920
Source documentation
Descending the compatible clamping maps gives the inverse of the cosieve map.
```
noncomputable def inverse :
    labelFiber (h.membershipLabel Aᶜ hA.compl) 1 ⟶ h.categorification.obj (nerve A) :=
…
```
theorem OAI.Thomason.Construction.CosieveSimplex.inverse_fac line 925
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.CosieveSimplex.fiberCocone, OAI.Thomason.Construction.CosieveSimplex.inverse, OAI.Thomason.Construction.CosieveSimplex.back
theorem OAI.Thomason.Construction.CosieveSimplex.inverse_inclusion line 951
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.compl) 1 := by
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.inverse, OAI.Thomason.Construction.subposetInclusion
theorem OAI.Thomason.Construction.CosieveSimplex.inverse_posetFiberMap line 967
Source documentation
The descended inverse is a right inverse of the canonical sieve map.
```
theorem inverse_posetFiberMap :
    inverse A hA h ≫ h.cosievePosetFiberMap A hA = 𝟙 _ := by
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.inverse
theorem OAI.Thomason.Construction.CosieveSimplex.whole_fiberLeg line 973
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.cosievePosetFiberMap A hA := by
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.whole, OAI.Thomason.Construction.CosieveSimplex.fiberCocone, OAI.Thomason.Construction.subposetInclusion
theorem OAI.Thomason.Construction.CosieveSimplex.posetFiberMap_inverse_on_leg line 983
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.cosievePosetFiberMap A hA ≫ inverse A hA h) = h.posetLeg s := by
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.inverse
theorem OAI.Thomason.Construction.CosieveSimplex.posetFiberMap_inverse line 1008
Source documentation
The descended inverse is also a left inverse, on the original sieve colimit.
```
theorem posetFiberMap_inverse :
    h.cosievePosetFiberMap A hA ≫ inverse A hA h = 𝟙 _ := by
…
```
Mentions: OAI.Thomason.Construction.CosieveSimplex.inverse
def OAI.Thomason.Construction.NormalizedSimplexIdentities.posetCosieveIso line 1026
Source documentation
A poset sieve categorifies to exactly the full one fibre of membership.
```
noncomputable def posetCosieveIso (h : NormalizedSimplexIdentities) [StrictColimitsInput]
    {P : Type} [PartialOrder P] (A : Set P) (hA : IsUpperSet A) :
    h.categorification.obj (nerve A) ≅ labelFiber (h.membershipLabel Aᶜ hA.compl) 1 where
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictColimitsInput