Sections of short exact sequences

This file contains basics of sections of short exact sequences. In particular it is proved that in a short exact sequence of

Main definitions

• MonoidHom.corrector: Given a short exact sequence 1 ⟶ H ⟶ K ⟶ G ⟶ 1 of groups (with maps ι : H → K and π : K → G) and a section σ : G → K of it (π ∘ σ = id_G), the corrector γ : K → H is the unique function such that k = σ(π(k)) * ι(γ(k)) for any k : K.
• MonoidHom.correctorHom: Given a short exact sequence 0 ⟶ U ⟶ V ⟶ W ⟶ 0 of abelian groups and a section σ : W → V of it, the corrector γ : V → U is a group homomorphism, uniquely specified by the condition v = σ(π(v)) + ι(γ(v)) for any v : V.
• LinearMap.chooseSection: Given a short exact sequence 0 ⟶ U ⟶ V ⟶ W ⟶ 0 of modules, where W is a free module, one can choose a linear section σ : W → V of the short exact sequence.
• LinearMap.corrector: Given a short exact sequence 0 ⟶ U ⟶ V ⟶ W ⟶ 0 of modules and a section σ : W → V, the corrector γ : V → U is a linear map, uniquely specified by the condition v = σ(π(v)) + ι(γ(v)) for any v : V.
• sesBasis: Given a short exact sequence 0 ⟶ U ⟶ V ⟶ W ⟶ 0 of modules and a section σ : W → V of it, one can construct a basis of V from a basis of W and a basis of U.

Main statements

• ses_directSum_isInternal: The property v = σ(π(v)) + ι(γ(v)) of a corrector γ of a section σ of a short exact sequence 0 ⟶ U ⟶ V ⟶ W ⟶ 0 of modules gives an internal direct sum decomposition V = σ(W) ⊕ ι(U).

Tags

short exact sequence

theorem MonoidHom.unique_corrector {U : Type u_1} {V : Type u_2} {W : Type u_3} [Group U] [Group V] [Group W] {f : U →* V} {g : V →* W} {σ : W → V} (hf : f.ker = ⊥) (v : V) (u₁ u₂ : U) (h₁ : v = σ (g v) * f u₁) (h₂ : v = σ (g v) * f u₂) : u₁ = u₂

Uniqueness of the "corrector" for a given vector.

theorem AddMonoidHom.unique_corrector {U : Type u_1} {V : Type u_2} {W : Type u_3} [AddGroup U] [AddGroup V] [AddGroup W] {f : U →+ V} {g : V →+ W} {σ : W → V} (hf : f.ker = ⊥) (v : V) (u₁ u₂ : U) (h₁ : v = σ (g v) + f u₁) (h₂ : v = σ (g v) + f u₂) : u₁ = u₂

theorem MonoidHom.exists_corrector {U : Type u_1} {V : Type u_2} {W : Type u_3} [Group U] [Group V] [Group W] {f : U →* V} {g : V →* W} {σ : W → V} (hfg : f.range = g.ker) (hgσ : ⇑g ∘ σ = _root_.id) (v : V) : ∃ (u : U), v = σ (g v) * f u

Existence of the "corrector" for a given vector.

theorem AddMonoidHom.exists_corrector {U : Type u_1} {V : Type u_2} {W : Type u_3} [AddGroup U] [AddGroup V] [AddGroup W] {f : U →+ V} {g : V →+ W} {σ : W → V} (hfg : f.range = g.ker) (hgσ : ⇑g ∘ σ = _root_.id) (v : V) : ∃ (u : U), v = σ (g v) + f u

noncomputable def MonoidHom.corrector {U : Type u_1} {V : Type u_2} {W : Type u_3} [Group U] [Group V] [Group W] {f : U →* V} {g : V →* W} {σ : W → V} (hfg : f.range = g.ker) (hgσ : ⇑g ∘ σ = _root_.id) (v : V) : U

The corrector function γ : V → U associated to a section σ : W → V of a short exact sequence 1 ⟶ U ⟶ V ⟶ W ⟶ 1.

Equations

• MonoidHom.corrector hfg hgσ v = ⋯.choose

