RealizationSubcomplexSemantics.lean`

60 declarations, 0 contain sorry, 0 declared as axioms

Barycentric coordinates on the actual realization of a horn

abbrev OAI.Thomason.Construction.HornBarycentric.simplexOrder line 21
theorem OAI.Thomason.Construction.HornBarycentric.simplexOrder_omits line 26
theorem OAI.Thomason.Construction.HornBarycentric.simplexOrder_naturality line 33
theorem OAI.Thomason.Construction.HornBarycentric.simplexPoint_mem line 41
Source documentation
Coordinates of a point in any original simplex lie in the geometric horn.
```
theorem simplexPoint_mem {n : ℕ} (i : Fin (n+2))
    (s : CostructuredArrow SSet.stdSimplex (Λ[n+1, i] : SSet.{0}))
    (x : StdSimplex ℝ (Fin (s.left.len+1))) :
    StdSimplex.map (simplexOrder i s) x ∈ horn i := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.simplexOrder, OAI.Thomason.Construction.HornBarycentric.horn
def OAI.Thomason.Construction.HornBarycentric.simplexPoint line 53
Source documentation
Barycentric coordinates on one original realized simplex.
```
def simplexPoint {n : ℕ} (i : Fin (n+2))
    (s : CostructuredArrow SSet.stdSimplex (Λ[n+1, i] : SSet.{0})) :
    (RealizationPrism.diagram (Λ[n+1, i] : SSet.{0})).obj s ⟶ TopCat.of (horn i) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.diagram, OAI.Thomason.Construction.HornBarycentric.horn
theorem OAI.Thomason.Construction.HornBarycentric.simplexPoint_naturality line 60
def OAI.Thomason.Construction.HornBarycentric.fromRealization line 75
Source documentation
The actual geometric realization has canonical coordinates in the geometric horn.
```
def fromRealization {n : ℕ} (i : Fin (n+2)) :
    SSet.toTop.obj (Λ[n+1, i] : SSet.{0}) ⟶ TopCat.of (horn i) :=
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.horn
theorem OAI.Thomason.Construction.HornBarycentric.fromRealization_fac line 83
def OAI.Thomason.Construction.HornBarycentric.simplexToFace line 111
Source documentation
Every original horn simplex factors through any face it omits.
```
def simplexToFace {n : ℕ} (i : Fin (n+2))
    (s : CostructuredArrow SSet.stdSimplex (Λ[n+1, i] : SSet.{0}))
    (j : Fin (n+2)) (hj : j ≠ i) (hs : ∀ k, simplexOrder i s k ≠ j) :
    s ⟶ faceIndex i j hj :=
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.simplexOrder, OAI.Thomason.Construction.HornBarycentric.faceIndex
theorem OAI.Thomason.Construction.HornBarycentric.toRealization_simplexPoint line 127
Source documentation
Gluing the coordinates of an original simplex returns its realization leg.
```
theorem toRealization_simplexPoint {n : ℕ} (i : Fin (n+2))
    (s : CostructuredArrow SSet.stdSimplex (Λ[n+1, i] : SSet.{0}))
    (x : SimplexCategory.toTop.{0}.obj s.left) :
    toRealization i ((simplexPoint i s).hom x) =
      (RealizationPrism.leg (Λ[n+1, i] : SSet.{0}) s).hom x := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.toRealization, OAI.Thomason.Construction.HornBarycentric.simplexPoint, OAI.Thomason.Construction.RealizationPrism.leg
theorem OAI.Thomason.Construction.HornBarycentric.from_toRealization line 149
Source documentation
One inverse equation follows from the colimit universal property.
```
theorem from_toRealization {n : ℕ} (i : Fin (n+2)) :
    fromRealization i ≫ TopCat.ofHom (toRealization i) =
      𝟙 (SSet.toTop.obj (Λ[n+1, i] : SSet.{0})) := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.fromRealization, OAI.Thomason.Construction.HornBarycentric.toRealization
theorem OAI.Thomason.Construction.HornBarycentric.toRealization_from line 161
Source documentation
The other inverse equation holds on any zero-coordinate face.
```
theorem toRealization_from {n : ℕ} (i : Fin (n+2)) (x : horn i) :
    (fromRealization i).hom (toRealization i x) = x := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.horn, OAI.Thomason.Construction.HornBarycentric.fromRealization, OAI.Thomason.Construction.HornBarycentric.toRealization
