FiniteKanBaseChangeApproximation.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Compact homotopy-fibre families factor through a finite simplicial base

theorem OAI.Thomason.Construction.compact_homotopyFiber_finite_base line 21

Source documentation

Every compact family in the genuine homotopy fibre of a realized map factors through one finite subcomplex of its base. The entire path, both endpoints, and the original total-space coordinate are retained exactly.

theorem compact_homotopyFiber_finite_base {K : Type} [TopologicalSpace K] [CompactSpace K]
    {E B : SSet.{0}} (p : E ⟶ B) (b : B.obj (.op (.mk 0)))
    (f : C(K, continuousHomotopyFiber (SSet.toTop.map p) (RealizationPrism.vertexPoint B b))) :
    ∃ (A : B.Subcomplex) (_ : SSet.Finite A.toSSet)
      (bA : A.toSSet.obj (.op (.mk 0))), bA.val = b ∧
      ∃ g : C(K, continuousHomotopyFiber (SSet.toTop.map (A.fromPreimage p))
          (RealizationPrism.vertexPoint A.toSSet bA)),
        (∀ k, (SSet.toTop.map (A.preimage p).ι).hom (g k).val.val.1 = (f k).val.val.1) ∧
        (∀ k t, (SSet.toTop.map A.ι).hom ((g k).val.val.2 t) = (f k).val.val.2 t) := by
…

Mentions: OAI.Thomason.Construction.continuousHomotopyFiber, OAI.Thomason.Construction.RealizationPrism.vertexPoint

theorem OAI.Thomason.Construction.compact_homotopyFiber_finite_arrow line 118

Source documentation

A compact family in a homotopy fibre is supported on an actual map between finite simplicial sets. Both comparison maps are monomorphisms, the square commutes strictly, and the entire original path is recovered.

theorem compact_homotopyFiber_finite_arrow {K : Type} [TopologicalSpace K] [CompactSpace K]
    {E B : SSet.{0}} (p : E ⟶ B) (b : B.obj (.op (.mk 0)))
    (f : C(K, continuousHomotopyFiber (SSet.toTop.map p) (RealizationPrism.vertexPoint B b))) :
    ∃ (A : B.Subcomplex) (_ : SSet.Finite A.toSSet)
      (L : SSet.{0}) (_ : SSet.Finite L) (j : L ⟶ E) (_ : Mono j)
      (q : L ⟶ A.toSSet) (bA : A.toSSet.obj (.op (.mk 0))),
      q ≫ A.ι = j ≫ p ∧ bA.val = b ∧
      ∃ g : C(K, continuousHomotopyFiber (SSet.toTop.map q)
          (RealizationPrism.vertexPoint A.toSSet bA)),
        (∀ k, (SSet.toTop.map j).hom (g k).val.val.1 = (f k).val.val.1) ∧
        (∀ k t, (SSet.toTop.map A.ι).hom ((g k).val.val.2 t) = (f k).val.val.2 t) := by
…

Mentions: OAI.Thomason.Construction.continuousHomotopyFiber, OAI.Thomason.Construction.RealizationPrism.vertexPoint

instance OAI.Thomason.Construction.kanBaseChangeWeak_stableUnderRetracts line 180
Source documentation
The Kan base-change property is closed under arrow retracts. The fibration above the larger target is pulled back along its retraction.
```
instance kanBaseChangeWeak_stableUnderRetracts : kanBaseChangeWeak.IsStableUnderRetracts where
…
```
instance OAI.Thomason.Construction.kanBaseChangeWeak_multiplicative line 262
theorem OAI.Thomason.Construction.sequence_map_mono_and_weak line 268

theorem OAI.Thomason.Construction.simplicial_sequence_leg_mono line 288

Source documentation

A colimit of a monic simplicial sequence has monic structure maps.

theorem simplicial_sequence_leg_mono (F : ℕ ⥤ SSet.{0}) {c : Cocone F}
    (hc : IsColimit c) (hm : ∀ n m (h : n ≤ m), Mono (F.map (homOfLE h))) (n : ℕ) :
    Mono (c.ι.app n) := by
…

