CanonicalExtensionCartesian.lean`

90 declarations, 0 contain sorry, 0 declared as axioms

Naturality of the nondegenerate face-poset comparison

A simplicial map preserving nondegenerate simplices induces a dimension-preserving map of face posets. Uniqueness of face inclusions makes the comparison to the original simplicial set strictly natural.

def OAI.Thomason.Construction.NonsingularLastVertex.PreservesNondegenerate line 35
Source documentation
The hypothesis records preservation of dimension, rather than choosing new nondegenerate representatives of possibly degenerate images.
```
def PreservesNondegenerate (f : X ⟶ Y) : Prop :=
…
```
theorem OAI.Thomason.Construction.NonsingularLastVertex.preservesNondegenerate_of_mono line 39
def OAI.Thomason.Construction.NonsingularLastVertex.faceMap line 42
theorem OAI.Thomason.Construction.NonsingularLastVertex.faceMap_dim line 52
theorem OAI.Thomason.Construction.NonsingularLastVertex.faceMap_simplex line 56
theorem OAI.Thomason.Construction.NonsingularLastVertex.faceMap_monoOfLE line 62
Source documentation
The same ordinal inclusion represents a face before and after the map.
```
theorem faceMap_monoOfLE (f : X ⟶ Y) (hf : PreservesNondegenerate f)
    {x y : X.N} (h : x ≤ y) :
    SSet.N.monoOfLE ((faceMap f hf).monotone h) = SSet.N.monoOfLE (X := X) h := by
…
```
Mentions: OAI.Thomason.Construction.NonsingularLastVertex.PreservesNondegenerate, OAI.Thomason.Construction.NonsingularLastVertex.faceMap
theorem OAI.Thomason.Construction.NonsingularLastVertex.faceMap_ordinal line 73
theorem OAI.Thomason.Construction.NonsingularLastVertex.map_naturality line 86
Source documentation
Naturality has the original simplicial maps on the bottom edge.
```
theorem map_naturality (f : X ⟶ Y) (hf : PreservesNondegenerate f) :
    nerveMap (faceMap f hf).monotone.functor ≫ map Y = map X ≫ f := by
…
```
Mentions: OAI.Thomason.Construction.NonsingularLastVertex.PreservesNondegenerate, OAI.Thomason.Construction.NonsingularLastVertex.faceMap, OAI.Thomason.Construction.NonsingularLastVertex.map
theorem OAI.Thomason.Construction.FaceSimplexResolution.nondegenerate_of_dimension_strictMono line 122
Source documentation
Strictly increasing dimensions exclude every actual simplicial degeneracy, without assuming the face category is thin.
```
theorem nondegenerate_of_dimension_strictMono {X : SSet.{0}} {n : ℕ}
    (s : (nerve (Face X)) _⦋n⦌)
    (hs : StrictMono (fun i => dimension (s.obj i))) :
    s ∈ (nerve (Face X)).nonDegenerate n := by
…
```
Mentions: OAI.Thomason.Construction.FaceSimplexResolution.Face, OAI.Thomason.Construction.FaceSimplexResolution.dimension
theorem OAI.Thomason.Construction.FaceSimplexResolution.nondegenerate_iff_dimension_strictMono line 138
theorem OAI.Thomason.Construction.FaceSimplexResolution.map_preservesNondegenerate line 146
Source documentation
Every map of face resolutions preserves nondegenerate simplices, even when the underlying simplicial map does not.
```
theorem map_preservesNondegenerate {X Y : SSet.{0}} (f : X ⟶ Y) :
    NonsingularLastVertex.PreservesNondegenerate (functor.map f) := by
…
```
Mentions: OAI.Thomason.Construction.NonsingularLastVertex.PreservesNondegenerate
theorem OAI.Thomason.Construction.FaceSimplexResolution.nondegenerateLift_preservesNondegenerate line 153
Source documentation
The lift of nondegenerate face flags also preserves their dimensions.
```
theorem nondegenerateLift_preservesNondegenerate (X : SSet.{0}) [X.Nonsingular] :
    NonsingularLastVertex.PreservesNondegenerate (nondegenerateLift X) := by