def OAI.Thomason.Construction.HornBarycentric.homeomorph line 173
Source documentation
The homeomorphism uses the actual realization, with its original topology.
```
def homeomorph {n : ℕ} (i : Fin (n+2)) :
    SSet.toTop.obj (Λ[n+1, i] : SSet.{0}) ≃ₜ horn i where
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.horn
def OAI.Thomason.Construction.HornBarycentric.simplexHomeomorph line 200
Source documentation
Standard barycentric coordinates on the realization of a representable.
```
def simplexHomeomorph (n : ℕ) :
    SSet.toTop.obj (Δ[n] : SSet.{0}) ≃ₜ StdSimplex ℝ (Fin (n+1)) :=
…
```
theorem OAI.Thomason.Construction.HornBarycentric.simplex_factor line 206
Source documentation
An original simplex has its specified vertex map in the ambient simplex.
```
theorem simplex_factor {n : ℕ} (i : Fin (n+2))
    (s : CostructuredArrow SSet.stdSimplex (Λ[n+1, i] : SSet.{0})) :
    s.hom ≫ Λ[n+1, i].ι = SSet.stdSimplex.map (SimplexCategory.Hom.mk (simplexOrder i s)) := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.simplexOrder

theorem OAI.Thomason.Construction.HornBarycentric.ambient_leg line 214

Source documentation

The ambient realization coordinates agree on every original simplex leg.

theorem ambient_leg {n : ℕ} (i : Fin (n+2))
    (s : CostructuredArrow SSet.stdSimplex (Λ[n+1, i] : SSet.{0})) :
    RealizationPrism.leg (Λ[n+1, i] : SSet.{0}) s ≫ SSet.toTop.map Λ[n+1, i].ι ≫
      SSet.toTopSimplex.hom.app (.mk (n+1)) =
    SimplexCategory.toTop.map (SimplexCategory.Hom.mk (simplexOrder i s)) := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.HornBarycentric.simplexOrder

theorem OAI.Thomason.Construction.HornBarycentric.homeomorph_inclusion line 230
Source documentation
The horn homeomorphism sends the actual inclusion to the literal subset inclusion.
```
theorem homeomorph_inclusion {n : ℕ} (i : Fin (n+2))
    (x : SSet.toTop.obj (Λ[n+1, i] : SSet.{0})) :
    simplexHomeomorph (n+1) ((SSet.toTop.map Λ[n+1, i].ι).hom x) =
      (homeomorph i x).val := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.simplexHomeomorph, OAI.Thomason.Construction.HornBarycentric.homeomorph
def OAI.Thomason.Construction.HornBarycentric.realizedRetraction line 265
Source documentation
The actual continuous retraction from a realized simplex to its horn.
```
def realizedRetraction {n : ℕ} (i : Fin (n+2)) :
    C(SSet.toTop.obj (Δ[n+1] : SSet.{0}), SSet.toTop.obj (Λ[n+1, i] : SSet.{0})) where
…
```
theorem OAI.Thomason.Construction.HornBarycentric.realizedRetraction_left line 272
Source documentation
The retraction is an exact left inverse to the realized horn inclusion.
```
theorem realizedRetraction_left {n : ℕ} (i : Fin (n+2))
    (x : SSet.toTop.obj (Λ[n+1, i] : SSet.{0})) :
    realizedRetraction i ((SSet.toTop.map Λ[n+1, i].ι).hom x) = x := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.realizedRetraction
