Restricting a pair of simplicial sets to a subcomplex

For a pair of simplicial sets P, given by a monomorphism P.hom : P.left ⟶ P.right, and a subcomplex S of the ambient simplicial set P.right, the restriction P.restrict S is the pair (S, S ∩ P.left), whose subcomplex is the preimage of S under P.hom. The inclusions of S and of its preimage assemble into a morphism of pairs P.restrictι S : P.restrict S ⟶ P, and a morphism of pairs f : P ⟶ P' carrying S into S' restricts to a morphism SSetPair.restrictMap f h : P.restrict S ⟶ P'.restrict S'. Restriction of morphisms is compatible with the inclusions (SSetPair.restrictMap_comp_restrictι), with identities (SSetPair.restrictMap_id) and with composition (SSetPair.restrictMap_comp).

Restriction is the combinatorial step of excision for singular homology, where the singular pair of a topological pair is restricted to the simplices subordinate to an open cover; the comparison of relative homology is in TauCeti.AlgebraicTopology.SimplicialSet.Homology.Restrict.

References

• A. Hatcher, Algebraic Topology, Section 2.1, proof of Theorem 2.20.

instance SSet.Subcomplex.instMonoFromPreimage_tauCeti {X Y : SSet} (S : X.Subcomplex) (p : Y ⟶ X) [CategoryTheory.Mono p] : CategoryTheory.Mono (S.fromPreimage p)

theorem SSet.Subcomplex.mem_range_fromPreimage_app_iff {X Y : SSet} (S : X.Subcomplex) (p : Y ⟶ X) {n : SimplexCategoryᵒᵖ} (x : S.toSSet.obj n) : x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom ((S.fromPreimage p).app n)) ↔ ↑x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (p.app n))

A simplex of S lies in the image of the preimage of S under p exactly when it lies in the image of p.

@[reducible, inline]

abbrev SSetPair.restrict (P : SSetPair) (S : P.right.Subcomplex) : SSetPair

The restriction of a pair of simplicial sets P to a subcomplex S of its ambient simplicial set: the pair (S, S ∩ P.left), whose subcomplex is the preimage of S under P.hom.

Equations

• P.restrict S = SSetPair.of (S.fromPreimage P.hom)

def SSetPair.restrictι (P : SSetPair) (S : P.right.Subcomplex) : P.restrict S ⟶ P

The inclusion of the restriction of a pair to a subcomplex into the pair.

Equations

• P.restrictι S = SSetPair.homMk (S.preimage P.hom).ι S.ι ⋯

@[simp]

theorem SSetPair.restrictι_left (P : SSetPair) (S : P.right.Subcomplex) : (P.restrictι S).left = (S.preimage P.hom).ι

@[simp]

theorem SSetPair.restrictι_right (P : SSetPair) (S : P.right.Subcomplex) : (P.restrictι S).right = S.ι

theorem SSetPair.mem_range_restrict_hom_app_iff (P : SSetPair) (S : P.right.Subcomplex) {n : SimplexCategoryᵒᵖ} (x : (P.restrict S).right.obj n) : x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom ((P.restrict S).hom.app n)) ↔ ↑x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (P.hom.app n))

A simplex of the restricted pair comes from its subcomplex exactly when the underlying simplex of P comes from the subcomplex of P.

def SSetPair.restrictMap {P : SSetPair} {S : P.right.Subcomplex} {P' : SSetPair} {S' : P'.right.Subcomplex} (f : P ⟶ P') (h : S ≤ S'.preimage f.right) : P.restrict S ⟶ P'.restrict S'

A morphism of pairs f : P ⟶ P' carrying a subcomplex S of P.right into a subcomplex S' of P'.right restricts to a morphism of the restricted pairs.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSetPair.restrictMap_left_app_coe {P : SSetPair} {S : P.right.Subcomplex} {P' : SSetPair} {S' : P'.right.Subcomplex} (f : P ⟶ P') (h : S ≤ S'.preimage f.right) {n : SimplexCategoryᵒᵖ} (x : (P.restrict S).left.obj n) : ↑((CategoryTheory.ConcreteCategory.hom ((restrictMap f h).left.app n)) x) = (CategoryTheory.ConcreteCategory.hom (f.left.app n)) ↑x