theorem OAI.Thomason.Construction.kanBaseChangeWeak_sequence line 304
Source documentation
Countable monic sequences preserve the actual Kan base-change weak test. The colimit is replaced by its increasing image subcomplexes only inside this proof; its original initial structure map is the conclusion.
```
theorem kanBaseChangeWeak_sequence (F : ℕ ⥤ SSet.{0}) {c : Cocone F}
    (hc : IsColimit c) (hm : ∀ n, Mono (F.map (homOfLE (Nat.le_succ n))))
    (hw : ∀ n, kanBaseChangeWeak (F.map (homOfLE (Nat.le_succ n)))) :
    kanBaseChangeWeak (c.ι.app 0) := by
…
```
Mentions: OAI.Thomason.Construction.kanBaseChangeWeak
abbrev OAI.Thomason.Construction.kanWeakMonomorphisms line 366
instance OAI.Thomason.Construction.kanWeakMonomorphisms_cobaseChange line 369
instance OAI.Thomason.Construction.kanWeakMonomorphisms_coproducts line 375
instance OAI.Thomason.Construction.kanWeakMonomorphisms_countable line 381
theorem OAI.Thomason.Construction.horn_generators_kanWeak line 408
Source documentation
Every horn generator has the required strengthened weak property.
```
theorem horn_generators_kanWeak : J.{0} ≤ kanWeakMonomorphisms := by
…
```
Mentions: OAI.Thomason.Construction.kanWeakMonomorphisms
theorem OAI.Thomason.Construction.anodyne_kanBaseChangeWeak line 417
Source documentation
Arbitrary anodyne extensions become actual realization weak equivalences on pullback along Kan fibrations.
```
theorem anodyne_kanBaseChangeWeak : SSet.anodyneExtensions.{0} ≤ kanWeakMonomorphisms := by
…
```
Mentions: OAI.Thomason.Construction.kanWeakMonomorphisms
theorem OAI.Thomason.Construction.kan_pullback_anodyne_weak line 427
Source documentation
The original canonical pullback map satisfies the actual weak test.
```
theorem kan_pullback_anodyne_weak {A B E : SSet.{0}} (i : A ⟶ B)
    (hi : SSet.anodyneExtensions i) (p : E ⟶ B) [HomotopicalAlgebra.Fibration p] :
    realizationWeakEquivalences (pullback.fst p i) :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

def OAI.Thomason.Construction.kanExtensionComparison line 450

Source documentation

The actual comparison to the restriction of a larger total space.

def kanExtensionComparison {E F B C : SSet.{0}} (p : E ⟶ B) (i : B ⟶ C)
    (j : E ⟶ F) (q : F ⟶ C) (h : j ≫ q = p ≫ i) : E ⟶ pullback q i :=
…

theorem OAI.Thomason.Construction.kanExtensionComparison_fst line 455
theorem OAI.Thomason.Construction.kanExtensionComparison_snd line 460

theorem OAI.Thomason.Construction.kanExtensionComparison_mono_weak line 466

Source documentation

Extending both base and total space by anodyne maps gives an actual weak comparison with the restriction, when the new projection is Kan.

theorem kanExtensionComparison_mono_weak {E F B C : SSet.{0}}
    (p : E ⟶ B) (i : B ⟶ C) (j : E ⟶ F) (q : F ⟶ C)
    (h : j ≫ q = p ≫ i) (hi : SSet.anodyneExtensions i)
    (hj : SSet.anodyneExtensions j) [HomotopicalAlgebra.Fibration q] :
    Mono (kanExtensionComparison p i j q h) ∧
      realizationWeakEquivalences (kanExtensionComparison p i j q h) := by
…

Mentions: OAI.Thomason.Construction.kanExtensionComparison, OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.exists_kan_anodyne_extension line 482

Source documentation

Every map over an anodyne extension of its base admits such a comparison. This uses only the algebraic horn factorization.

theorem exists_kan_anodyne_extension {E B C : SSet.{0}} (p : E ⟶ B)
    (i : B ⟶ C) (hi : SSet.anodyneExtensions i) :
    ∃ (F : SSet.{0}) (j : E ⟶ F) (q : F ⟶ C),
      SSet.anodyneExtensions j ∧ HomotopicalAlgebra.Fibration q ∧
      ∃ h : j ≫ q = p ≫ i,
        Mono (kanExtensionComparison p i j q h) ∧
        realizationWeakEquivalences (kanExtensionComparison p i j q h) := by
…

Mentions: OAI.Thomason.Construction.kanExtensionComparison, OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.kan_anodyne_preimage_weak line 514

Source documentation

The actual preimage inclusion of an anodyne subcomplex is weak.

theorem kan_anodyne_preimage_weak {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (A : B.Subcomplex) (hA : SSet.anodyneExtensions A.ι) :
    realizationWeakEquivalences (A.preimage p).ι :=
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.finite_relative_kan_preimage_approximation line 522

Source documentation

A finite relative lifting problem into the total realization can be moved into an anodyne preimage, keeping the prescribed boundary exactly. Both the lift and the whole relative homotopy lie in finite subcomplexes.

theorem finite_relative_kan_preimage_approximation {E B K L : SSet.{0}} [L.Finite]
    (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (A : B.Subcomplex) (hA : SSet.anodyneExtensions A.ι)
    (i : K ⟶ L) [Mono i] (a : K ⟶ (A.preimage p).toSSet)
    (b : SSet.toTop.obj L ⟶ SSet.toTop.obj E)
    (h : SSet.toTop.map a ≫ SSet.toTop.map (A.preimage p).ι = SSet.toTop.map i ≫ b) :
    ∃ (S : (A.preimage p).toSSet.Subcomplex) (T : E.Subcomplex),
      SSet.Finite S.toSSet ∧ SSet.Finite T.toSSet ∧
      ∃ (g : S.toSSet ⟶ T.toSSet) (a' : K ⟶ S.toSSet)
        (c : SSet.toTop.obj L ⟶ SSet.toTop.obj S.toSSet)
        (b' : SSet.toTop.obj L ⟶ SSet.toTop.obj T.toSSet),
        g ≫ T.ι = S.ι ≫ (A.preimage p).ι ∧ a' ≫ S.ι = a ∧
…