def OAI.Thomason.Construction.HornBarycentric.realizedDeformation line 285
Source documentation
The deformation is stationary on the entire realized horn, so it can be glued after arbitrary horn attachments.
```
def realizedDeformation {n : ℕ} (i : Fin (n+2)) :
    ((SSet.toTop.map Λ[n+1, i].ι).hom.comp (realizedRetraction i)).HomotopyRel
      (ContinuousMap.id _) (Set.range (SSet.toTop.map Λ[n+1, i].ι).hom) where
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.realizedRetraction
def OAI.Thomason.Construction.RealizationPrism.simplexCarrier line 335
Source documentation
The subcomplex generated by the restriction to the nonzero barycentric coordinates.
```
def simplexCarrier (K : SSet.{0}) {n : ℕ} (s : K.obj (.op (.mk n)))
    (x : StdSimplex ℝ (Fin (n+1))) : K.Subcomplex :=
…
```

theorem OAI.Thomason.Construction.RealizationPrism.simplexCarrier_naturality line 342

Source documentation

Degenerate operators may merge support vertices but preserve the generated carrier.

theorem simplexCarrier_naturality (K : SSet.{0}) {m n : ℕ}
    (f : Fin (m+1) →o Fin (n+1)) (s : K.obj (.op (.mk n)))
    (x : StdSimplex ℝ (Fin (m+1))) :
    simplexCarrier K (K.map (show SimplexCategory.mk m ⟶ .mk n from SimplexCategory.Hom.mk f).op s) x =
      simplexCarrier K s (StdSimplex.map f x) := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.simplexCarrier

def OAI.Thomason.Construction.RealizationPrism.carrierCocone line 373
Source documentation
The supported carriers are compatible with every simplex arrow.
```
def carrierCocone (K : SSet.{0}) : Cocone (diagram K ⋙ forget TopCat) where
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.diagram
def OAI.Thomason.Construction.RealizationPrism.carrier line 387
Source documentation
Every actual realization point has a well-defined supported simplex subcomplex.
```
def carrier (K : SSet.{0}) : SSet.toTop.obj K → K.Subcomplex :=
…
```
theorem OAI.Thomason.Construction.RealizationPrism.carrier_leg line 391
Source documentation
The intrinsic carrier is computed on any representative simplex.
```
theorem carrier_leg (K : SSet.{0}) (j : CostructuredArrow SSet.stdSimplex K)
    (p : (diagram K).obj j) :
    carrier K ((leg K j).hom p) = simplexCarrier K (SSet.yonedaEquiv j.hom) p.down :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.diagram, OAI.Thomason.Construction.RealizationPrism.carrier, OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.RealizationPrism.simplexCarrier
theorem OAI.Thomason.Construction.RealizationPrism.simplexCarrier_le line 414
abbrev OAI.Thomason.Construction.RealizationPrism.FaceIndex line 419
Source documentation
Only finitely many parameter simplices of dimension at most n are needed.
```
abbrev FaceIndex (n : ℕ) := Σ k : Fin (n+1), (SimplexCategory.mk k.val ⟶ .mk n)
```
theorem OAI.Thomason.Construction.RealizationPrism.supportLen_le line 421

theorem OAI.Thomason.Construction.RealizationPrism.simplexCarrier_le_iff line 428

Source documentation

The points carried by a subcomplex form a finite union of affine simplex images.

theorem simplexCarrier_le_iff (K : SSet.{0}) (A : K.Subcomplex) {n : ℕ}
    (s : K.obj (.op (.mk n))) (x : StdSimplex ℝ (Fin (n+1))) :
    simplexCarrier K s x ≤ A ↔
      ∃ i : FaceIndex n, K.map i.2.op s ∈ A.obj (.op (.mk i.1.val)) ∧
        x ∈ Set.range (StdSimplex.map i.2.toOrderHom) := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.simplexCarrier, OAI.Thomason.Construction.RealizationPrism.FaceIndex

theorem OAI.Thomason.Construction.RealizationPrism.simplexCarrier_isClosed line 448
Source documentation
The carrier condition is closed on each parameter simplex.
```
theorem simplexCarrier_isClosed (K : SSet.{0}) (A : K.Subcomplex) {n : ℕ}
    (s : K.obj (.op (.mk n))) :
    IsClosed (Set.ofPred (fun x : StdSimplex ℝ (Fin (n+1)) => simplexCarrier K s x ≤ A)) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.simplexCarrier
