Relative simplicial homology

In this file, given a pair P : SSetPair of simplicial sets, we define the chain complex P.chainComplex R of P with coefficients in R (where R is an object in a preadditive category with coproducts). The homology in degree n of this complex is denoted P.homology R n: this is the relative homology of the pair, which is related to the homology of simplicial sets P.left and P.right via a long homology sequence (see the lemmas SSetPair.homology_exact₁, SSetPair.homology_exact₂ and SSetPair.homology_exact₃),

@[reducible, inline]

noncomputable abbrev SSetPair.chainComplexFunctorLeft (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor C (CategoryTheory.Functor SSetPair (ChainComplex C ℕ))

The bifunctor which sends R : C and a pair of simplicial sets i : X ⟶ Y (with i a monomorphism) to X.chainComplex R, which is the chain complex of X with coefficients in R (the usual one is for C := Ab and R := ℤ.).

Equations

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

@[reducible, inline]

noncomputable abbrev SSetPair.chainComplexFunctorRight (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor C (CategoryTheory.Functor SSetPair (ChainComplex C ℕ))

The bifunctor which sends R : C and a pair of simplicial sets i : X ⟶ Y (with i a monomorphism) to Y.chainComplex R, which is the chain complex of Y with coefficients in R (the usual one is for C := Ab and R := ℤ.).

Equations

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

@[reducible, inline]

noncomputable abbrev SSetPair.chainComplexFunctorLeftToRight (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] : chainComplexFunctorLeft C ⟶ chainComplexFunctorRight C

The map X.chainComplex R ⟶ Y.chainComplex R for each pair of simplicial sets i : X ⟶ Y (with i a monomorphism), and R : C, as a natural transformation of bifunctors C ⥤ SSetPair ⥤ ChainComplex C ℕ.

Equations

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

instance SSetPair.instMonoFNatChainComplexMapHomSSet (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (P : SSetPair) (n : ℕ) : CategoryTheory.Mono ((SSet.chainComplexMap P.hom R).f n)

instance SSetPair.instMonoChainComplexNatChainComplexMapHomSSet (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (P : SSetPair) : CategoryTheory.Mono (SSet.chainComplexMap P.hom R)

instance SSetPair.instMonoFNatAppChainComplexFunctorChainComplexFunctorLeftToRight (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (P : SSetPair) (n : ℕ) : CategoryTheory.Mono ((((chainComplexFunctorLeftToRight C).app R).app P).f n)

instance SSetPair.instMonoChainComplexNatAppFunctorChainComplexFunctorLeftToRight (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (P : SSetPair) : CategoryTheory.Mono (((chainComplexFunctorLeftToRight C).app R).app P)

instance SSetPair.instMonoFunctorChainComplexNatAppChainComplexFunctorLeftToRight (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : CategoryTheory.Mono ((chainComplexFunctorLeftToRight C).app R)

instance SSetPair.instMonoFunctorChainComplexNatChainComplexFunctorLeftToRight (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] : CategoryTheory.Mono (chainComplexFunctorLeftToRight C)

instance SSetPair.instHasCokernelFNatAppChainComplexFunctorChainComplexFunctorLeftToRight (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (P : SSetPair) (n : ℕ) : CategoryTheory.Limits.HasCokernel ((((chainComplexFunctorLeftToRight C).app R).app P).f n)

instance SSetPair.instHasCokernelFNatChainComplexMapHomSSet (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (P : SSetPair) (n : ℕ) : CategoryTheory.Limits.HasCokernel ((SSet.chainComplexMap P.hom R).f n)

instance SSetPair.instHasCokernelChainComplexNatAppFunctorChainComplexFunctorLeftToRight (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (P : SSetPair) : CategoryTheory.Limits.HasCokernel (((chainComplexFunctorLeftToRight C).app R).app P)

instance SSetPair.instHasCokernelFunctorChainComplexNatAppChainComplexFunctorLeftToRight (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : CategoryTheory.Limits.HasCokernel ((chainComplexFunctorLeftToRight C).app R)

instance SSetPair.instHasCokernelFunctorChainComplexNatChainComplexFunctorLeftToRight (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] : CategoryTheory.Limits.HasCokernel (chainComplexFunctorLeftToRight C)

noncomputable def SSetPair.chainComplexFunctor (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor C (CategoryTheory.Functor SSetPair (ChainComplex C ℕ))

The relative chain complex associated to a pair of simplicial sets, with coefficients in R : C, as a bifunctor C ⥤ SSetPair.{w} ⥤ ChainComplex C ℕ. It computes the simplicial homology of a pair of simplicial sets with coefficients in R. One can recover the ordinary relative simplicial chain complex when C := Ab and R := ℤ.

Equations

• SSetPair.chainComplexFunctor C = CategoryTheory.Limits.cokernel (SSetPair.chainComplexFunctorLeftToRight C)

noncomputable def SSetPair.chainComplexFunctorπ (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] : chainComplexFunctorRight C ⟶ chainComplexFunctor C

For any pair of simplicial sets i : X ⟶ Y (with i a monomorphism) and any R : C, this is the map from the chain complex of Y (with coefficients in R) to the chain complex of the pair, as a natural transformation of bifunctors C ⥤ SSetPair ⥤ ChainComplex C ℕ.

Equations

• SSetPair.chainComplexFunctorπ C = CategoryTheory.Limits.cokernel.π (SSetPair.chainComplexFunctorLeftToRight C)

instance SSetPair.instEpiFunctorChainComplexNatChainComplexFunctorπ (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] : CategoryTheory.Epi (chainComplexFunctorπ C)

@[simp]

theorem SSetPair.chainComplexFunctor_condition (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] : CategoryTheory.CategoryStruct.comp (chainComplexFunctorLeftToRight C) (chainComplexFunctorπ C) = 0

@[simp]

theorem SSetPair.chainComplexFunctor_condition_assoc (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {Z : CategoryTheory.Functor C (CategoryTheory.Functor SSetPair (ChainComplex C ℕ))} (h : chainComplexFunctor C ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainComplexFunctorLeftToRight C) (CategoryTheory.CategoryStruct.comp (chainComplexFunctorπ C) h) = CategoryTheory.CategoryStruct.comp 0 h

@[reducible, inline]

noncomputable abbrev SSetPair.cokernelCoforkChainComplexFunctorLeftToRight (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] : CategoryTheory.Limits.CokernelCofork (chainComplexFunctorLeftToRight C)

The (colimit) cokernel cofork expressing the bifunctor SSetPair.chainComplexFunctor C : C ⥤ SSetPair ⥤ ChainComplex C ℕ as a cokernel of chainComplexFunctorLeftToRight C.

Equations

• SSetPair.cokernelCoforkChainComplexFunctorLeftToRight C = CategoryTheory.Limits.CokernelCofork.ofπ (SSetPair.chainComplexFunctorπ C) ⋯

noncomputable def SSetPair.isColimitCokernelCoforkChainComplexFunctorLeftToRight (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] : CategoryTheory.Limits.IsColimit (cokernelCoforkChainComplexFunctorLeftToRight C)

The bifunctor SSetPair.chainComplexFunctor C : C ⥤ SSetPair ⥤ ChainComplex C ℕ is a cokernel of chainComplexFunctorLeftToRight C.

Equations

• SSetPair.isColimitCokernelCoforkChainComplexFunctorLeftToRight C = CategoryTheory.Limits.cokernelIsCokernel (SSetPair.chainComplexFunctorLeftToRight C)

instance SSetPair.instPreservesColimitFunctorChainComplexNatWalkingParallelPairParallelPairChainComplexFunctorLeftToRightOfNatHomChainComplexFunctorLeftChainComplexFunctorRightObjEvaluation (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (chainComplexFunctorLeftToRight C) 0) ((CategoryTheory.evaluation C (CategoryTheory.Functor SSetPair (ChainComplex C ℕ))).obj R)

instance SSetPair.instPreservesColimitFunctorChainComplexNatWalkingParallelPairParallelPairAppChainComplexFunctorLeftToRightOfNatHomObjChainComplexFunctorLeftChainComplexFunctorRightEvaluation (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (P : SSetPair) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair ((chainComplexFunctorLeftToRight C).app R) 0) ((CategoryTheory.evaluation SSetPair (ChainComplex C ℕ)).obj P)

instance SSetPair.instPreservesColimitFunctorChainComplexNatWalkingParallelPairCompParallelPairChainComplexFunctorLeftToRightOfNatHomChainComplexFunctorLeftChainComplexFunctorRightObjEvaluation (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (P : SSetPair) : CategoryTheory.Limits.PreservesColimit ((CategoryTheory.Limits.parallelPair (chainComplexFunctorLeftToRight C) 0).comp ((CategoryTheory.evaluation C (CategoryTheory.Functor SSetPair (ChainComplex C ℕ))).obj R)) ((CategoryTheory.evaluation SSetPair (ChainComplex C ℕ)).obj P)

instance SSetPair.instPreservesColimitChainComplexNatWalkingParallelPairParallelPairAppFunctorChainComplexFunctorLeftToRightOfNatHomObjChainComplexFunctorLeftChainComplexFunctorRightEvalDown (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (P : SSetPair) (n : ℕ) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (((chainComplexFunctorLeftToRight C).app R).app P) 0) (HomologicalComplex.eval C (ComplexShape.down ℕ) n)

instance SSetPair.instPreservesColimitChainComplexNatWalkingParallelPairCompFunctorParallelPairChainComplexFunctorLeftToRightOfNatHomChainComplexFunctorLeftChainComplexFunctorRightObjEvaluationEvalDown (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (P : SSetPair) (n : ℕ) : CategoryTheory.Limits.PreservesColimit ((CategoryTheory.Limits.parallelPair (chainComplexFunctorLeftToRight C) 0).comp (((CategoryTheory.evaluation C (CategoryTheory.Functor SSetPair (ChainComplex C ℕ))).obj R).comp ((CategoryTheory.evaluation SSetPair (ChainComplex C ℕ)).obj P))) (HomologicalComplex.eval C (ComplexShape.down ℕ) n)

instance SSetPair.instPreservesColimitFunctorChainComplexNatWalkingParallelPairParallelPairChainComplexFunctorLeftToRightOfNatHomChainComplexFunctorLeftChainComplexFunctorRightCompObjEvaluationEvalDown (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (P : SSetPair) (n : ℕ) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (chainComplexFunctorLeftToRight C) 0) (((CategoryTheory.evaluation C (CategoryTheory.Functor SSetPair (ChainComplex C ℕ))).obj R).comp (((CategoryTheory.evaluation SSetPair (ChainComplex C ℕ)).obj P).comp (HomologicalComplex.eval C (ComplexShape.down ℕ) n)))

instance SSetPair.instPreservesColimitChainComplexNatWalkingParallelPairParallelPairChainComplexMapHomSSetOfNatHomChainComplexObjIdLeftRightEvalDown (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (P : SSetPair) (n : ℕ) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (SSet.chainComplexMap P.hom R) 0) (HomologicalComplex.eval C (ComplexShape.down ℕ) n)

@[reducible, inline]

noncomputable abbrev SSetPair.chainComplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) : ChainComplex C ℕ

The relative chain complex of a pair P of simplicial sets with coefficients in R : C (e.g. C := Ab and R := ℤ.) This identifies to the cokernel of the morphism P.left.chainComplex R ⟶ P.right.chainComplex R of simplicial chain complexes.

Equations

• P.chainComplex R = ((SSetPair.chainComplexFunctor C).obj R).obj P

@[reducible, inline]

noncomputable abbrev SSetPair.chainComplexMap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : SSetPair} (f : P ⟶ P') (R : C) : P.chainComplex R ⟶ P'.chainComplex R

The morphism of relative simplicial chain complexes induces by a morphism of pairs of simplicial sets.

Equations

• SSetPair.chainComplexMap f R = ((SSetPair.chainComplexFunctor C).obj R).map f

noncomputable def SSetPair.chainComplexπ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) : P.right.chainComplex R ⟶ P.chainComplex R

Given a pair of simplicial sets i : X ⟶ Y (with i a monomorphism), this is the morphism from the chain complex of Y to the chain complex of the pair.

Equations

• P.chainComplexπ R = ((SSetPair.chainComplexFunctorπ C).app R).app P

@[simp]

theorem SSetPair.chainComplex_condition {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap P.hom R) (P.chainComplexπ R) = 0

@[simp]

theorem SSetPair.chainComplex_condition_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) {Z : ChainComplex C ℕ} (h : P.chainComplex R ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap P.hom R) (CategoryTheory.CategoryStruct.comp (P.chainComplexπ R) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem SSetPair.chainComplex_condition_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap P.hom R).f n) ((P.chainComplexπ R).f n) = 0

@[simp]

theorem SSetPair.chainComplex_condition_f_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) (n : ℕ) {Z : C} (h : (P.chainComplex R).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap P.hom R).f n) (CategoryTheory.CategoryStruct.comp ((P.chainComplexπ R).f n) h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def SSetPair.cokernelCoforkChainComplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) : CategoryTheory.Limits.CokernelCofork (SSet.chainComplexMap P.hom R)

Given a pair of simplicial sets i : X ⟶ Y (with i a monomorphism) and R : C (e.g. C := Ab and R := ℤ), this is the cokernel cofork expressing the chain complex SSetPair.chainComplex of the pair as a cokernel of the map X.chainComplex R ⟶ Y.chainComplex R.

Equations

• P.cokernelCoforkChainComplex R = CategoryTheory.Limits.CokernelCofork.ofπ (P.chainComplexπ R) ⋯

noncomputable def SSetPair.isColimitCokernelCoforkChainComplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) : CategoryTheory.Limits.IsColimit (P.cokernelCoforkChainComplex R)

Given a pair of simplicial sets i : X ⟶ Y (with i a monomorphism) and R : C (e.g. C := Ab and R := ℤ), the chain complex SSetPair.chainComplex of the pair is a cokernel of the map X.chainComplex R ⟶ Y.chainComplex R.

Equations

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

instance SSetPair.instEpiChainComplexNatChainComplexπ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) : CategoryTheory.Epi (P.chainComplexπ R)

instance SSetPair.isIso_chainComplexπ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) [P.left.HasDimensionLT 0] : CategoryTheory.IsIso (P.chainComplexπ R)

theorem SSetPair.isZero_chainComplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) [CategoryTheory.IsIso P.hom] : CategoryTheory.Limits.IsZero (P.chainComplex R)

noncomputable def SSetPair.cokernelCoforkChainComplexX {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) (n : ℕ) : CategoryTheory.Limits.CokernelCofork ((SSet.chainComplexMap P.hom R).f n)

Given a pair of simplicial sets i : X ⟶ Y (with i a monomorphism), R : C (e.g. C := Ab and R := ℤ) and n : ℕ, this is the cokernel cofork expressing the chain complex SSetPair.chainComplex of the pair in degree n as a cokernel of the map (X.chainComplex R).X n ⟶ (Y.chainComplex R).X n.

Equations

• P.cokernelCoforkChainComplexX R n = CategoryTheory.Limits.CokernelCofork.ofπ ((P.chainComplexπ R).f n) ⋯

noncomputable def SSetPair.isColimitCokernelCoforkChainComplexX {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) (n : ℕ) : CategoryTheory.Limits.IsColimit (P.cokernelCoforkChainComplexX R n)

Given a pair of simplicial sets i : X ⟶ Y (with i a monomorphism), R : C (e.g. C := Ab and R := ℤ) and n : ℕ, the chain complex SSetPair.chainComplex of the pair in degree n is a cokernel of the map (X.chainComplex R).X n ⟶ (Y.chainComplex R).X n.

Equations

• P.isColimitCokernelCoforkChainComplexX R n = (P.cokernelCoforkChainComplex R).mapIsColimit (P.isColimitCokernelCoforkChainComplex R) (HomologicalComplex.eval C (ComplexShape.down ℕ) n)

instance SSetPair.instEpiFNatChainComplexπ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) (n : ℕ) : CategoryTheory.Epi ((P.chainComplexπ R).f n)

@[reducible, inline]

noncomputable abbrev SSetPair.chainComplexShortComplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) : CategoryTheory.ShortComplex (ChainComplex C ℕ)

Given a pair of simplicial sets corresponding to a monomorphism i : X ⟶ Y, this is the (short exact) short complex which relates the chain complex of X, of Y and of the pair.

Equations

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

@[reducible, inline]

noncomputable abbrev SSetPair.homology {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : C

The relative simplicial homology with coefficients in R : C in degree n of a pair of simplicial sets.

Equations

• P.homology R n = HomologicalComplex.homology (P.chainComplex R) n

@[reducible, inline]

noncomputable abbrev SSetPair.homologyMap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : SSetPair} (f : P ⟶ P') (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : P.homology R n ⟶ P'.homology R n

The morphism in relative simplicial homology that is induced by a morphism of pairs of simplicial sets.

Equations

• SSetPair.homologyMap f R n = HomologicalComplex.homologyMap (SSetPair.chainComplexMap f R) n

@[simp]

theorem SSetPair.homologyMap_id {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : SSetPair.homologyMap (CategoryTheory.CategoryStruct.id P) R n = CategoryTheory.CategoryStruct.id (P.homology R n)

theorem SSetPair.homologyMap_comp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' P'' : SSetPair} (f : P ⟶ P') (g : P' ⟶ P'') (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : SSetPair.homologyMap (CategoryTheory.CategoryStruct.comp f g) R n = CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap f R n) (SSetPair.homologyMap g R n)

theorem SSetPair.homologyMap_comp_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' P'' : SSetPair} (f : P ⟶ P') (g : P' ⟶ P'') (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) {Z : C} (h : P''.homology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap (CategoryTheory.CategoryStruct.comp f g) R n) h = CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap f R n) (CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap g R n) h)

@[implicit_reducible]

noncomputable def SSetPair.homologyFunctor {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : CategoryTheory.Functor SSetPair C

The relative simplicial homology functor in degree n with coefficients in R : C.

Equations

• SSetPair.homologyFunctor R n = { obj := fun (P : SSetPair) => P.homology R n, map := fun {X Y : SSetPair} (f : X ⟶ Y) => SSetPair.homologyMap f R n, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem SSetPair.homologyFunctor_obj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) (P : SSetPair) : (homologyFunctor R n).obj P = P.homology R n

@[simp]

theorem SSetPair.homologyFunctor_map {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) {X✝ Y✝ : SSetPair} (f : X✝ ⟶ Y✝) : (homologyFunctor R n).map f = SSetPair.homologyMap f R n

@[reducible, inline]

noncomputable abbrev SSetPair.homologyπ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : P.right.homology R n ⟶ P.homology R n

Given a pair of simplicial sets corresponding to a monomorphism i : X ⟶ Y, this is the morphism from the homology of Y to the relative homology of the pair.

Equations

• P.homologyπ R n = HomologicalComplex.homologyMap (P.chainComplexπ R) n

@[simp]

theorem SSetPair.homologyMap_hom_homologyπ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : CategoryTheory.CategoryStruct.comp (SSet.homologyMap P.hom R n) (P.homologyπ R n) = 0

@[simp]

theorem SSetPair.homologyMap_hom_homologyπ_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) {Z : C} (h : P.homology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSet.homologyMap P.hom R n) (CategoryTheory.CategoryStruct.comp (P.homologyπ R n) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem SSetPair.shortExact_chainComplexShortComplex {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : SSetPair) (R : A) : (P.chainComplexShortComplex R).ShortExact

noncomputable def SSetPair.homologyδ {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : SSetPair) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : P.homology R n ⟶ P.left.homology R m

Given a pair of simplicial sets corresponding to a monomorphism i : X ⟶ Y, this is the connecting morphism from the homology of the pair to the homology of X.

Equations

• P.homologyδ R n m h = ⋯.δ n m ⋯

@[simp]

theorem SSetPair.homologyδ_comp {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : SSetPair) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (P.homologyδ R n m h) (SSet.homologyMap P.hom R m) = 0

@[simp]

theorem SSetPair.homologyδ_comp_assoc {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : SSetPair) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) {Z : A} (h✝ : P.right.homology R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.homologyδ R n m h) (CategoryTheory.CategoryStruct.comp (SSet.homologyMap P.hom R m) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem SSetPair.comp_homologyδ {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : SSetPair) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (P.homologyπ R n) (P.homologyδ R n m h) = 0

@[simp]

theorem SSetPair.comp_homologyδ_assoc {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : SSetPair) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) {Z : A} (h✝ : P.left.homology R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.homologyπ R n) (CategoryTheory.CategoryStruct.comp (P.homologyδ R n m h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

theorem SSetPair.homology_exact₁ {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : SSetPair) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : { X₁ := P.homology R n, X₂ := P.left.homology R m, X₃ := ((CategoryTheory.Functor.id SSet).obj P.right).homology R m, f := P.homologyδ R n m h, g := SSet.homologyMap P.hom R m, zero := ⋯ }.Exact

Given P : SSetPair corresponding to a monomorphism i : Y ⟶ X, the sequence Hₘ₊₁(X;Y) ⟶ Hₘ(Y) ⟶ Hₘ(X) is exact.

theorem SSetPair.homology_exact₂ {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : SSetPair) (R : A) (n : ℕ) : { X₁ := ((CategoryTheory.Functor.id SSet).obj P.left).homology R n, X₂ := ((CategoryTheory.Functor.id SSet).obj P.right).homology R n, X₃ := P.homology R n, f := SSet.homologyMap P.hom R n, g := P.homologyπ R n, zero := ⋯ }.Exact

Given P : SSetPair corresponding to a monomorphism i : Y ⟶ X, the sequence Hₙ(Y) ⟶ Hₙ(X) ⟶ Hₙ(X;Y) is exact.

theorem SSetPair.homology_exact₃ {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : SSetPair) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : { X₁ := P.right.homology R n, X₂ := P.homology R n, X₃ := P.left.homology R m, f := P.homologyπ R n, g := P.homologyδ R n m h, zero := ⋯ }.Exact

Given P : SSetPair corresponding to a monomorphism i : Y ⟶ X, the sequence Hₘ₊₁(X) ⟶ Hₘ₊₁(X;Y) ⟶ Hₘ(Y) is exact.

instance SSetPair.instEpiHomologyπOfNatNat {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : SSetPair) (R : A) : CategoryTheory.Epi (P.homologyπ R 0)