KanBaseChangeExhaustion.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

Exact finite approximation inside fibres over contracted parameters

theorem OAI.Thomason.Construction.contracted_realization_to_point_weak line 33
Source documentation
The explicit stationary simplicial contraction makes the actual realization weakly contractible, via its original chosen vertex.
```
theorem contracted_realization_to_point_weak (B : SSet.{0}) (v : B _⦋0⦌)
    (C : SSet.Homotopy (SSet.const v) (𝟙 B))
    (hC : ∀ L : SSet.{0}, (SSet.const (X := L) v) ▷ Δ[1] ≫ C.h =
…
```
theorem OAI.Thomason.Construction.kan_acyclic_finite_contracted_continuousFiber_weak line 61
Source documentation
Every real-point fibre of an acyclic Kan map over the finite contracted base is weakly contractible. No choice of vertex for that point or singular replacement of the original total space is used.
```
theorem kan_acyclic_finite_contracted_continuousFiber_weak
    {E B : SSet.{0}} [B.Finite] (v : B _⦋0⦌)
    (C : SSet.Homotopy (SSet.const v) (𝟙 B))
    (hC : ∀ L : SSet.{0}, (SSet.const (X := L) v) ▷ Δ[1] ≫ C.h =
…
```
theorem OAI.Thomason.Construction.kan_acyclic_finite_contracted_simplicialFiber_weak line 76
Source documentation
The original simplicial vertex fibre has the same weak-contractibility test. This is the fibre in which the higher boundary must eventually be filled simplicially.
```
theorem kan_acyclic_finite_contracted_simplicialFiber_weak
    {E B : SSet.{0}} [B.Finite] (v : B _⦋0⦌)
    (C : SSet.Homotopy (SSet.const v) (𝟙 B))
    (hC : ∀ L : SSet.{0}, (SSet.const (X := L) v) ▷ Δ[1] ≫ C.h =
…
```
theorem OAI.Thomason.Construction.finite_relative_contracted_fiber_extension line 91
Source documentation
A finite higher extension problem admits an exact continuous extension in one finite subcomplex of the ORIGINAL simplicial fibre. The entire prescribed boundary map is retained, before applying any singular unit.
```
theorem finite_relative_contracted_fiber_extension
    {E B A K : SSet.{0}} [B.Finite] [K.Finite] (v : B _⦋0⦌)
    (C : SSet.Homotopy (SSet.const v) (𝟙 B))
    (hC : ∀ L : SSet.{0}, (SSet.const (X := L) v) ▷ Δ[1] ≫ C.h =
…
```

theorem OAI.Thomason.Construction.RealizedCube.finite_relative_fiber_approximation line 137

Source documentation

A continuous relative family in the total realization of a cubical Kan fibration can be moved into any vertex fibre, in finite support. The boundary is kept simplicial and exact, and the resulting total-space homotopy is stationary there. No acyclicity of the original fibration is needed.