noncomputable def AddMonoidHom.corrector {U : Type u_1} {V : Type u_2} {W : Type u_3} [AddGroup U] [AddGroup V] [AddGroup W] {f : U →+ V} {g : V →+ W} {σ : W → V} (hfg : f.range = g.ker) (hgσ : ⇑g ∘ σ = _root_.id) (v : V) : U

The additive corrector function γ : V → U associated to a section σ : W → V of a short exact sequence 0 ⟶ U ⟶ V ⟶ W ⟶ 0.

Equations

• AddMonoidHom.corrector hfg hgσ v = ⋯.choose

theorem MonoidHom.corrector_spec {U : Type u_1} {V : Type u_2} {W : Type u_3} [Group U] [Group V] [Group W] {f : U →* V} {g : V →* W} {σ : W → V} (hfg : f.range = g.ker) (hgσ : ⇑g ∘ σ = _root_.id) (v : V) : v = σ (g v) * f (corrector hfg hgσ v)

The corrector map γ : V → U satisfies v = σ(g(v)) * f(γ(v)) for any v : V.

theorem AddMonoidHom.corrector_spec {U : Type u_1} {V : Type u_2} {W : Type u_3} [AddGroup U] [AddGroup V] [AddGroup W] {f : U →+ V} {g : V →+ W} {σ : W → V} (hfg : f.range = g.ker) (hgσ : ⇑g ∘ σ = _root_.id) (v : V) : v = σ (g v) + f (corrector hfg hgσ v)

theorem MonoidHom.corrector_eq_iff {U : Type u_1} {V : Type u_2} {W : Type u_3} [Group U] [Group V] [Group W] {f : U →* V} {g : V →* W} {σ : W → V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : ⇑g ∘ σ = _root_.id) (v : V) (u : U) : corrector hfg hgσ v = u ↔ v = σ (g v) * f u

theorem AddMonoidHom.corrector_eq_iff {U : Type u_1} {V : Type u_2} {W : Type u_3} [AddGroup U] [AddGroup V] [AddGroup W] {f : U →+ V} {g : V →+ W} {σ : W → V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : ⇑g ∘ σ = _root_.id) (v : V) (u : U) : corrector hfg hgσ v = u ↔ v = σ (g v) + f u

theorem MonoidHom.image_corrector_eq_self_of_mem_ker {U : Type u_1} {V : Type u_2} {W : Type u_3} [Group U] [Group V] [Group W] {f : U →* V} {g : V →* W} {σ : W →* V} (hfg : f.range = g.ker) (hgσ : ⇑g ∘ ⇑σ = _root_.id) {v : V} (hv : v ∈ g.ker) : f (corrector hfg hgσ v) = v

theorem AddMonoidHom.image_corrector_eq_self_of_mem_ker {U : Type u_1} {V : Type u_2} {W : Type u_3} [AddGroup U] [AddGroup V] [AddGroup W] {f : U →+ V} {g : V →+ W} {σ : W →+ V} (hfg : f.range = g.ker) (hgσ : ⇑g ∘ ⇑σ = _root_.id) {v : V} (hv : v ∈ g.ker) : f (corrector hfg hgσ v) = v

theorem MonoidHom.corrector_one {U : Type u_1} {V : Type u_2} {W : Type u_3} [Group U] [Group V] [Group W] {f : U →* V} {g : V →* W} {σ : W →* V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : ⇑g ∘ ⇑σ = _root_.id) : corrector hfg hgσ 1 = 1

theorem AddMonoidHom.corrector_zero {U : Type u_1} {V : Type u_2} {W : Type u_3} [AddGroup U] [AddGroup V] [AddGroup W] {f : U →+ V} {g : V →+ W} {σ : W →+ V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : ⇑g ∘ ⇑σ = _root_.id) : corrector hfg hgσ 0 = 0

theorem MonoidHom.corrector_mul {U : Type u_1} {V : Type u_2} {W : Type u_3} [Group U] [CommGroup V] [Group W] {f : U →* V} {g : V →* W} {σ : W →* V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : ⇑g ∘ ⇑σ = _root_.id) (v₁ v₂ : V) : corrector hfg hgσ (v₁ * v₂) = corrector hfg hgσ v₁ * corrector hfg hgσ v₂