theorem OAI.Thomason.Construction.RealizationPrism.carrier_isClosed line 465
Source documentation
The intrinsic condition of lying in a subcomplex is closed in geometric realization.
```
theorem carrier_isClosed (K : SSet.{0}) (A : K.Subcomplex) :
    IsClosed (Set.ofPred (fun x : SSet.toTop.obj K => carrier K x ≤ A)) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.carrier
theorem OAI.Thomason.Construction.RealizationPrism.simplexCarrier_image line 494
theorem OAI.Thomason.Construction.RealizationPrism.carrier_image line 503
Source documentation
The supported carrier commutes with every simplicial map.
```
theorem carrier_image {K L : SSet.{0}} (f : K ⟶ L) (x : SSet.toTop.obj K) :
    carrier L ((SSet.toTop.map f).hom x) = (carrier K x).image f := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.carrier
theorem OAI.Thomason.Construction.RealizationPrism.carrier_inclusion_le line 514
Source documentation
A point of a realized subcomplex has its ambient carrier in that subcomplex.
```
theorem carrier_inclusion_le (K : SSet.{0}) (A : K.Subcomplex)
    (x : SSet.toTop.obj (A : SSet)) :
    carrier K ((SSet.toTop.map A.ι).hom x) ≤ A := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.carrier
def OAI.Thomason.Construction.RealizationPrism.supportedLift line 521
Source documentation
A supported simplex whose carrier lies in A lifts to an actual point of |A|.
```
def supportedLift (K : SSet.{0}) (A : K.Subcomplex) {n : ℕ}
    (s : K.obj (.op (.mk n))) (x : StdSimplex ℝ (Fin (n+1)))
    (h : simplexCarrier K s x ≤ A) : SSet.toTop.obj (A : SSet) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.simplexCarrier
theorem OAI.Thomason.Construction.RealizationPrism.supportedLift_inclusion line 532
Source documentation
The lift evaluates to the original simplex point, with its zero coordinates restored.
```
theorem supportedLift_inclusion (K : SSet.{0}) (A : K.Subcomplex) {n : ℕ}
    (s : K.obj (.op (.mk n))) (x : StdSimplex ℝ (Fin (n+1)))
    (h : simplexCarrier K s x ≤ A) :
    (SSet.toTop.map A.ι).hom (supportedLift K A s x h) =
      (leg K (CostructuredArrow.mk (SSet.yonedaEquiv.symm s))).hom (ULift.up x) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.simplexCarrier, OAI.Thomason.Construction.RealizationPrism.supportedLift, OAI.Thomason.Construction.RealizationPrism.leg
theorem OAI.Thomason.Construction.RealizationPrism.mem_range_inclusion_iff line 563
Source documentation
Membership in a realized subcomplex is exactly the intrinsic carrier condition.
```
theorem mem_range_inclusion_iff (K : SSet.{0}) (A : K.Subcomplex)
    (x : SSet.toTop.obj K) :
    x ∈ Set.range (SSet.toTop.map A.ι).hom ↔ carrier K x ≤ A := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.carrier
theorem OAI.Thomason.Construction.RealizationPrism.inclusion_isClosed_range line 585
Source documentation
Every simplicial subcomplex has closed image under actual geometric realization.
```
theorem inclusion_isClosed_range (K : SSet.{0}) (A : K.Subcomplex) :
    IsClosed (Set.range (SSet.toTop.map A.ι).hom) := by
…
```

theorem OAI.Thomason.Construction.RealizationPrism.supportedLift_naturality line 612

Source documentation

Supported lifts agree across arbitrary simplex operators, including degeneracies.

theorem supportedLift_naturality (K : SSet.{0}) (A : K.Subcomplex) {m n : ℕ}
    (f : SimplexCategory.mk m ⟶ .mk n) (s : K.obj (.op (.mk n)))
    (x : StdSimplex ℝ (Fin (m+1)))
    (h₁ : simplexCarrier K (K.map f.op s) x ≤ A)
    (h₂ : simplexCarrier K s (StdSimplex.map f.toOrderHom x) ≤ A) :
    supportedLift K A (K.map f.op s) x h₁ =
      supportedLift K A s (StdSimplex.map f.toOrderHom x) h₂ := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.simplexCarrier, OAI.Thomason.Construction.RealizationPrism.supportedLift