…
```
Mentions: OAI.Thomason.Construction.NonsingularLastVertex.PreservesNondegenerate, OAI.Thomason.Construction.FaceSimplexResolution.nondegenerateLift
theorem OAI.Thomason.Construction.FaceSimplexResolution.resolvedMap_preservesNondegenerate line 163
Source documentation
Resolving any map out of a nonsingular source retains the dimension of every nondegenerate source flag.
```
theorem resolvedMap_preservesNondegenerate {A X : SSet.{0}} [A.Nonsingular]
    (a : A ⟶ X) : NonsingularLastVertex.PreservesNondegenerate (resolvedMap a) := by
…
```
Mentions: OAI.Thomason.Construction.NonsingularLastVertex.PreservesNondegenerate, OAI.Thomason.Construction.FaceSimplexResolution.resolvedMap
theorem OAI.Thomason.Construction.FaceSimplexResolution.resolvedMap_factor_preservesNondegenerate line 170
Source documentation
A factorization of the resolved boundary still preserves nondegenerate simplices, independently of which finite target contains it.
```
theorem resolvedMap_factor_preservesNondegenerate {A X S : SSet.{0}} [A.Nonsingular]
    (a : A ⟶ X) (a' : nerve A.N ⟶ S) (j : S ⟶ functor.obj X)
    (h : a' ≫ j = resolvedMap a) : NonsingularLastVertex.PreservesNondegenerate a' := by
…
```
Mentions: OAI.Thomason.Construction.FaceSimplexResolution.resolvedMap, OAI.Thomason.Construction.NonsingularLastVertex.PreservesNondegenerate
def OAI.Thomason.Construction.FaceSimplexResolution.mapFaceFunctor line 180
Source documentation
The actual map of face-simplex categories underlying the resolution.
```
def mapFaceFunctor {X Y : SSet.{0}} (f : X ⟶ Y) : Face X ⥤ Face Y :=
…
```
Mentions: OAI.Thomason.Construction.FaceSimplexResolution.Face
theorem OAI.Thomason.Construction.FaceSimplexResolution.mapFaceFunctor_nerveMap line 183
theorem OAI.Thomason.Construction.FaceSimplexResolution.nondegenerateFaceFunctor_naturality line 188
Source documentation
The chosen nondegenerate face lift is natural on every map preserving nondegenerate simplices; the bottom map is the actual face resolution.
```
theorem nondegenerateFaceFunctor_naturality {X Y : SSet.{0}}
    [X.Nonsingular] [Y.Nonsingular] (f : X ⟶ Y)
    (hf : NonsingularLastVertex.PreservesNondegenerate f) :
    (NonsingularLastVertex.faceMap f hf).monotone.functor ⋙ nondegenerateFaceFunctor Y =
      nondegenerateFaceFunctor X ⋙ mapFaceFunctor f := by
…
```
Mentions: OAI.Thomason.Construction.NonsingularLastVertex.PreservesNondegenerate, OAI.Thomason.Construction.NonsingularLastVertex.faceMap, OAI.Thomason.Construction.FaceSimplexResolution.nondegenerateFaceFunctor, OAI.Thomason.Construction.FaceSimplexResolution.mapFaceFunctor
theorem OAI.Thomason.Construction.FaceSimplexResolution.nondegenerateLift_naturality line 211
structure OAI.Thomason.Construction.SieveRetraction line 244
Source documentation
A downward-closed full subposet whose inclusion has a right adjoint.
```
structure SieveRetraction (A : Set E) where
…
```
theorem OAI.Thomason.Construction.SieveRetraction.rightAdjoint_le line 253
theorem OAI.Thomason.Construction.SieveRetraction.rightAdjoint_coe line 257
def OAI.Thomason.Construction.SieveRetraction.projection line 263
Source documentation
The associated idempotent endomorphism of the ambient poset.
```
def projection : E →o E :=
…
```
theorem OAI.Thomason.Construction.SieveRetraction.projection_apply line 268
theorem OAI.Thomason.Construction.SieveRetraction.projection_mem line 270
theorem OAI.Thomason.Construction.SieveRetraction.projection_of_mem line 273
theorem OAI.Thomason.Construction.SieveRetraction.projection_idempotent line 277
structure OAI.Thomason.Construction.SieveRetraction.GreatestNew line 282
Source documentation
A greatest element of the new part of the poset. It need not be greatest in the whole poset: old objects can lie above neither it nor the new part.
```
structure GreatestNew (x : E) : Prop where
…
```
theorem OAI.Thomason.Construction.SieveRetraction.old_le_retracted_greatest line 289
def OAI.Thomason.Construction.SieveRetraction.replaceNew line 295
Source documentation
Fix the old subposet and send every new element to a fixed value.
```
noncomputable def replaceNew (c : E)
    (hc : ∀ a e, a ∈ A → e ∉ A → a ≤ e → a ≤ c) : E →o E := by
…
```
theorem OAI.Thomason.Construction.SieveRetraction.replaceNew_old line 308
theorem OAI.Thomason.Construction.SieveRetraction.replaceNew_new line 315
def OAI.Thomason.Construction.SieveRetraction.upperCollapse line 322
Source documentation
The common upper endpoint g in the local zigzag.
```
noncomputable def upperCollapse : E →o E :=
…
```
def OAI.Thomason.Construction.SieveRetraction.oldCollapse line 326
Source documentation
The old-valued endpoint k in the local zigzag.
```
noncomputable def oldCollapse : E →o E :=
…
```
theorem OAI.Thomason.Construction.SieveRetraction.identity_le_upperCollapse line 330
theorem OAI.Thomason.Construction.SieveRetraction.oldCollapse_le_upperCollapse line 336
theorem OAI.Thomason.Construction.SieveRetraction.upperCollapse_old line 343
theorem OAI.Thomason.Construction.SieveRetraction.oldCollapse_old line 346
theorem OAI.Thomason.Construction.SieveRetraction.upperCollapse_new line 349
theorem OAI.Thomason.Construction.SieveRetraction.oldCollapse_mem line 352
def OAI.Thomason.Construction.SieveRetraction.oldCollapseRetraction line 359
Source documentation
The endpoint k factors through the old subposet as a retraction.
```
noncomputable def oldCollapseRetraction : E →o A :=
…
```
theorem OAI.Thomason.Construction.SieveRetraction.oldCollapseRetraction_coe line 364

theorem OAI.Thomason.Construction.SieveRetraction.local_zigzag line 371

Source documentation

The exact order-theoretic hypotheses of the two relative prisms in Lemma greatest-new: id ≤ g ≥ k, fixed on the old part, with g constant on the new part and k factoring through a retraction to the old part.

theorem local_zigzag :
    (∀ e, e ≤ R.upperCollapse hx e) ∧
    (∀ e, R.oldCollapse hx e ≤ R.upperCollapse hx e) ∧
    (∀ a, a ∈ A → R.upperCollapse hx a = a ∧ R.oldCollapse hx a = a) ∧
    (∀ e, e ∉ A → R.upperCollapse hx e = x) ∧
    (∀ a : A, R.oldCollapseRetraction hx a = a) :=
…

def OAI.Thomason.Construction.SieveRetraction.stableClosure line 386
Source documentation
Add retraction images once; idempotence makes this stable already.
```
def stableClosure (s : Finset E) : Finset E := s ∪ s.image R.projection
```
theorem OAI.Thomason.Construction.SieveRetraction.subset_stableClosure line 388
theorem OAI.Thomason.Construction.SieveRetraction.stableClosure_stable line 391
def OAI.Thomason.Construction.SieveRetraction.Stable line 399
theorem OAI.Thomason.Construction.SieveRetraction.stable_union line 401
theorem OAI.Thomason.Construction.SieveRetraction.finite_stable_superset line 409
Source documentation
Every finite subset lies in a finite retraction-stable full subposet.
```
theorem finite_stable_superset (s : Finset E) :
    ∃ t : Finset E, s ⊆ t ∧ R.Stable t :=
…
```
theorem OAI.Thomason.Construction.SieveRetraction.stable_directed line 415
Source documentation
The stable finite supports form a directed system under inclusion.
```
theorem stable_directed (s t : Finset E) (hs : R.Stable s) (ht : R.Stable t) :
    ∃ q : Finset E, R.Stable q ∧ s ⊆ q ∧ t ⊆ q :=
…
```
def OAI.Thomason.Construction.SieveRetraction.restrictToStable line 420
Source documentation
Restrict to a stable finite full subposet. It need not be a sieve in E.
```
def restrictToStable (s : Finset E) (hs : R.Stable s) :
    SieveRetraction {e : {e : E // e ∈ s} | (e : E) ∈ A} where
…
```
Mentions: OAI.Thomason.Construction.SieveRetraction
abbrev OAI.Thomason.Construction.SimplicialHomotopyDescent.diagram line 451
abbrev OAI.Thomason.Construction.SimplicialHomotopyDescent.cocone line 453
def OAI.Thomason.Construction.SimplicialHomotopyDescent.isColimit line 456
def OAI.Thomason.Construction.SimplicialHomotopyDescent.prismCocone line 462
def OAI.Thomason.Construction.SimplicialHomotopyDescent.assemble line 473
theorem OAI.Thomason.Construction.SimplicialHomotopyDescent.assemble_fac line 482
def OAI.Thomason.Construction.SimplicialHomotopyDescent.homotopy line 491
theorem OAI.Thomason.Construction.map_iff_of_weak_coaugmentation line 557
Source documentation
Naturality of an objectwise weak equivalence from the identity proves that its target endofunctor preserves and reflects weak equivalences.
```
theorem map_iff_of_weak_coaugmentation (j : 𝟭 C ⟶ F)
    (hj : ∀ X, W (j.app X)) {X Y : C} (f : X ⟶ Y) :
    W (F.map f) ↔ W f := by
…
```
theorem OAI.Thomason.Construction.map_iff_of_weak_augmentation line 572
Source documentation
The analogous argument for a weak equivalence to the identity.
```
theorem map_iff_of_weak_augmentation (e : F ⟶ 𝟭 C)
    (he : ∀ X, W (e.app X)) {X Y : C} (f : X ⟶ Y) :
    W (F.map f) ↔ W f := by
…
```
def OAI.Thomason.Construction.extensionCoaugmentation line 595
Source documentation
The mate of a last-vertex transformation under the actual subdivision adjunction. Its components are the canonical maps to extension; their being weak equivalences remains a separate published input.
```
noncomputable def extensionCoaugmentation
    (e : SSet.sd.{u} ⟶ 𝟭 SSet.{u}) : 𝟭 SSet.{u} ⟶ SSet.ex where
…
```
def OAI.Thomason.Construction.canonicalExtension line 603
Source documentation
The canonical extension map, obtained from the actual last-vertex map.
```
noncomputable def canonicalExtension : 𝟭 SSet.{u} ⟶ SSet.ex :=
…
```
theorem OAI.Thomason.Construction.canonicalExtension_eq line 607
Source documentation
Taking mates identifies the two canonical extension transformations.
```
theorem canonicalExtension_eq :
    canonicalExtension.{u} = Thomason.Subdivision.exComparison := by
…
```
Mentions: OAI.Thomason.Subdivision.exComparison

theorem OAI.Thomason.Construction.ex_map_iff line 616

Source documentation

Goerss--Jardine III.4.6 implies that Ex preserves and reflects W.

theorem ex_map_iff (j : 𝟭 SSet.{u} ⟶ SSet.ex) (hj : ∀ X, W (j.app X))
    {X Y : SSet.{u}} (f : X ⟶ Y) : W (SSet.ex.map f) ↔ W f :=
…

theorem OAI.Thomason.Construction.sd_map_iff line 621

Source documentation

The last-vertex weak equivalence implies the analogous statement for Sd.

theorem sd_map_iff (e : SSet.sd.{u} ⟶ 𝟭 SSet.{u}) (he : ∀ X, W (e.app X))
    {X Y : SSet.{u}} (f : X ⟶ Y) : W (SSet.sd.map f) ↔ W f :=
…

theorem OAI.Thomason.Construction.ex_twice_map_iff line 626

Source documentation

In particular two extensions do not change the detected weak equivalences.

theorem ex_twice_map_iff (j : 𝟭 SSet.{u} ⟶ SSet.ex) (hj : ∀ X, W (j.app X))
    {X Y : SSet.{u}} (f : X ⟶ Y) :
    W ((SSet.ex ⋙ SSet.ex).map f) ↔ W f :=
…

theorem OAI.Thomason.Construction.sd_twice_map_iff line 632

Source documentation

Likewise two subdivisions preserve and reflect weak equivalences.

theorem sd_twice_map_iff (e : SSet.sd.{u} ⟶ 𝟭 SSet.{u}) (he : ∀ X, W (e.app X))
    {X Y : SSet.{u}} (f : X ⟶ Y) :
    W ((SSet.sd ⋙ SSet.sd).map f) ↔ W f :=
…

theorem OAI.Thomason.Construction.nerve_weak_equivalences_eq line 641
Source documentation
The equality N⁻¹ W = (Ex² N)⁻¹ W used to prescribe the Thomason weak equivalences. This applies to any actual nerve functor N.
```
theorem nerve_weak_equivalences_eq (N : D ⥤ SSet.{u})
    (j : 𝟭 SSet.{u} ⟶ SSet.ex) (hj : ∀ X, W (j.app X)) :
    W.inverseImage N = W.inverseImage (N ⋙ SSet.ex ⋙ SSet.ex) := by
…
```
theorem OAI.Thomason.Construction.nerve_weak_equivalences_eq_of_last_vertex line 650
Source documentation
The same weak-equivalence identification with the extension map explicitly constructed as the mate of the last-vertex map.
```
theorem nerve_weak_equivalences_eq_of_last_vertex (N : D ⥤ SSet.{u})
    (e : SSet.sd.{u} ⟶ 𝟭 SSet.{u})
    (hj : ∀ X, W ((extensionCoaugmentation e).app X)) :
    W.inverseImage N = W.inverseImage (N ⋙ SSet.ex ⋙ SSet.ex) :=
…
```
Mentions: OAI.Thomason.Construction.extensionCoaugmentation
theorem OAI.Thomason.Construction.canonical_nerve_weak_equivalences_eq line 659
Source documentation
The precise specialization used for the Thomason model classes. The only subdivision/extension input is the published weak-equivalence property of the canonical map to Ex.
```
theorem canonical_nerve_weak_equivalences_eq (N : D ⥤ SSet.{u})
    (hj : ∀ X, W (canonicalExtension.app X)) :
    W.inverseImage N = W.inverseImage (N ⋙ SSet.ex ⋙ SSet.ex) :=
…
```

theorem OAI.Thomason.Construction.canonicalExtension_fac line 665

Source documentation

The mate identity used in the Quillen-equivalence argument.

theorem canonicalExtension_fac (X : SSet.{u}) :
    canonicalExtension.app X = SSet.sdExAdjunction.unit.app X ≫
      SSet.ex.map (lastVertex.app X) :=
…

theorem OAI.Thomason.Construction.subdivision_unit_weak_equivalence line 672
Source documentation
The published weak-equivalence properties of last vertex and extension imply that the unit of subdivision-extension is a weak equivalence.
```
theorem subdivision_unit_weak_equivalence
    (he : ∀ X, W (lastVertex.app X))
    (hj : ∀ X, W (canonicalExtension.app X)) (X : SSet.{u}) :
    W (SSet.sdExAdjunction.unit.app X) := by
…
```

theorem OAI.Thomason.Construction.subdivision_twice_unit_weak_equivalence line 682

Source documentation

The unit for two subdivisions and two extensions is also a weak equivalence.

theorem subdivision_twice_unit_weak_equivalence
    (he : ∀ X, W (lastVertex.app X))
    (hj : ∀ X, W (canonicalExtension.app X)) (X : SSet.{u}) :
    W ((SSet.sdExAdjunction.comp SSet.sdExAdjunction).unit.app X) := by
…

theorem OAI.Thomason.Construction.adjunct_weak_equivalence_iff line 702
Source documentation
The weak-equivalence calculation underlying the Quillen-equivalence criterion: if the unit is weak, an adjunct is weak exactly when its image under the right adjoint is weak.
```
theorem adjunct_weak_equivalence_iff (hu : ∀ X, W (adj.unit.app X))
    {X : C} {Y : D} (f : L.obj X ⟶ Y) :
    W (adj.homEquiv X Y f) ↔ W (R.map f) := by
…
```
def OAI.Thomason.Construction.initialVertexChain line 732
Source documentation
The initial segment ending at a vertex of a finite ordered simplex.
```
def initialVertexChain {n : ℕ} (i : ULift.{u} (Fin (n + 1))) :
    NonemptyFiniteChains (ULift.{u} (Fin (n + 1))) where
…
```
theorem OAI.Thomason.Construction.initialVertexChain_monotone line 738
def OAI.Thomason.Construction.initialVertexChainHom line 745
Source documentation
Initial segments form a monotone section of the maximum operation.
```
def initialVertexChainHom (n : ℕ) : ULift.{u} (Fin (n + 1)) →o
    NonemptyFiniteChains (ULift.{u} (Fin (n + 1))) :=
…
```
theorem OAI.Thomason.Construction.chainMaximum_initialVertexChain line 749

def OAI.Thomason.Construction.simplexInitialVertexChain line 758

Source documentation

A degreewise section, not claimed to be natural in the ordinal.

def simplexInitialVertexChain (n : SimplexCategory) :
    SimplexCategory.toPartOrd.{u}.obj n ⟶
      (SimplexCategory.toPartOrd.{u} ⋙ PartOrd.nonemptyFiniteChainsFunctor).obj n :=
…

theorem OAI.Thomason.Construction.simplexInitialVertexChain_fac line 763
def OAI.Thomason.Construction.simplexLastVertexSection line 770
Source documentation
The section on the nerve of each ordinal.
```
def simplexLastVertexSection (n : SimplexCategory) :
    SSet.stdSimplex.{u}.obj n ⟶ SimplexCategory.sd.obj n :=
…
```
theorem OAI.Thomason.Construction.simplexLastVertexSection_fac line 775
def OAI.Thomason.Construction.lastVertexStandardSection line 794
Source documentation
Last vertex is split surjective on every standard simplex.
```
def lastVertexStandardSection (n : SimplexCategory) :
    SSet.stdSimplex.{u}.obj n ⟶ SSet.sd.obj (SSet.stdSimplex.obj n) :=
…
```
theorem OAI.Thomason.Construction.lastVertexStandardSection_fac line 798
theorem OAI.Thomason.Construction.lastVertex_standard_epi line 803

theorem OAI.Thomason.Construction.canonicalExtension_simplex line 809

Source documentation

The adjoint of j_X after a standard simplex is precisely the last-vertex map followed by that simplex.

theorem canonicalExtension_simplex (X : SSet.{u}) (n : SimplexCategory)
    (f : SSet.stdSimplex.obj n ⟶ X) :
    f ≫ canonicalExtension.app X = SSet.sdExAdjunction.homEquiv _ _
      (lastVertex.app (SSet.stdSimplex.obj n) ≫ f) := by
…

theorem OAI.Thomason.Construction.canonicalExtension_mono line 821
Source documentation
The canonical extension map is an actual monomorphism in every degree.
```
theorem canonicalExtension_mono (X : SSet.{u}) : Mono (canonicalExtension.app X) := by
…
```

theorem OAI.Thomason.Construction.canonicalExtension_simplex_lift line 861

Source documentation

A simplex of an extension lying over an original simplex has a unique original lift along a monomorphism.

theorem canonicalExtension_simplex_lift {A B : SSet.{u}} (i : A ⟶ B) [Mono i]
    (n : SimplexCategory) (x : SSet.stdSimplex.obj n ⟶ B)
    (a : SSet.stdSimplex.obj n ⟶ SSet.ex.obj A)
    (h : x ≫ canonicalExtension.app B = a ≫ SSet.ex.map i) :
    ∃ b : SSet.stdSimplex.obj n ⟶ A,
      b ≫ i = x ∧ b ≫ canonicalExtension.app A = a := by
…

theorem OAI.Thomason.Construction.canonicalExtension_isPullback line 895
Source documentation
Naturality of the actual canonical extension is a pullback along every monomorphism of simplicial sets.
```
theorem canonicalExtension_isPullback {A B : SSet.{u}} (i : A ⟶ B) [Mono i] :
    IsPullback i (canonicalExtension.app A) (canonicalExtension.app B) (SSet.ex.map i) := by
…
```

theorem OAI.Thomason.Construction.preimage_range_of_isPullback line 916

Source documentation

A pullback square identifies the preimage of the bottom map's range with the range of its top map.

theorem preimage_range_of_isPullback {W X Y Z : SSet.{u}}
    {t : W ⟶ X} {l : W ⟶ Y} {r : X ⟶ Z} {b : Y ⟶ Z}
    (h : IsPullback t l r b) :
    (SSet.Subcomplex.range b).preimage r = SSet.Subcomplex.range t := by
…

theorem OAI.Thomason.Construction.canonicalExtension_preimage_range line 934

Source documentation

A simplex of B enters the extension of a subobject precisely when it already lies in that subobject.

theorem canonicalExtension_preimage_range {A B : SSet.{u}} (i : A ⟶ B) [Mono i] :
    (SSet.Subcomplex.range (SSet.ex.map i)).preimage (canonicalExtension.app B) =
      SSet.Subcomplex.range i :=
…