theorem AddMonoidHom.corrector_add {U : Type u_1} {V : Type u_2} {W : Type u_3} [AddGroup U] [AddCommGroup V] [AddGroup W] {f : U →+ V} {g : V →+ W} {σ : W →+ V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : ⇑g ∘ ⇑σ = _root_.id) (v₁ v₂ : V) : corrector hfg hgσ (v₁ + v₂) = corrector hfg hgσ v₁ + corrector hfg hgσ v₂

noncomputable def MonoidHom.correctorHom {U : Type u_1} {V : Type u_2} {W : Type u_3} [Group U] [CommGroup V] [Group W] {f : U →* V} {g : V →* W} {σ : W →* V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : g.comp σ = id W) : V →* U

The corrector homomorphism γ : V → U associated to a multiplicative section σ : W → V of a short exact sequence 1 ⟶ U ⟶ V ⟶ W ⟶ 1.

Equations

• MonoidHom.correctorHom hf hfg hgσ = { toFun := MonoidHom.corrector hfg ⋯, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def AddMonoidHom.correctorHom {U : Type u_1} {V : Type u_2} {W : Type u_3} [AddGroup U] [AddCommGroup V] [AddGroup W] {f : U →+ V} {g : V →+ W} {σ : W →+ V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : g.comp σ = id W) : V →+ U

The additive corrector homomorphism γ : V → U associated to an additive section σ : W → V of a short exact sequence 0 ⟶ U ⟶ V ⟶ W ⟶ 0.

Equations

• AddMonoidHom.correctorHom hf hfg hgσ = { toFun := AddMonoidHom.corrector hfg ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem MonoidHom.correctorHom_eq_iff {U : Type u_1} {V : Type u_2} {W : Type u_3} [Group U] [CommGroup V] [Group W] {f : U →* V} {g : V →* W} {σ : W →* V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : g.comp σ = id W) (v : V) (u : U) : (correctorHom hf hfg hgσ) v = u ↔ v = σ (g v) * f u

theorem AddMonoidHom.correctorHom_eq_iff {U : Type u_1} {V : Type u_2} {W : Type u_3} [AddGroup U] [AddCommGroup V] [AddGroup W] {f : U →+ V} {g : V →+ W} {σ : W →+ V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : g.comp σ = id W) (v : V) (u : U) : (correctorHom hf hfg hgσ) v = u ↔ v = σ (g v) + f u

theorem MonoidHom.image_correctorHom_eq_self_of_mem_ker {U : Type u_1} {V : Type u_2} {W : Type u_3} [Group U] [CommGroup V] [Group W] {f : U →* V} {g : V →* W} {σ : W →* V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : g.comp σ = id W) {v : V} (hv : v ∈ g.ker) : f ((correctorHom hf hfg hgσ) v) = v

theorem AddMonoidHom.image_correctorHom_eq_self_of_mem_ker {U : Type u_1} {V : Type u_2} {W : Type u_3} [AddGroup U] [AddCommGroup V] [AddGroup W] {f : U →+ V} {g : V →+ W} {σ : W →+ V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : g.comp σ = id W) {v : V} (hv : v ∈ g.ker) : f ((correctorHom hf hfg hgσ) v) = v

noncomputable def LinearMap.chooseSection {𝕜 : Type u_1} [CommSemiring 𝕜] {V : Type u_2} {W : Type u_3} [AddCommGroup V] [Module 𝕜 V] [AddCommGroup W] [Module 𝕜 W] [Module.Free 𝕜 W] {g : V →ₗ[𝕜] W} (hg : g.range = ⊤) : W →ₗ[𝕜] V

A choice of a linear section of a surjective linear map to a free module.

Equations

• LinearMap.chooseSection hg = ((Module.Free.chooseBasis 𝕜 W).constr 𝕜) fun (i : Module.Free.ChooseBasisIndex 𝕜 W) => ⋯.choose

theorem LinearMap.choose_section_prop {𝕜 : Type u_1} [CommSemiring 𝕜] {V : Type u_2} {W : Type u_3} [AddCommGroup V] [Module 𝕜 V] [AddCommGroup W] [Module 𝕜 W] [Module.Free 𝕜 W] {g : V →ₗ[𝕜] W} (hg : g.range = ⊤) : g ∘ₗ chooseSection hg = 1

theorem LinearMap.choose_section_prop_apply {𝕜 : Type u_1} [CommSemiring 𝕜] {V : Type u_2} {W : Type u_3} [AddCommGroup V] [Module 𝕜 V] [AddCommGroup W] [Module 𝕜 W] [Module.Free 𝕜 W] {g : V →ₗ[𝕜] W} (hg : g.range = ⊤) (w : W) : g ((chooseSection hg) w) = w

theorem LinearMap.correctorHom_smul {𝕜 : Type u_1} [Ring 𝕜] {U : Type u_2} {V : Type u_3} {W : Type u_4} [AddCommGroup U] [Module 𝕜 U] [AddCommGroup V] [Module 𝕜 V] [AddCommGroup W] [Module 𝕜 W] {f : U →ₗ[𝕜] V} {g : V →ₗ[𝕜] W} {σ : W →ₗ[𝕜] V} (hf : f.toAddMonoidHom.ker = ⊥) (hfg : f.toAddMonoidHom.range = g.toAddMonoidHom.ker) (hgσ : g.toAddMonoidHom.comp σ.toAddMonoidHom = AddMonoidHom.id W) (c : 𝕜) (v : V) : (AddMonoidHom.correctorHom hf hfg hgσ) (c • v) = c • (AddMonoidHom.correctorHom hf hfg hgσ) v

noncomputable def LinearMap.corrector {𝕜 : Type u_1} [Ring 𝕜] {U : Type u_2} {V : Type u_3} {W : Type u_4} [AddCommGroup U] [Module 𝕜 U] [AddCommGroup V] [Module 𝕜 V] [AddCommGroup W] [Module 𝕜 W] {f : U →ₗ[𝕜] V} {g : V →ₗ[𝕜] W} {σ : W →ₗ[𝕜] V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : g ∘ₗ σ = 1) : V →ₗ[𝕜] U

The corrector linear map γ : V → U associated to a linear section σ : W → V of a short exact sequence 0 ⟶ U ⟶ V ⟶ W ⟶ 0.

Equations

• LinearMap.corrector hf hfg hgσ = { toFun := ⇑(AddMonoidHom.correctorHom ⋯ ⋯ ⋯), map_add' := ⋯, map_smul' := ⋯ }

theorem LinearMap.corrector_spec {𝕜 : Type u_1} [Ring 𝕜] {U : Type u_2} {V : Type u_3} {W : Type u_4} [AddCommGroup U] [Module 𝕜 U] [AddCommGroup V] [Module 𝕜 V] [AddCommGroup W] [Module 𝕜 W] {f : U →ₗ[𝕜] V} {g : V →ₗ[𝕜] W} {σ : W →ₗ[𝕜] V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : g ∘ₗ σ = 1) (v : V) : v = σ (g v) + f ((corrector hf hfg hgσ) v)

The corrector map γ : V → U satisfies v = σ(g(v)) + f(γ(v)) for any v : V.

theorem LinearMap.corrector_eq_iff {𝕜 : Type u_1} [Ring 𝕜] {U : Type u_2} {V : Type u_3} {W : Type u_4} [AddCommGroup U] [Module 𝕜 U] [AddCommGroup V] [Module 𝕜 V] [AddCommGroup W] [Module 𝕜 W] {f : U →ₗ[𝕜] V} {g : V →ₗ[𝕜] W} {σ : W →ₗ[𝕜] V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : g ∘ₗ σ = 1) (v : V) (u : U) : (corrector hf hfg hgσ) v = u ↔ v = σ (g v) + f u

theorem LinearMap.image_corrector_eq_self_of_mem_ker {𝕜 : Type u_1} [Ring 𝕜] {U : Type u_2} {V : Type u_3} {W : Type u_4} [AddCommGroup U] [Module 𝕜 U] [AddCommGroup V] [Module 𝕜 V] [AddCommGroup W] [Module 𝕜 W] {f : U →ₗ[𝕜] V} {g : V →ₗ[𝕜] W} {σ : W →ₗ[𝕜] V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : g ∘ₗ σ = 1) {v : V} (hv : v ∈ g.ker) : f ((corrector hf hfg hgσ) v) = v

theorem ses_directSum_isInternal {𝕜 : Type u_1} [Ring 𝕜] {U : Type u_2} {V : Type u_3} {W : Type u_4} [AddCommGroup U] [Module 𝕜 U] [AddCommGroup V] [Module 𝕜 V] [AddCommGroup W] [Module 𝕜 W] {f : U →ₗ[𝕜] V} {g : V →ₗ[𝕜] W} {σ : W →ₗ[𝕜] V} (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : g ∘ₗ σ = 1) : DirectSum.IsInternal fun (j : Bool) => if j = true then f.range else σ.range

A short exact sequence of modules together with a section gives an internal direct sum decomposition.

noncomputable def sesBasis' {𝕜 : Type u_1} [Ring 𝕜] {U : Type u_2} {V : Type u_3} {W : Type u_4} [AddCommGroup U] [Module 𝕜 U] [AddCommGroup V] [Module 𝕜 V] [AddCommGroup W] [Module 𝕜 W] {f : U →ₗ[𝕜] V} {g : V →ₗ[𝕜] W} {σ : W →ₗ[𝕜] V} {ιU ιW : Type u} (basU : Module.Basis ιU 𝕜 U) (basW : Module.Basis ιW 𝕜 W) (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : g ∘ₗ σ = 1) : Module.Basis ((j' : Bool) × (fun (j : Bool) => if j = true then ιU else ιW) j') 𝕜 V

From a short exact sequence of modules, a section of it, we can construct a basis of the middle module from bases of the two other modules. (See sesBasis for a more conveniently indexed basis.)

Equations

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

noncomputable def sesBasis {𝕜 : Type u_1} [Ring 𝕜] {U : Type u_2} {V : Type u_3} {W : Type u_4} [AddCommGroup U] [Module 𝕜 U] [AddCommGroup V] [Module 𝕜 V] [AddCommGroup W] [Module 𝕜 W] {f : U →ₗ[𝕜] V} {g : V →ₗ[𝕜] W} {σ : W →ₗ[𝕜] V} {ιU ιW : Type u} (basU : Module.Basis ιU 𝕜 U) (basW : Module.Basis ιW 𝕜 W) (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : g ∘ₗ σ = 1) : Module.Basis (ιU ⊕ ιW) 𝕜 V

From a short exact sequence of modules, a section of it, we can construct a basis of the middle module from bases of the two other modules.

Equations

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

@[simp]

theorem ses_basis_eq_of_left {𝕜 : Type u_1} [Ring 𝕜] {U : Type u_2} {V : Type u_3} {W : Type u_4} [AddCommGroup U] [Module 𝕜 U] [AddCommGroup V] [Module 𝕜 V] [AddCommGroup W] [Module 𝕜 W] {f : U →ₗ[𝕜] V} {g : V →ₗ[𝕜] W} {σ : W →ₗ[𝕜] V} {ιU ιW : Type u} (basU : Module.Basis ιU 𝕜 U) (basW : Module.Basis ιW 𝕜 W) (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : g ∘ₗ σ = 1) (iu : ιU) : (sesBasis basU basW hf hfg hgσ) (Sum.inl iu) = f (basU iu)

@[simp]

theorem ses_basis_eq_of_right {𝕜 : Type u_1} [Ring 𝕜] {U : Type u_2} {V : Type u_3} {W : Type u_4} [AddCommGroup U] [Module 𝕜 U] [AddCommGroup V] [Module 𝕜 V] [AddCommGroup W] [Module 𝕜 W] {f : U →ₗ[𝕜] V} {g : V →ₗ[𝕜] W} {σ : W →ₗ[𝕜] V} {ιU ιW : Type u} (basU : Module.Basis ιU 𝕜 U) (basW : Module.Basis ιW 𝕜 W) (hf : f.ker = ⊥) (hfg : f.range = g.ker) (hgσ : g ∘ₗ σ = 1) (iw : ιW) : (sesBasis basU basW hf hfg hgσ) (Sum.inr iw) = σ (basW iw)