Exactness of a pair

• For two maps f : M → N and g : N → P, with Zero P, Function.Exact f g says that Set.range f = Set.preimage g {0}

• For linear maps f : M →ₗ[R] N and g : N →ₗ[R] P, Exact f g says that range f = ker g

TODO :

• add the cases of AddMonoidHom

• generalize to SemilinearMap, even SemilinearMapClass

• add the multiplicative case (Function.Exact will become Function.AddExact?)

def Function.Exact {M : Type u_2} {N : Type u_4} {P : Type u_6} (f : M → N) (g : N → P) [Zero P] : Prop

The maps f and g form an exact pair : g y = 0 iff y belongs to the image of f

Equations

• Function.Exact f g = ∀ (y : N), g y = 0 ↔ y ∈ Set.range f

theorem Function.Exact.apply_apply_eq_zero {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [Zero P] (h : Function.Exact f g) (x : M) : g (f x) = 0

theorem Function.Exact.comp_eq_zero {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [Zero P] (h : Function.Exact f g) : g ∘ f = 0

theorem Function.Exact.of_comp_of_mem_range {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [Zero P] (h1 : g ∘ f = 0) (h2 : ∀ (x : N), g x = 0 → x ∈ Set.range f) : Function.Exact f g

theorem Function.Exact.of_comp_eq_zero_of_ker_in_range {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [Zero P] (hc : g ∘ f = 0) (hr : ∀ (y : N), g y = 0 → y ∈ Set.range f) : Function.Exact f g

theorem Function.Exact.linearMap_ker_eq {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (hfg : Function.Exact ⇑f ⇑g) : LinearMap.ker g = LinearMap.range f

theorem LinearMap.exact_iff {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} : Function.Exact ⇑f ⇑g ↔ LinearMap.ker g = LinearMap.range f

theorem LinearMap.exact_of_comp_eq_zero_of_ker_le_range {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h1 : g ∘ₗ f = 0) (h2 : LinearMap.ker g ≤ LinearMap.range f) : Function.Exact ⇑f ⇑g

theorem LinearMap.exact_of_comp_of_mem_range {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h1 : g ∘ₗ f = 0) (h2 : ∀ (x : N), g x = 0 → x ∈ LinearMap.range f) : Function.Exact ⇑f ⇑g

theorem Function.Exact.linearMap_comp_eq_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact ⇑f ⇑g) : g ∘ₗ f = 0

theorem Function.Surjective.comp_exact_iff_exact {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {P : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R M'] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} {p : M' →ₗ[R] M} (h : Function.Surjective ⇑p) : Function.Exact ⇑(f ∘ₗ p) ⇑g ↔ Function.Exact ⇑f ⇑g

theorem Function.Injective.comp_exact_iff_exact {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} {P' : Type u_7} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid P'] [Module R M] [Module R N] [Module R P] [Module R P'] {f : M →ₗ[R] N} {g : N →ₗ[R] P} {i : P →ₗ[R] P'} (h : Function.Injective ⇑i) : Function.Exact ⇑f ⇑(i ∘ₗ g) ↔ Function.Exact ⇑f ⇑g

theorem LinearEquiv.conj_exact_iff_exact {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {P : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid N'] [AddCommMonoid P] [Module R M] [Module R N] [Module R N'] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (e : N ≃ₗ[R] N') : Function.Exact ⇑(↑e ∘ₗ f) ⇑(g ∘ₗ ↑e.symm) ↔ Function.Exact ⇑f ⇑g

theorem Function.Exact.of_ladder_linearEquiv_of_exact {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {N' : Type u_5} {P : Type u_6} {P' : Type u_7} [Semiring R] [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid N] [AddCommMonoid N'] [AddCommMonoid P] [AddCommMonoid P'] [Module R M] [Module R M'] [Module R N] [Module R N'] [Module R P] [Module R P'] {f₁₂ : M →ₗ[R] N} {f₂₃ : N →ₗ[R] P} {g₁₂ : M' →ₗ[R] N'} {g₂₃ : N' →ₗ[R] P'} {e₁ : M ≃ₗ[R] M'} {e₂ : N ≃ₗ[R] N'} {e₃ : P ≃ₗ[R] P'} (h₁₂ : g₁₂ ∘ₗ ↑e₁ = ↑e₂ ∘ₗ f₁₂) (h₂₃ : g₂₃ ∘ₗ ↑e₂ = ↑e₃ ∘ₗ f₂₃) (H : Function.Exact ⇑f₁₂ ⇑f₂₃) : Function.Exact ⇑g₁₂ ⇑g₂₃

theorem Function.Exact.iff_of_ladder_linearEquiv {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {N' : Type u_5} {P : Type u_6} {P' : Type u_7} [Semiring R] [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid N] [AddCommMonoid N'] [AddCommMonoid P] [AddCommMonoid P'] [Module R M] [Module R M'] [Module R N] [Module R N'] [Module R P] [Module R P'] {f₁₂ : M →ₗ[R] N} {f₂₃ : N →ₗ[R] P} {g₁₂ : M' →ₗ[R] N'} {g₂₃ : N' →ₗ[R] P'} {e₁ : M ≃ₗ[R] M'} {e₂ : N ≃ₗ[R] N'} {e₃ : P ≃ₗ[R] P'} (h₁₂ : g₁₂ ∘ₗ ↑e₁ = ↑e₂ ∘ₗ f₁₂) (h₂₃ : g₂₃ ∘ₗ ↑e₂ = ↑e₃ ∘ₗ f₂₃) : Function.Exact ⇑g₁₂ ⇑g₂₃ ↔ Function.Exact ⇑f₁₂ ⇑f₂₃

noncomputable def Function.Exact.splitSurjectiveEquiv {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [Semiring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id } ≃ { e : N ≃ₗ[R] M × P // f = ↑e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ ↑e }

Given an exact sequence 0 → M → N → P, giving a section P → N is equivalent to giving a splitting N ≃ M × P.

Equations

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

noncomputable def Function.Exact.splitInjectiveEquiv {R : Type u_8} {M : Type u_9} {N : Type u_10} {P : Type u_11} [Semiring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id } ≃ { e : N ≃ₗ[R] M × P // f = ↑e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ ↑e }

Given an exact sequence M → N → P → 0, giving a retraction N → M is equivalent to giving a splitting N ≃ M × P.

Equations

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

theorem Function.Exact.split_tfae' {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [Semiring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact ⇑f ⇑g) : [Function.Injective ⇑f ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id, Function.Surjective ⇑g ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id, ∃ (e : N ≃ₗ[R] M × P), f = ↑e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ ↑e].TFAE

theorem Function.Exact.split_tfae {R : Type u_8} {M : Type u_9} {N : Type u_10} {P : Type u_11} [Semiring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) : [∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id, ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id, ∃ (e : N ≃ₗ[R] M × P), f = ↑e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ ↑e].TFAE

Equivalent characterizations of split exact sequences. Also known as the Splitting lemma.

theorem Function.Exact.exact_mapQ_iff {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [Ring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (hfg : Function.Exact ⇑f ⇑g) {p : Submodule R M} {q : Submodule R N} {r : Submodule R P} (hpq : p ≤ Submodule.comap f q) (hqr : q ≤ Submodule.comap g r) : Function.Exact ⇑(p.mapQ q f hpq) ⇑(q.mapQ r g hqr) ↔ LinearMap.range g ⊓ r ≤ Submodule.map g q

A necessary and sufficient condition for an exact sequence to descend to a quotient.