FiniteCosieveMembership.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The actual Street image of a finite-dimensional cosieve

theorem OAI.Thomason.Construction.FiniteReflectionInput.cosieveMembershipLabel_object line 17
theorem OAI.Thomason.Construction.FiniteReflectionInput.cosieveMembershipLabel_inter line 32

theorem OAI.Thomason.Construction.FiniteReflectionInput.posetCosieveStreet_range line 44

Source documentation

Finite reflection identifies the literal inclusion's Street image with the full one-fibre subcomplex.

theorem posetCosieveStreet_range {P : Type} [PartialOrder P]
    (A : Set P) (hA : IsUpperSet A) :
    SSet.Subcomplex.range ((h.finiteStreetNerve (n+1)).map
      (r.reflect.map (h.posetMap (subposetInclusion A)))) =
      h.fiberStreetSubcomplex (r.membershipLabel h Aᶜ hA.compl) 1 := by
…

Mentions: OAI.Thomason.Construction.subposetInclusion

theorem OAI.Thomason.Construction.FiniteReflectionInput.posetCosieve_nerve_mono line 59
Source documentation
The actual finite-dimensional cosieve nerve map is monomorphic.
```
theorem posetCosieve_nerve_mono {P : Type} [PartialOrder P]
    (A : Set P) (hA : IsUpperSet A) :
    Mono ((h.finiteStreetNerve (n+1)).map
      (r.reflect.map (h.posetMap (subposetInclusion A)))) := by
…
```
Mentions: OAI.Thomason.Construction.subposetInclusion

theorem OAI.Thomason.Construction.FiniteReflectionInput.street_cosieve_maps_isPushout line 73

Source documentation

The actual composite N c takes this two-cosieve square to a pushout.

theorem street_cosieve_maps_isPushout
    {P : Type} [PartialOrder P]
    (A B : Set P) (hA : IsUpperSet A) (hB : IsUpperSet B)
    (hcover : ∀ x, x ∈ A ∨ x ∈ B) :
    IsPushout ((r.categorification h ⋙ h.finiteStreetNerve (n+1)).map
        (nerveMap (interLeft A B).monotone.functor))
      ((r.categorification h ⋙ h.finiteStreetNerve (n+1)).map
        (nerveMap (interRight A B).monotone.functor))
      ((h.finiteStreetNerve (n+1)).map (r.reflect.map (h.posetMap (subposetInclusion A))))
      ((h.finiteStreetNerve (n+1)).map (r.reflect.map (h.posetMap (subposetInclusion B)))) := by
…

Mentions: OAI.Thomason.Construction.interLeft, OAI.Thomason.Construction.interRight, OAI.Thomason.Construction.subposetInclusion

theorem OAI.Thomason.Construction.FiniteReflectionInput.cosieveMembershipLabel_one_iff line 131

theorem OAI.Thomason.Construction.FiniteReflectionInput.posetMap_cosieveMembership_one line 145

Source documentation

A reflected monotone map landing in a cosieve lands in its full one fibre on all cells.

theorem posetMap_cosieveMembership_one {E P : Type} [PartialOrder E] [PartialOrder P]
    (A : Set P) (hA : IsUpperSet A) (f : E →o P) (hf : ∀ x, f x ∈ A)
    (x : ((r.categorification h).obj (nerve E)).val) :
    (r.membershipLabel h Aᶜ hA.compl).toFun ((r.reflect.map (h.posetMap f)).toFun x) =
      StrictPoset.identity 1 := by
…

Mentions: OAI.Thomason.Construction.StrictPoset.identity