FiniteSieveNaturality.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Thomason.Construction.SieveMap.finiteMembership line 21
Source documentation
Reflected membership labels commute with the original reflected map.
```
theorem finiteMembership :
    Hom.comp (r.reflect.map (h.posetMap f)) (r.membershipLabel h B hB) =
      r.membershipLabel h A hA := by
…
```

def OAI.Thomason.Construction.SieveMap.finiteFiberMap line 37

Source documentation

This is the restriction to full zero fibres of the reflected map itself.

noncomputable def finiteFiberMap :
    r.reflectedLabelFiber (r.membershipLabel h A hA) ⟶
      r.reflectedLabelFiber (r.membershipLabel h B hB) :=
…

theorem OAI.Thomason.Construction.SieveMap.finiteNaturality line 44
Source documentation
Naturality holds in the finite category, not only after lifting it to omega.
```
theorem finiteNaturality :
    r.posetFiberMap h A hA ≫ finiteFiberMap r A B f hf h hA hB =
      r.reflect.map (h.posetMap (restriction A B f hf)) ≫ r.posetFiberMap h B hB := by
…
```
Mentions: OAI.Thomason.Construction.SieveMap.finiteFiberMap, OAI.Thomason.Construction.SieveMap.restriction
theorem OAI.Thomason.Construction.SieveMap.finiteSieve_isIso line 59
Source documentation
The canonical finite sieve identification is an isomorphism.
```
theorem finiteSieve_isIso :
    IsIso (C := Truncated (n+1)) (r.posetFiberMap h A hA) := by
…
```