Hopf problem: foundations · triangle period family homology splitting

Supporting definitions and proofs for this stage of the six-sphere construction.

noncomputable def Mathoverflow1973.TrianglePeriodFamilyHomologySplitting.freeRightSection {M : Type u_1} {K : Type u_2} [AddCommGroup M] [AddCommGroup K] [Module ℤ M] [Module ℤ K] [Module.Free ℤ K] (g : M →ₗ[ℤ] K) (hg : Function.Surjective ⇑g) : K →ₗ[ℤ] M

A linear right inverse to a surjective map with free codomain.

Equations

• Mathoverflow1973.TrianglePeriodFamilyHomologySplitting.freeRightSection g hg = Classical.choose ⋯

@[simp]

theorem Mathoverflow1973.TrianglePeriodFamilyHomologySplitting.freeRightSection_rightInverse {M : Type u_1} {K : Type u_2} [AddCommGroup M] [AddCommGroup K] [Module ℤ M] [Module ℤ K] [Module.Free ℤ K] (g : M →ₗ[ℤ] K) (hg : Function.Surjective ⇑g) (k : K) : g ((freeRightSection g hg) k) = k