The generator of the relative homology of the interval modulo its endpoints

The identification TauCeti.singularHomologyCubeBoundaryPairIso R 1 : H₁(I¹, ∂I¹; R) ≅ R is transported from the disk pair (D¹, S⁰), whose generator is sent by the connecting morphism to the standard generator [-e₀] - [e₀] of reduced H₀(S⁰) (TauCeti.reducedSingularHomologyTopCatSphereIso). This file computes the generator explicitly: it is the negative of the relative class of the standard singular simplex t ↦ t of the interval, that is, the class of the simplex running from 1 to 0 (TauCeti.singularHomologyCubeBoundaryPairIso_one_inv).

The sign is checked through the connecting morphism, which is injective because I¹ is contractible. Under the homeomorphism TauCeti.diskHomeomorphCube 1, the point e₀ of S⁰ goes to 1 and -e₀ to 0 (the radial rescaling onto the sup-norm ball keeps the sign of the coordinate and the affine map x ↦ (x + 1) / 2 follows), so the generator is sent to [0] - [1]. The standard simplex is sent to [1] - [0] (TauCeti.cubeRelClass_singularHomologyδ).

Main definitions and results

• TauCeti.cubeSimplex, TauCeti.cubeRelClass: the standard 1-simplex of I¹ and its class in H₁(I¹, ∂I¹; R); TauCeti.cubeRelClass_singularHomologyMap: its image under a map of pairs.
• TauCeti.reducedSingularHomologyTopCatSphereIso_zero_inv_ι: the generator of reduced H₀(S⁰) is [-e₀] - [e₀] on TopCat.sphere 0.
• TauCeti.eq_sphereMinus_or_eq_spherePlus, TauCeti.sphereMinus_ne_spherePlus: S⁰ consists of the two distinct points -e₀ and e₀.
• TauCeti.singularHomologyCubeBoundaryPairIso_one_inv: the generator of H₁(I¹, ∂I¹; R) is -cubeRelClass R.

def TauCeti.cubePoint (t : ↑unitInterval) : ↑TopPair.fst

The point of the cube I¹ with coordinate t.

@[simp]

theorem TauCeti.cubePoint_down (t : ↑unitInterval) : (cubePoint t).down = fun (x : Fin 1) => t

theorem TauCeti.continuous_cubePoint : Continuous cubePoint

The parametrization TauCeti.cubePoint of the cube I¹ is continuous.

def TauCeti.cubeEnd (t : ↑unitInterval) (ht : t = 0 ∨ t = 1) : ↑TopPair.snd

An endpoint of the cube I¹, as a point of its boundary.

theorem TauCeti.map_cubeEnd (t : ↑unitInterval) (ht : t = 0 ∨ t = 1) : (CategoryTheory.ConcreteCategory.hom TopPair.map) (cubeEnd t ht) = cubePoint t

The endpoint TauCeti.cubeEnd t ht of I¹ is the point TauCeti.cubePoint t.

noncomputable def TauCeti.cubeSimplex : (TopCat.toSSet.obj TopPair.fst).obj (Opposite.op { len := 1 })

The standard singular 1-simplex of the cube I¹, from 0 to 1: the singular 1-simplex TauCeti.TopCat.simplex₁ of the parametrization TauCeti.cubePoint of I¹.

noncomputable def TauCeti.cubeEndVertex (t : ↑unitInterval) (ht : t = 0 ∨ t = 1) : (TopCat.toSSet.obj TopPair.snd).obj (Opposite.op { len := 0 })

An endpoint of the cube I¹, as a singular 0-simplex of its boundary.

theorem TauCeti.toSSetObjEquiv_cubeSimplex_apply (a : Convexity.StdSimplex ℝ (Fin 2)) : ((TopPair.fst.toSSetObjEquiv (Opposite.op { len := 1 })) cubeSimplex) a = cubePoint (Convexity.StdSimplex.homeomorphI a)

The standard simplex of I¹ is the parametrization of the standard 1-simplex by its last weight.

theorem TauCeti.δ_one_cubeSimplex : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj TopPair.fst) 1)) cubeSimplex = (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map TopPair.map).app (Opposite.op { len := 0 }))) (cubeEndVertex 0 ⋯)

theorem TauCeti.δ_zero_cubeSimplex : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj TopPair.fst) 0)) cubeSimplex = (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map TopPair.map).app (Opposite.op { len := 0 }))) (cubeEndVertex 1 ⋯)

noncomputable def TauCeti.cubeRelClass {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) : R ⟶ (cubeBoundaryPair 1).singularHomology R 1

The relative class in H₁(I¹, ∂I¹; R) of the standard singular 1-simplex of the cube.

theorem TauCeti.cubeRelClass_singularHomologyδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) : CategoryTheory.CategoryStruct.comp (cubeRelClass R) ((cubeBoundaryPair 1).singularHomologyδ R 1 0 cubeRelClass_singularHomologyδ._proof_2) = singularHomology₀Section R (cubeEnd 1 ⋯) - singularHomology₀Section R (cubeEnd 0 ⋯)

