OAI/CategoryTheory/Thomason/Transfer/FiniteCosieveAttachmentCover.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thomason.Construction.FiniteReflectionInput.cosieve_piece_pushout line 19

   Source documentation

   The smaller categorified poset attachment is the actual full finite fibre.

   theorem cosieve_piece_pushout {P : Type} [PartialOrder P]
       (A U : Set P) (hU : IsUpperSet U) (hAU : A ⊆ U)
       {X Y : Truncated.{0} (n + 1)}
       {a : (r.categorification h).obj (nerve A) ⟶ X}
       {b : (r.categorification h).obj (nerve P) ⟶ Y} {j : X ⟶ Y}
       (hp : IsPushout (r.reflect.map (h.posetMap (subposetInclusion A))) a b j)
       (pY : Y ⟶ finiteInterval n)
       (hb : b ≫ pY = r.membershipLabel h Uᶜ hU.compl) (hj : j ≫ pY = finiteConstantLabel X 1) :
       IsPushout (r.reflect.map (h.posetMap (subposetInclusionWithin A U hAU))) a
         (((r.posetCosieveIso h U hU).hom) ≫ finiteLabelFiberMap (r.membershipLabel h Uᶜ hU.compl) pY 1 b hb)
         ((finiteConstantFiberIso X 1).inv ≫
           finiteLabelFiberMap (finiteConstantLabel X 1) pY 1 j hj) := by
   …

   Mentions: OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.subposetInclusionWithin

2. theorem OAI.Thomason.Construction.FiniteReflectionInput.cosieve_piece_label line 49

   Source documentation

   Construct the compatible label using the original finite pushout.

   theorem cosieve_piece_label {P : Type} [PartialOrder P]
       (A U : Set P) (hU : IsUpperSet U) (hAU : A ⊆ U)
       {X Y : Truncated.{0} (n + 1)}
       {a : (r.categorification h).obj (nerve A) ⟶ X}
       {b : (r.categorification h).obj (nerve P) ⟶ Y} {j : X ⟶ Y}
       (hp : IsPushout (r.reflect.map (h.posetMap (subposetInclusion A))) a b j) :
       ∃ pY : Y ⟶ finiteInterval n,
         b ≫ pY = r.membershipLabel h Uᶜ hU.compl ∧ j ≫ pY = finiteConstantLabel X 1 := by
   …

   Mentions: OAI.Thomason.Construction.subposetInclusion

3. theorem OAI.Thomason.Construction.FiniteReflectionInput.disjoint_cosieve_piece_label line 68

   Source documentation

   A disjoint cosieve extends across the old target by the constant zero label.

   theorem disjoint_cosieve_piece_label {P : Type} [PartialOrder P]
       (A U : Set P) (hU : IsUpperSet U) (hAU : ∀ x ∈ A, x ∉ U)
       {X Y : Truncated.{0} (n+1)}
       {a : (r.categorification h).obj (nerve A) ⟶ X}
       {b : (r.categorification h).obj (nerve P) ⟶ Y} {j : X ⟶ Y}
       (hp : IsPushout (r.reflect.map (h.posetMap (subposetInclusion A))) a b j) :
       ∃ pY : Y ⟶ finiteInterval n,
         b ≫ pY = r.membershipLabel h Uᶜ hU.compl ∧ j ≫ pY = finiteConstantLabel X 0 := by
   …

   Mentions: OAI.Thomason.Construction.subposetInclusion

4. theorem OAI.Thomason.Construction.FiniteReflectionInput.disjoint_cosieve_piece_iso line 86

   Source documentation

   The disjoint finite cosieve is isomorphic to the post-attachment fibre.

   theorem disjoint_cosieve_piece_iso {P : Type} [PartialOrder P]
       (A U : Set P) (hU : IsUpperSet U) (hAU : ∀ x ∈ A, x ∉ U)
       {X Y : Truncated.{0} (n+1)}
       {a : (r.categorification h).obj (nerve A) ⟶ X}
       {b : (r.categorification h).obj (nerve P) ⟶ Y} {j : X ⟶ Y}
       (hp : IsPushout (r.reflect.map (h.posetMap (subposetInclusion A))) a b j)
       (pY : Y ⟶ finiteInterval n)
       (hb : b ≫ pY = r.membershipLabel h Uᶜ hU.compl) (hj : j ≫ pY = finiteConstantLabel X 0) :
       IsIso ((r.posetCosieveIso h U hU).hom ≫
         finiteLabelFiberMap (r.membershipLabel h Uᶜ hU.compl) pY 1 b hb) := by
   …

   Mentions: OAI.Thomason.Construction.subposetInclusion

5. theorem OAI.Thomason.Construction.FiniteReflectionInput.cosieve_attachment_street_pushout line 126