theorem OAI.Thomason.Construction.RealizationPrism.supportedLift_of_mem line 659
Source documentation
When the entire simplex is in the subcomplex, its lift is its original realization.
```
theorem supportedLift_of_mem (K : SSet.{0}) (A : K.Subcomplex) {n : ℕ}
    (s : (A : SSet).obj (.op (.mk n))) (x : StdSimplex ℝ (Fin (n+1)))
    (h : simplexCarrier K s.val x ≤ A) :
    supportedLift K A s.val x h =
      (leg (A : SSet) (CostructuredArrow.mk (SSet.yonedaEquiv.symm s))).hom (ULift.up x) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.simplexCarrier, OAI.Thomason.Construction.RealizationPrism.supportedLift, OAI.Thomason.Construction.RealizationPrism.leg

def OAI.Thomason.Construction.RealizationPrism.liftOrNone line 703

Source documentation

The partial lift of a simplex point, defined precisely when its carrier is in A.

def liftOrNone (K : SSet.{0}) (A : K.Subcomplex) {n : ℕ}
    (s : K.obj (.op (.mk n))) (x : StdSimplex ℝ (Fin (n+1))) :
    Option (SSet.toTop.obj (A : SSet)) :=
…

theorem OAI.Thomason.Construction.RealizationPrism.liftOrNone_naturality line 708
def OAI.Thomason.Construction.RealizationPrism.partialLiftCocone line 722
Source documentation
Partial lifts form a cocone of underlying sets; no continuity of the partial map is asserted.
```
def partialLiftCocone (K : SSet.{0}) (A : K.Subcomplex) :
    Cocone (diagram K ⋙ forget TopCat) where
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.diagram
def OAI.Thomason.Construction.RealizationPrism.partialLift line 738
Source documentation
A set-theoretic partial inverse to the realized inclusion.
```
def partialLift (K : SSet.{0}) (A : K.Subcomplex) :
    SSet.toTop.obj K → Option (SSet.toTop.obj (A : SSet)) :=
…
```
theorem OAI.Thomason.Construction.RealizationPrism.partialLift_leg line 743
theorem OAI.Thomason.Construction.RealizationPrism.partialLift_inclusion line 750
Source documentation
On points already in |A|, the partial inverse recovers the point itself.
```
theorem partialLift_inclusion (K : SSet.{0}) (A : K.Subcomplex)
    (x : SSet.toTop.obj (A : SSet)) :
    partialLift K A ((SSet.toTop.map A.ι).hom x) = some x := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.partialLift
theorem OAI.Thomason.Construction.RealizationPrism.inclusion_injective line 768
Source documentation
Geometric realization sends a simplicial subcomplex inclusion to an injective map.
```
theorem inclusion_injective (K : SSet.{0}) (A : K.Subcomplex) :
    Function.Injective (SSet.toTop.map A.ι).hom := by
…
```
theorem OAI.Thomason.Construction.RealizationPrism.carrier_simplexPoint line 791

def OAI.Thomason.Construction.RealizationPrism.faceSimplex line 801

Source documentation

A simplex of the subcomplex obtained by applying an ambient face operator.

def faceSimplex (K : SSet.{0}) (A : K.Subcomplex) {n : ℕ}
    (s : K.obj (.op (.mk n))) (i : FaceIndex n)
    (h : K.map i.2.op s ∈ A.obj (.op (.mk i.1.val))) :
    (A : SSet).obj (.op (.mk i.1.val)) := ⟨K.map i.2.op s, h⟩

Mentions: OAI.Thomason.Construction.RealizationPrism.FaceIndex

theorem OAI.Thomason.Construction.RealizationPrism.faceSimplex_inclusion line 806

theorem OAI.Thomason.Construction.RealizationPrism.simplexPoint_preimage_inclusion_image line 816

Source documentation

On a parameter simplex, the image of a subset of |A| is a finite union of face images.

theorem simplexPoint_preimage_inclusion_image (K : SSet.{0}) (A : K.Subcomplex)
    (B : Set (SSet.toTop.obj (A : SSet))) {n : ℕ} (s : K.obj (.op (.mk n))) :
    (simplexPoint K s) ⁻¹' ((SSet.toTop.map A.ι).hom '' B) =
      ⋃ i : {i : FaceIndex n // K.map i.2.op s ∈ A.obj (.op (.mk i.1.val))},
        (StdSimplex.map i.val.2.toOrderHom) ''
          ((simplexPoint (A : SSet) (faceSimplex K A s i.val i.property)) ⁻¹' B) := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.simplexPoint, OAI.Thomason.Construction.RealizationPrism.FaceIndex, OAI.Thomason.Construction.RealizationPrism.faceSimplex

theorem OAI.Thomason.Construction.RealizationPrism.inclusion_isClosedMap line 842
Source documentation
Realization of a subcomplex inclusion is a closed map.
```
theorem inclusion_isClosedMap (K : SSet.{0}) (A : K.Subcomplex) :
    IsClosedMap (SSet.toTop.map A.ι).hom := by
