Subcomplexes transported along isomorphisms

An isomorphism e : X ≅ Y of simplicial sets carries a subcomplex A of X to the subcomplex A.preimage e.inv of Y, and the inclusions of the two subcomplexes are isomorphic arrows. Hence any class of morphisms that respects isomorphisms, such as the (inner) anodyne extensions, contains one inclusion exactly when it contains the other.

Main results

• SSet.Subcomplex.isoOfPreimageEq: for A.preimage e.inv = B, the restriction of e to an isomorphism (A : SSet) ≅ B, compatible with the inclusions.
• SSet.Subcomplex.morphismProperty_ι_iff_of_preimage_eq: for A.preimage e.inv = B and a class W of morphisms respecting isomorphisms, W A.ι ↔ W B.ι.

def SSet.Subcomplex.isoOfPreimageEq {X Y : SSet} (e : X ≅ Y) {A : X.Subcomplex} {B : Y.Subcomplex} (h : A.preimage e.inv = B) : A.toSSet ≅ B.toSSet

If an isomorphism e : X ≅ Y carries a subcomplex A of X to a subcomplex B of Y, it restricts to an isomorphism between A and B.

@[simp]

theorem SSet.Subcomplex.isoOfPreimageEq_hom_ι {X Y : SSet} (e : X ≅ Y) {A : X.Subcomplex} {B : Y.Subcomplex} (h : A.preimage e.inv = B) : CategoryTheory.CategoryStruct.comp (isoOfPreimageEq e h).hom B.ι = CategoryTheory.CategoryStruct.comp A.ι e.hom

The restriction of e to A ≅ B commutes with the inclusions and e.hom.

@[simp]

theorem SSet.Subcomplex.isoOfPreimageEq_hom_ι_assoc {X Y : SSet} (e : X ≅ Y) {A : X.Subcomplex} {B : Y.Subcomplex} (h : A.preimage e.inv = B) {Z : SSet} (h✝ : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoOfPreimageEq e h).hom (CategoryTheory.CategoryStruct.comp B.ι h✝) = CategoryTheory.CategoryStruct.comp A.ι (CategoryTheory.CategoryStruct.comp e.hom h✝)

The restriction of e to A ≅ B commutes with the inclusions and e.hom.

@[simp]

theorem SSet.Subcomplex.isoOfPreimageEq_inv_ι {X Y : SSet} (e : X ≅ Y) {A : X.Subcomplex} {B : Y.Subcomplex} (h : A.preimage e.inv = B) : CategoryTheory.CategoryStruct.comp (isoOfPreimageEq e h).inv A.ι = CategoryTheory.CategoryStruct.comp B.ι e.inv

The restriction of e to A ≅ B commutes with the inclusions and e.inv.

@[simp]

theorem SSet.Subcomplex.isoOfPreimageEq_inv_ι_assoc {X Y : SSet} (e : X ≅ Y) {A : X.Subcomplex} {B : Y.Subcomplex} (h : A.preimage e.inv = B) {Z : SSet} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoOfPreimageEq e h).inv (CategoryTheory.CategoryStruct.comp A.ι h✝) = CategoryTheory.CategoryStruct.comp B.ι (CategoryTheory.CategoryStruct.comp e.inv h✝)

The restriction of e to A ≅ B commutes with the inclusions and e.inv.

theorem SSet.Subcomplex.morphismProperty_ι_iff_of_preimage_eq {X Y : SSet} (W : CategoryTheory.MorphismProperty SSet) [W.RespectsIso] (e : X ≅ Y) {A : X.Subcomplex} {B : Y.Subcomplex} (h : A.preimage e.inv = B) : W A.ι ↔ W B.ι

If an isomorphism e : X ≅ Y carries a subcomplex A of X to a subcomplex B of Y, then a class of morphisms respecting isomorphisms contains the inclusion of A exactly when it contains the inclusion of B.