FinitePosetUnitInduction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite induction for the actual adjunction-unit comparison

Empty and greatest-element posets are the base cases. Every other finite poset is covered by deleting two distinct maximal elements. The published simplicial gluing lemma applies to the natural transformation on the two actual nerve squares. All hypotheses below are proved for the constructed Street adjunctions in the following specialization.

theorem OAI.Thomason.Construction.comparison_two_sieve_gluing line 23

Source documentation

Two-sieve gluing for a natural comparison on ordinary poset nerves.

theorem comparison_two_sieve_gluing {F : SSet.{0} ⥤ SSet.{0}} (η : 𝟭 _ ⟶ F)
    (g : PublishedSimplicialGluingInput)
    {P : Type} [PartialOrder P] (A B : Set P)
    (hA : IsLowerSet A) (hB : IsLowerSet B) (hc : ∀ x, x ∈ A ∨ x ∈ B)
    (hp : IsPushout (F.map (nerveMap (interLeft A B).monotone.functor))
      (F.map (nerveMap (interRight A B).monotone.functor))
      (F.map (nerveMap (subposetInclusion A).monotone.functor))
      (F.map (nerveMap (subposetInclusion B).monotone.functor)))
    [Mono (F.map (nerveMap (subposetInclusion (A ∩ B)).monotone.functor))]
    (wA : realizationWeakEquivalences (η.app (nerve A)))
    (wB : realizationWeakEquivalences (η.app (nerve B)))
    (wI : realizationWeakEquivalences (η.app (nerve (A ∩ B : Set P)))) :
…

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

theorem OAI.Thomason.Construction.finite_poset_comparison_induction line 53

Source documentation

Finite induction uses the empty and greatest-element cases and the preservation of these particular two-sieve pushouts.

theorem finite_poset_comparison_induction
    {F : SSet.{0} ⥤ SSet.{0}} (η : 𝟭 _ ⟶ F) (g : PublishedSimplicialGluingInput)
    (hempty : ∀ (P : Type) [PartialOrder P] [IsEmpty P],
      realizationWeakEquivalences (η.app (nerve P)))
    (hgreat : ∀ (P : Type) [PartialOrder P] (x : P), (∀ y, y ≤ x) →
      realizationWeakEquivalences (η.app (nerve P)))
    (hmono : ∀ (P : Type) [PartialOrder P] [Finite P] (A : Set P), IsLowerSet A →
      Mono (F.map (nerveMap (subposetInclusion A).monotone.functor)))
    (hpushout : ∀ (P : Type) [PartialOrder P] [Finite P] (A B : Set P),
      IsLowerSet A → IsLowerSet B → (∀ x, x ∈ A ∨ x ∈ B) →
      IsPushout (F.map (nerveMap (interLeft A B).monotone.functor))
        (F.map (nerveMap (interRight A B).monotone.functor))
…

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