…
```
theorem OAI.Thomason.Construction.RealizationPrism.inclusion_isClosedEmbedding line 872
Source documentation
The actual topological map induced by a simplicial subcomplex is a closed embedding.
```
theorem inclusion_isClosedEmbedding (K : SSet.{0}) (A : K.Subcomplex) :
    IsClosedEmbedding (SSet.toTop.map A.ι).hom :=
…
```
def OAI.Thomason.Construction.RealizationPrism.carrierHomeomorph line 895
Source documentation
The realization of a subcomplex is its intrinsic carrier subspace, homeomorphically.
```
def carrierHomeomorph (K : SSet.{0}) (A : K.Subcomplex) :
    SSet.toTop.obj (A : SSet) ≃ₜ Set.ofPred (fun x : SSet.toTop.obj K => carrier K x ≤ A) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.carrier
def OAI.Thomason.Construction.RealizationPrism.carrierInclusion line 900
theorem OAI.Thomason.Construction.RealizationPrism.carrierHomeomorph_inclusion line 904
theorem OAI.Thomason.Construction.RealizationPrism.inclusion_weak_iff_carrier line 912
Source documentation
The Kan–Quillen realization test of an actual subcomplex inclusion is exactly the weak homotopy test of the corresponding intrinsic closed subspace.
```
theorem inclusion_weak_iff_carrier (K : SSet.{0}) (A : K.Subcomplex) :
    realizationWeakEquivalences A.ι ↔ IsWeakHomotopyEquivalence (carrierInclusion K A) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.RealizationPrism.carrierInclusion

theorem OAI.Thomason.Construction.RealizationPrism.range_preimage_inclusion line 920

Source documentation

Realization commutes with the underlying sets of inverse images of subcomplexes.

theorem range_preimage_inclusion {K L : SSet.{0}} (f : K ⟶ L) (A : L.Subcomplex) :
    Set.range (SSet.toTop.map (A.preimage f).ι).hom =
      (SSet.toTop.map f).hom ⁻¹' Set.range (SSet.toTop.map A.ι).hom := by
…

def OAI.Thomason.Construction.RealizationPrism.preimageHomeomorph line 928

Source documentation

The inverse-image subcomplex realizes to the actual topological inverse-image subspace.

def preimageHomeomorph {K L : SSet.{0}} (f : K ⟶ L) (A : L.Subcomplex) :
    SSet.toTop.obj (A.preimage f : SSet) ≃ₜ
      ((SSet.toTop.map f).hom ⁻¹' Set.range (SSet.toTop.map A.ι).hom) :=
…

theorem OAI.Thomason.Construction.RealizationPrism.fromPreimage_commutes line 935

Source documentation

Both projections of the inverse-image square are the actual realized maps.

theorem fromPreimage_commutes {K L : SSet.{0}} (f : K ⟶ L) (A : L.Subcomplex) :
    SSet.toTop.map (A.fromPreimage f) ≫ SSet.toTop.map A.ι =
      SSet.toTop.map (A.preimage f).ι ≫ SSet.toTop.map f := by
…