theorem finite_relative_fiber_approximation {E A K : SSet.{0}} [K.Finite]
    (n : ℕ) (p : E ⟶ obj n) [HomotopicalAlgebra.Fibration p] (b : (obj n) _⦋0⦌)
    (i : A ⟶ K) [Mono i] (a : A ⟶ (simplicialPointFiber p b).toSSet)
    (d : SSet.toTop.obj K ⟶ SSet.toTop.obj E)
    (h : SSet.toTop.map a ≫ SSet.toTop.map (simplicialPointFiber p b).ι =
      SSet.toTop.map i ≫ d) :
    ∃ S : (simplicialPointFiber p b).toSSet.Subcomplex,
      SSet.Finite S.toSSet ∧ ∃ (a' : A ⟶ S.toSSet)
        (c : SSet.toTop.obj K ⟶ SSet.toTop.obj S.toSSet),
        a' ≫ S.ι = a ∧ SSet.toTop.map i ≫ c = SSet.toTop.map a' ∧
        Nonempty ((c ≫ SSet.toTop.map S.ι ≫
          SSet.toTop.map (simplicialPointFiber p b).ι).hom.HomotopyRel d.hom
…

Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.simplicialPointFiber

theorem OAI.Thomason.Construction.RealizedCube.acyclic_fiber_weak line 155
Source documentation
Every vertex fibre of an actual weak Kan fibration over a finite cube has weakly contractible realization.
```
theorem acyclic_fiber_weak {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ obj n) [HomotopicalAlgebra.Fibration p]
    (hp : realizationWeakEquivalences p) (b : (obj n) _⦋0⦌) :
    IsWeakHomotopyEquivalence
      (ContinuousMap.const (SSet.toTop.obj (simplicialPointFiber p b).toSSet) ()) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.simplicialPointFiber

theorem OAI.Thomason.Construction.RealizedCube.finite_relative_acyclic_fiber_extension line 167

Source documentation

Higher finite relative extension in an acyclic cubical fibre has an exact continuous solution in one finite subcomplex of the literal fibre.

theorem finite_relative_acyclic_fiber_extension {E A K : SSet.{0}} [K.Finite]
    (n : ℕ) (p : E ⟶ obj n) [HomotopicalAlgebra.Fibration p]
    (hp : realizationWeakEquivalences p) (b : (obj n) _⦋0⦌)
    (i : A ⟶ K) [Mono i] (a : A ⟶ (simplicialPointFiber p b).toSSet) :
    ∃ S : (simplicialPointFiber p b).toSSet.Subcomplex,
      SSet.Finite S.toSSet ∧ ∃ (a' : A ⟶ S.toSSet)
        (c : SSet.toTop.obj K ⟶ SSet.toTop.obj S.toSSet),
        a' ≫ S.ι = a ∧ SSet.toTop.map i ≫ c = SSet.toTop.map a' := by
…

Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.simplicialPointFiber

theorem OAI.Thomason.Construction.RealizedCube.acyclic_edge_lifting line 208
Source documentation
An actual weak Kan fibration over a finite cube lifts every edge with both endpoints prescribed. The endpoint correction is performed by an actual edge in the weakly contractible vertex fibre.
```
theorem acyclic_edge_lifting {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ obj n) [HomotopicalAlgebra.Fibration p]
    (hp : realizationWeakEquivalences p) (x y : E _⦋0⦌)
    (b : SSet.Edge (p.app _ x) (p.app _ y)) :
    ∃ e : SSet.Edge x y, e.map p = b :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.RealizedCube.acyclic_boundary_one line 217
Source documentation
The full one-dimensional acyclic boundary lifting theorem for arbitrary Kan fibrations whose base is a finite simplicial cube.
```
theorem acyclic_boundary_one {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ obj n) [HomotopicalAlgebra.Fibration p]
    (hp : realizationWeakEquivalences p) :
    HasLiftingProperty (SSet.boundary 1).ι p :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.RealizedCube.finite_boundary_lifting_reduction line 246
Source documentation
A weak Kan map over a finite cube gives every cubical boundary square an exact continuous extension in one finite subcomplex of its ORIGINAL initial simplicial fibre. The original square has a simplicial lift exactly when the retained boundary is simplicially nullhomotopic in that fibre. No Kan or acyclicity property is asserted for the finite carrier itself.
```
theorem finite_boundary_lifting_reduction {E : SSet.{0}} (m n : ℕ)
    (p : E ⟶ obj m) [HomotopicalAlgebra.Fibration p]
    (hp : realizationWeakEquivalences p)
    (a : (boundary n : SSet.{0}) ⟶ E) (b : obj (n+1) ⟶ obj m)
    (hab : a ≫ p = (boundary n).ι ≫ b) :
    ∃ (r : E ⟶ (simplicialPointFiber p (initialVertex m)).toSSet)
      (S : (simplicialPointFiber p (initialVertex m)).toSSet.Subcomplex)
      (_ : SSet.Finite S.toSSet)
      (aS : (boundary n : SSet.{0}) ⟶ S.toSSet)
      (c : SSet.toTop.obj (obj (n+1)) ⟶ SSet.toTop.obj S.toSSet),
      (simplicialPointFiber p (initialVertex m)).ι ≫ r = 𝟙 _ ∧
      aS ≫ S.ι = a ≫ r ∧
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.RealizedCube.boundary, OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.RealizedCube.initialVertex

theorem OAI.Thomason.Construction.finite_relative_lift_with_homotopy_support line 288

Source documentation

A relative weak lift between realizations can be confined to a map of finite subcomplexes, including the entire homotopy in the target. The original simplicial boundary is retained exactly.

theorem finite_relative_lift_with_homotopy_support {A B L Y : SSet.{0}} [B.Finite]
    (i : A ⟶ B) [Mono i] (f : L ⟶ Y) (hf : realizationWeakEquivalences f)
    (a : A ⟶ L) (b : SSet.toTop.obj B ⟶ SSet.toTop.obj Y)
    (h : SSet.toTop.map a ≫ SSet.toTop.map f = SSet.toTop.map i ≫ b) :
    ∃ (S : L.Subcomplex) (T : Y.Subcomplex),
      SSet.Finite S.toSSet ∧ SSet.Finite T.toSSet ∧
      ∃ (g : S.toSSet ⟶ T.toSSet) (a' : A ⟶ S.toSSet)
        (c : SSet.toTop.obj B ⟶ SSet.toTop.obj S.toSSet)
        (b' : SSet.toTop.obj B ⟶ SSet.toTop.obj T.toSSet),
        g ≫ T.ι = S.ι ≫ f ∧ a' ≫ S.ι = a ∧
        SSet.toTop.map i ≫ c = SSet.toTop.map a' ∧
        b' ≫ SSet.toTop.map T.ι = b ∧
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.kan_acyclic_simplex_fiber_weak line 379
Source documentation
Every vertex fibre of an actual weak Kan fibration over a standard simplex has weakly contractible realization.
```
theorem kan_acyclic_simplex_fiber_weak {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p]
    (hp : realizationWeakEquivalences p) (b : (Δ[n] : SSet.{0}) _⦋0⦌) :
    IsWeakHomotopyEquivalence
      (ContinuousMap.const (SSet.toTop.obj (simplicialPointFiber p b).toSSet) ()) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.simplicialPointFiber

theorem OAI.Thomason.Construction.finite_relative_simplex_fiber_extension line 393

Source documentation

A finite relative extension problem in such a fibre has an exact continuous solution in one finite subcomplex of the same literal fibre. The boundary map stays simplicial and is preserved exactly. This theorem asserts the geometric finite approximation stage, not a simplicial filler.

theorem finite_relative_simplex_fiber_extension {E A K : SSet.{0}} [K.Finite]
    (n : ℕ) (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p]
    (hp : realizationWeakEquivalences p) (b : (Δ[n] : SSet.{0}) _⦋0⦌)
    (i : A ⟶ K) [Mono i] (a : A ⟶ (simplicialPointFiber p b).toSSet) :
    ∃ S : (simplicialPointFiber p b).toSSet.Subcomplex,
      SSet.Finite S.toSSet ∧ ∃ (a' : A ⟶ S.toSSet)
        (c : SSet.toTop.obj K ⟶ SSet.toTop.obj S.toSSet),
        a' ≫ S.ι = a ∧ SSet.toTop.map i ≫ c = SSet.toTop.map a' := by
…

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

theorem OAI.Thomason.Construction.singular_relative_lift_of_continuous line 433

Source documentation

A continuous relative weak lift has an exact simplicial adjoint and a stationary simplicial projection homotopy. The target remains the singular realization; no descent to the original simplicial set is asserted.

theorem singular_relative_lift_of_continuous {A K E B : SSet.{0}}
    (i : A ⟶ K) (p : E ⟶ B) (a : A ⟶ E) (b : K ⟶ B)
    (c : SSet.toTop.obj K ⟶ SSet.toTop.obj E)
    (hc : SSet.toTop.map i ≫ c = SSet.toTop.map a)
    (H : (c ≫ SSet.toTop.map p).hom.HomotopyRel (SSet.toTop.map b).hom
      (Set.range (SSet.toTop.map i).hom)) :
    ∃ (d : K ⟶ TopCat.toSSet.obj (SSet.toTop.obj E))
      (G : SSet.Homotopy (d ≫ TopCat.toSSet.map (SSet.toTop.map p))
        (b ≫ sSetTopAdj.unit.app B)),
      i ≫ d = a ≫ sSetTopAdj.unit.app E ∧
      i ▷ Δ[1] ≫ G.h =
        fst A Δ[1] ≫ a ≫ sSetTopAdj.unit.app E ≫ TopCat.toSSet.map (SSet.toTop.map p) := by
…

theorem OAI.Thomason.Construction.finite_singular_relative_lift_of_continuous line 474

Source documentation

The complete singular relative lift lies in two finite subcomplexes, including every simplex of its stationary projection homotopy.

theorem finite_singular_relative_lift_of_continuous {A K E B : SSet.{0}} [K.Finite]
    (i : A ⟶ K) (p : E ⟶ B) (a : A ⟶ E) (b : K ⟶ B)
    (c : SSet.toTop.obj K ⟶ SSet.toTop.obj E)
    (hc : SSet.toTop.map i ≫ c = SSet.toTop.map a)
    (H : (c ≫ SSet.toTop.map p).hom.HomotopyRel (SSet.toTop.map b).hom
      (Set.range (SSet.toTop.map i).hom)) :
    ∃ (S : (TopCat.toSSet.obj (SSet.toTop.obj E)).Subcomplex)
      (T : (TopCat.toSSet.obj (SSet.toTop.obj B)).Subcomplex),
      SSet.Finite S.toSSet ∧ SSet.Finite T.toSSet ∧
      ∃ (q : S.toSSet ⟶ T.toSSet) (aS : A ⟶ S.toSSet)
        (bT : K ⟶ T.toSSet) (dS : K ⟶ S.toSSet)
        (G : SSet.Homotopy (dS ≫ q) bT),
…

theorem OAI.Thomason.Construction.finite_singular_weak_relative_lift line 540

Source documentation

Every actual weak simplicial map admits this finite, stationary singular approximation to each finite relative lifting problem. A Kan hypothesis is not needed until descent and exactification in the original simplicial set.

theorem finite_singular_weak_relative_lift {A K E B : SSet.{0}} [K.Finite]
    (i : A ⟶ K) [Mono i] (p : E ⟶ B) (hp : realizationWeakEquivalences p)
    (a : A ⟶ E) (b : K ⟶ B) (h : a ≫ p = i ≫ b) :
    ∃ (S : (TopCat.toSSet.obj (SSet.toTop.obj E)).Subcomplex)
      (T : (TopCat.toSSet.obj (SSet.toTop.obj B)).Subcomplex),
      SSet.Finite S.toSSet ∧ SSet.Finite T.toSSet ∧
      ∃ (q : S.toSSet ⟶ T.toSSet) (aS : A ⟶ S.toSSet)
        (bT : K ⟶ T.toSSet) (dS : K ⟶ S.toSSet)
        (G : SSet.Homotopy (dS ≫ q) bT),
        q ≫ T.ι = S.ι ≫ TopCat.toSSet.map (SSet.toTop.map p) ∧
        aS ≫ S.ι = a ≫ sSetTopAdj.unit.app E ∧
        bT ≫ T.ι = b ≫ sSetTopAdj.unit.app B ∧ i ≫ dS = aS ∧
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.weak_mono_realization_deformation line 577

Source documentation

A monomorphic actual realization weak equivalence has a continuous retraction and a homotopy fixing its entire realized image.

theorem weak_mono_realization_deformation {A B : SSet.{0}} (i : A ⟶ B) [Mono i]
    (hi : realizationWeakEquivalences i) :
    ∃ r : SSet.toTop.obj B ⟶ SSet.toTop.obj A,
      SSet.toTop.map i ≫ r = 𝟙 _ ∧
      Nonempty ((r ≫ SSet.toTop.map i).hom.HomotopyRel (ContinuousMap.id _)
        (Set.range (SSet.toTop.map i).hom)) := by
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.weak_mono_iff_realization_deformation line 587

Source documentation

The strong deformation condition is exactly the realization weak test on a simplicial monomorphism. No anodyne-class identification is assumed.

theorem weak_mono_iff_realization_deformation {A B : SSet.{0}} (i : A ⟶ B) [Mono i] :
    realizationWeakEquivalences i ↔
      ∃ r : SSet.toTop.obj B ⟶ SSet.toTop.obj A,
        SSet.toTop.map i ≫ r = 𝟙 _ ∧
        Nonempty ((r ≫ SSet.toTop.map i).hom.HomotopyRel (ContinuousMap.id _)
          (Set.range (SSet.toTop.map i).hom)) := by
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.weak_mono_coproduct line 628

theorem OAI.Thomason.Construction.realization_coproduct_weak line 642

Source documentation

The original coproduct map satisfies the actual realization weak test.

theorem realization_coproduct_weak {α : Type} {A B : α → SSet.{0}}
    (f : ∀ a, A a ⟶ B a) (hf : ∀ a, realizationWeakEquivalences (f a)) :
    realizationWeakEquivalences (CategoryTheory.Limits.Sigma.map f) := by
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

def OAI.Thomason.Construction.simplicialCofan_pullback_isColimit line 702

Source documentation

An arbitrary coproduct of simplicial sets remains a coproduct after pullback. The proof uses the literal disjoint partition in each degree.

def simplicialCofan_pullback_isColimit {α : Type} {A D : α → SSet.{0}}
    (c : Cofan A) (hc : IsColimit c)
    (d : Cofan D) (p : d.pt ⟶ c.pt) (q : ∀ a, D a ⟶ A a)
    (h : ∀ a, IsPullback (d.inj a) (q a) p (c.inj a)) : IsColimit d := by
…

def OAI.Thomason.Construction.simplicialCofan_pullback line 739

Source documentation

Canonical pullback pieces above an arbitrary coproduct form a coproduct of the original total space.

def simplicialCofan_pullback (α : Type) (A : α → SSet.{0}) (c : Cofan A)
    (hc : IsColimit c) {E : SSet.{0}} (p : E ⟶ c.pt) :
    IsColimit (Cofan.mk E (fun a => pullback.fst p (c.inj a))) :=
…

theorem OAI.Thomason.Construction.simplicialCofan_map_weak line 747

Source documentation

Objectwise actual weak equivalences between arbitrary coproduct presentations induce a weak equivalence of the original total objects.

theorem simplicialCofan_map_weak {α : Type} {A B : α → SSet.{0}}
    (c : Cofan A) (hc : IsColimit c) (d : Cofan B) (hd : IsColimit d)
    (f : c.pt ⟶ d.pt) (u : ∀ a, A a ⟶ B a)
    (hu : ∀ a, c.inj a ≫ f = u a ≫ d.inj a)
    (hw : ∀ a, realizationWeakEquivalences (u a)) : realizationWeakEquivalences f := by
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.realization_weak_mono_pushout line 787
Source documentation
Cobase change preserves actual realization weak equivalences when the changed map is monomorphic. The realized deformation is glued explicitly.
```
theorem realization_weak_mono_pushout {A B X P : SSet.{0}}
    {i : A ⟶ B} {f : A ⟶ X} {b : B ⟶ P} {j : X ⟶ P}
    (sq : IsPushout i f b j) [Mono i] (hi : realizationWeakEquivalences i) :
    realizationWeakEquivalences j := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
instance OAI.Thomason.Construction.weakMonos_stableUnderCobaseChange line 797
Source documentation
This stability is proved directly from geometric realization, without identifying acyclic monomorphisms with anodyne extensions.
```
instance weakMonos_stableUnderCobaseChange :
    (MorphismProperty.monomorphisms SSet.{0} ⊓ realizationWeakEquivalences).IsStableUnderCobaseChange where
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
def OAI.Thomason.Construction.kanBaseChangeWeak line 824
Source documentation
Weak equivalence after every base change along an actual Kan fibration. This is a property to be proved for cells, not an extra main-theorem input.
```
def kanBaseChangeWeak : MorphismProperty SSet.{0} := fun _ B i =>
…
```
theorem OAI.Thomason.Construction.kanBaseChangeWeak.of_isPullback line 830
Source documentation
The canonical pullback formulation also applies to any specified cartesian square, retaining its original upper map.
```
theorem kanBaseChangeWeak.of_isPullback {A B A' B' : SSet.{0}}
    {i : A ⟶ B} {i' : A' ⟶ B'} {a : A' ⟶ A} {p : B' ⟶ B}
    (hi : kanBaseChangeWeak i) [HomotopicalAlgebra.Fibration p]
    (h : IsPullback i' a p i) : realizationWeakEquivalences i' := by
…
```
Mentions: OAI.Thomason.Construction.kanBaseChangeWeak, OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.horn_kanBaseChangeWeak line 839
Source documentation
Every generating horn satisfies the Kan base-change test.
```
theorem horn_kanBaseChangeWeak (n : ℕ) (i : Fin (n+2)) :
    kanBaseChangeWeak (Λ[n+1, i] : SSet.Subcomplex (Δ[n+1] : SSet.{0})).ι := by
…
```
Mentions: OAI.Thomason.Construction.kanBaseChangeWeak
theorem OAI.Thomason.Construction.kanBaseChangeWeak_pushout line 848
Source documentation
Pulling back a monic pushout gives a pushout. The weak upper attaching map is obtained by testing the original cell along the restricted Kan fibration, then the proved geometric gluing theorem applies.
```
theorem kanBaseChangeWeak_pushout {A B C D : SSet.{0}}
    {i : A ⟶ B} {f : A ⟶ C} {b : B ⟶ D} {j : C ⟶ D}
    (sq : IsPushout i f b j) [Mono i] (hi : kanBaseChangeWeak i) :
    kanBaseChangeWeak j := by
…
```
Mentions: OAI.Thomason.Construction.kanBaseChangeWeak
theorem OAI.Thomason.Construction.horn_attachment_kanBaseChangeWeak line 864
Source documentation
In particular, any single horn attachment remains a weak equivalence under arbitrary Kan base change.
```
theorem horn_attachment_kanBaseChangeWeak {C D : SSet.{0}} (n : ℕ) (k : Fin (n+2))
    {f : (Λ[n+1, k] : SSet.{0}) ⟶ C} {b : (Δ[n+1] : SSet.{0}) ⟶ D}
    {j : C ⟶ D}
    (sq : IsPushout (Λ[n+1, k] : SSet.Subcomplex _).ι f b j) :
    kanBaseChangeWeak j := kanBaseChangeWeak_pushout sq (horn_kanBaseChangeWeak n k)
```
Mentions: OAI.Thomason.Construction.kanBaseChangeWeak, OAI.Thomason.Construction.kanBaseChangeWeak_pushout, OAI.Thomason.Construction.horn_kanBaseChangeWeak
theorem OAI.Thomason.Construction.kanBaseChangeWeak_comp line 871
Source documentation
The cell property composes, using the exact iterated-pullback isomorphism.
```
theorem kanBaseChangeWeak_comp {A B C : SSet.{0}} {i : A ⟶ B} {j : B ⟶ C}
    (hi : kanBaseChangeWeak i) (hj : kanBaseChangeWeak j) : kanBaseChangeWeak (i ≫ j) := by
…
```
Mentions: OAI.Thomason.Construction.kanBaseChangeWeak
theorem OAI.Thomason.Construction.kanBaseChangeWeak_sigma line 900
Source documentation
Arbitrary coproducts preserve the actual Kan base-change weak test. Each restricted upper map is the base change of its original component.
```
theorem kanBaseChangeWeak_sigma {α : Type} {A B : α → SSet.{0}}
    (i : ∀ a, A a ⟶ B a) (hi : ∀ a, kanBaseChangeWeak (i a)) :
    kanBaseChangeWeak (CategoryTheory.Limits.Sigma.map i) := by
…
```
Mentions: OAI.Thomason.Construction.kanBaseChangeWeak

theorem OAI.Thomason.Construction.subcomplex_preimage_isPullback line 954

Source documentation

Inverse image of a subcomplex is the actual categorical pullback.

theorem subcomplex_preimage_isPullback {X E : SSet.{0}} (A : X.Subcomplex) (p : E ⟶ X) :
    IsPullback (A.preimage p).ι (A.fromPreimage p) p A.ι := by
…

theorem OAI.Thomason.Construction.subcomplex_fromPreimage_fibration line 970

Source documentation

Restricting a Kan fibration to an actual subcomplex is still Kan.

theorem subcomplex_fromPreimage_fibration {X E : SSet.{0}}
    (A : X.Subcomplex) (p : E ⟶ X) [HomotopicalAlgebra.Fibration p] :
    HomotopicalAlgebra.Fibration (A.fromPreimage p) := by
…

theorem OAI.Thomason.Construction.subcomplex_preimage_inclusion_isPullback line 978

Source documentation

Preimages of an inclusion form the required comparison pullback.

theorem subcomplex_preimage_inclusion_isPullback {X E : SSet.{0}}
    {A B : X.Subcomplex} (h : A ≤ B) (p : E ⟶ X) :
    IsPullback (SSet.Subcomplex.homOfLE (SSet.Subcomplex.preimage_monotone p h))
      (A.fromPreimage p) (B.fromPreimage p) (SSet.Subcomplex.homOfLE h) := by
…

theorem OAI.Thomason.Construction.kanBaseChangeWeak_exhaustion line 988
Source documentation
An increasing union of subcomplexes passes the actual Kan base-change weak-equivalence test once the initial-to-stage comparisons do. Compact cubes and relative homotopies justify the passage to the union.
```
theorem kanBaseChangeWeak_exhaustion {X : SSet.{0}} (A : ℕ → X.Subcomplex)
    (hA : Monotone A) (hcover : iSup A = ⊤)
    (hW : ∀ n, kanBaseChangeWeak (SSet.Subcomplex.homOfLE (hA (Nat.zero_le n)))) :
    kanBaseChangeWeak (A 0).ι := by
…
```
Mentions: OAI.Thomason.Construction.kanBaseChangeWeak