@[simp]

theorem SSetPair.restrictMap_right_app_coe {P : SSetPair} {S : P.right.Subcomplex} {P' : SSetPair} {S' : P'.right.Subcomplex} (f : P ⟶ P') (h : S ≤ S'.preimage f.right) {n : SimplexCategoryᵒᵖ} (x : (P.restrict S).right.obj n) : ↑((CategoryTheory.ConcreteCategory.hom ((restrictMap f h).right.app n)) x) = (CategoryTheory.ConcreteCategory.hom (f.right.app n)) ↑x

theorem SSetPair.restrictMap_comp_restrictι {P : SSetPair} {S : P.right.Subcomplex} {P' : SSetPair} {S' : P'.right.Subcomplex} (f : P ⟶ P') (h : S ≤ S'.preimage f.right) : CategoryTheory.CategoryStruct.comp (restrictMap f h) (P'.restrictι S') = CategoryTheory.CategoryStruct.comp (P.restrictι S) f

The restriction of a morphism of pairs commutes with the inclusions of the restricted pairs.

theorem SSetPair.restrictMap_comp_restrictι_assoc {P : SSetPair} {S : P.right.Subcomplex} {P' : SSetPair} {S' : P'.right.Subcomplex} (f : P ⟶ P') (h : S ≤ S'.preimage f.right) {Z : SSetPair} (h✝ : P' ⟶ Z) : CategoryTheory.CategoryStruct.comp (restrictMap f h) (CategoryTheory.CategoryStruct.comp (P'.restrictι S') h✝) = CategoryTheory.CategoryStruct.comp (P.restrictι S) (CategoryTheory.CategoryStruct.comp f h✝)

The restriction of a morphism of pairs commutes with the inclusions of the restricted pairs.

@[simp]

theorem SSetPair.restrictMap_id (P : SSetPair) (S : P.right.Subcomplex) (h : S ≤ S.preimage (CategoryTheory.CategoryStruct.id P.right)) : restrictMap (CategoryTheory.CategoryStruct.id P) h = CategoryTheory.CategoryStruct.id (P.restrict S)

Restricting the identity of a pair gives the identity of the restricted pair.

theorem SSetPair.restrictMap_comp {P : SSetPair} {S : P.right.Subcomplex} {P' : SSetPair} {S' : P'.right.Subcomplex} (f : P ⟶ P') (h : S ≤ S'.preimage f.right) {P'' : SSetPair} {S'' : P''.right.Subcomplex} (g : P' ⟶ P'') (h' : S' ≤ S''.preimage g.right) : CategoryTheory.CategoryStruct.comp (restrictMap f h) (restrictMap g h') = restrictMap (CategoryTheory.CategoryStruct.comp f g) ⋯

Restricting a composite of morphisms of pairs gives the composite of the restrictions.

theorem SSetPair.restrictMap_comp_assoc {P : SSetPair} {S : P.right.Subcomplex} {P' : SSetPair} {S' : P'.right.Subcomplex} (f : P ⟶ P') (h : S ≤ S'.preimage f.right) {P'' : SSetPair} {S'' : P''.right.Subcomplex} (g : P' ⟶ P'') (h' : S' ≤ S''.preimage g.right) {Z : SSetPair} (h✝ : P''.restrict S'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (restrictMap f h) (CategoryTheory.CategoryStruct.comp (restrictMap g h') h✝) = CategoryTheory.CategoryStruct.comp (restrictMap (CategoryTheory.CategoryStruct.comp f g) ⋯) h✝

Restricting a composite of morphisms of pairs gives the composite of the restrictions.