The connecting morphism sends the relative class of the standard simplex of I¹ to the difference of the classes of its endpoints, [1] - [0].

theorem TauCeti.cubeRelClass_singularHomologyMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P : TopPair} (f : cubeBoundaryPair 1 ⟶ P) : CategoryTheory.CategoryStruct.comp (cubeRelClass R) (TopPair.singularHomologyMap f R 1) = SSetPair.relClass₁ R (TopPair.toSSetPair.obj P) ((CategoryTheory.ConcreteCategory.hom ((TopPair.toSSetPair.map f).right.app (Opposite.op { len := 1 }))) cubeSimplex) ((CategoryTheory.ConcreteCategory.hom ((TopPair.toSSetPair.map f).left.app (Opposite.op { len := 0 }))) (cubeEndVertex 0 ⋯)) ((CategoryTheory.ConcreteCategory.hom ((TopPair.toSSetPair.map f).left.app (Opposite.op { len := 0 }))) (cubeEndVertex 1 ⋯)) ⋯ ⋯

A map of pairs f : (I¹, ∂I¹) ⟶ P sends the relative class of the standard simplex of I¹ to the relative class of the image simplex.

@[reducible, inline]

noncomputable abbrev TauCeti.sphereZeroBasis : OrthonormalBasis (Fin 1) ℝ (EuclideanSpace ℝ (ULift.{w, 0} (Fin 1)))

The standard orthonormal basis of EuclideanSpace ℝ (ULift (Fin 1)), which determines the generator of reduced H₀(S⁰).

noncomputable def TauCeti.spherePlus : ↑(TopCat.diskBoundary 1)

The point e₀ of TopCat.sphere 0.

noncomputable def TauCeti.sphereMinus : ↑(TopCat.diskBoundary 1)

The point -e₀ of TopCat.sphere 0.

theorem TauCeti.reducedSingularHomologyTopCatSphereIso_zero_inv_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) : CategoryTheory.CategoryStruct.comp (reducedSingularHomologyTopCatSphereIso R 0).inv ((reducedSingularHomologyι R 0).app (TopCat.sphere 0)) = singularHomology₀Section R sphereMinus - singularHomology₀Section R spherePlus

The standard generator of reduced H₀(S⁰) is the class [-e₀] - [e₀].

theorem TauCeti.spherePlus_coord : (↑((CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion 1)) spherePlus).down).ofLp 0 = 1

theorem TauCeti.sphereMinus_coord : (↑((CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion 1)) sphereMinus).down).ofLp 0 = -1

theorem TauCeti.eq_sphereMinus_or_eq_spherePlus (p : ↑(TopCat.diskBoundary 1)) : p = sphereMinus ∨ p = spherePlus

S⁰ consists of the two points -e₀ and e₀.

theorem TauCeti.sphereMinus_ne_spherePlus : sphereMinus ≠ spherePlus

The two points -e₀ and e₀ of S⁰ are distinct.

theorem TauCeti.diskBoundaryPairToCube_snd_spherePlus : (CategoryTheory.ConcreteCategory.hom (TopPair.Hom.snd (diskBoundaryPairToCube 1))) spherePlus = cubeEnd 1 ⋯

theorem TauCeti.diskBoundaryPairToCube_snd_sphereMinus : (CategoryTheory.ConcreteCategory.hom (TopPair.Hom.snd (diskBoundaryPairToCube 1))) sphereMinus = cubeEnd 0 ⋯

instance TauCeti.mono_cubeBoundaryPair_singularHomologyδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) : CategoryTheory.Mono ((cubeBoundaryPair 1).singularHomologyδ R 1 0 cubeRelClass_singularHomologyδ._proof_2)

The connecting morphism of the cube pair (I¹, ∂I¹) is a monomorphism, since I¹ is contractible.

theorem TauCeti.singularHomologyCubeBoundaryPairIso_one_inv_singularHomologyδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) : CategoryTheory.CategoryStruct.comp (singularHomologyCubeBoundaryPairIso R 1).inv ((cubeBoundaryPair 1).singularHomologyδ R 1 0 cubeRelClass_singularHomologyδ._proof_2) = singularHomology₀Section R (cubeEnd 0 ⋯) - singularHomology₀Section R (cubeEnd 1 ⋯)

The connecting morphism sends the generator of H₁(I¹, ∂I¹; R) to [0] - [1].

theorem TauCeti.singularHomologyCubeBoundaryPairIso_one_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) : (singularHomologyCubeBoundaryPairIso R 1).inv = -cubeRelClass R

The generator of H₁(I¹, ∂I¹; R) is the negative of the relative class of the standard singular simplex t ↦ t of the interval: it is the class of the simplex running from 1 to 0. Indeed the connecting morphism sends the generator to [0] - [1], the transport of the standard generator [-e₀] - [e₀] of reduced H₀(S⁰), and the standard simplex to [1] - [0].