# 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 additive maps f : M →+ N and g : N →+ P, Exact f g says that range f = ker g

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

## TODO : #

• 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 : MN) (g : NP) [Zero P] :

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

Equations
Instances For
theorem Function.Exact.apply_apply_eq_zero {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : MN} {g : NP} [Zero P] (h : ) (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 : MN} {g : NP} [Zero P] (h : ) :
g f = 0
theorem Function.Exact.of_comp_of_mem_range {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : MN} {g : NP} [Zero P] (h1 : g f = 0) (h2 : ∀ (x : N), g x = 0x ) :
theorem Function.Exact.comp_injective {M : Type u_2} {N : Type u_4} {P : Type u_6} {P' : Type u_7} {f : MN} {g : NP} (g' : PP') [Zero P] [Zero P'] (exact : ) (inj : ) (h0 : g' 0 = 0) :
theorem Function.Exact.of_comp_eq_zero_of_ker_in_range {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : MN} {g : NP} [Zero P] (hc : g f = 0) (hr : ∀ (y : N), g y = 0y ) :
theorem AddMonoidHom.exact_iff {M : Type u_2} {N : Type u_4} {P : Type u_6} [] [] [] {f : M →+ N} {g : N →+ P} :
Function.Exact f g g.ker = f.range
theorem AddMonoidHom.exact_of_comp_eq_zero_of_ker_le_range {M : Type u_2} {N : Type u_4} {P : Type u_6} [] [] [] {f : M →+ N} {g : N →+ P} (h1 : g.comp f = 0) (h2 : g.ker f.range) :
Function.Exact f g
theorem AddMonoidHom.exact_of_comp_of_mem_range {M : Type u_2} {N : Type u_4} {P : Type u_6} [] [] [] {f : M →+ N} {g : N →+ P} (h1 : g.comp f = 0) (h2 : ∀ (x : N), g x = 0x f.range) :
Function.Exact f g
theorem Function.Exact.addMonoidHom_ker_eq {M : Type u_2} {N : Type u_4} {P : Type u_6} [] [] [] {f : M →+ N} {g : N →+ P} (hfg : Function.Exact f g) :
g.ker = f.range
theorem Function.Exact.addMonoidHom_comp_eq_zero {M : Type u_2} {N : Type u_4} {P : Type u_6} [] [] [] {f : M →+ N} {g : N →+ P} (h : Function.Exact f g) :
g.comp f = 0
theorem Function.Exact.of_ladder_addEquiv_of_exact {X₁ : Type u_8} {X₂ : Type u_9} {X₃ : Type u_10} {Y₁ : Type u_11} {Y₂ : Type u_12} {Y₃ : Type u_13} [] [] [] [] [] [] (e₁ : X₁ ≃+ Y₁) (e₂ : X₂ ≃+ Y₂) (e₃ : X₃ ≃+ Y₃) {f₁₂ : X₁ →+ X₂} {f₂₃ : X₂ →+ X₃} {g₁₂ : Y₁ →+ Y₂} {g₂₃ : Y₂ →+ Y₃} (comm₁₂ : g₁₂.comp e₁ = (↑e₂).comp f₁₂) (comm₂₃ : g₂₃.comp e₂ = (↑e₃).comp f₂₃) (H : Function.Exact f₁₂ f₂₃) :
Function.Exact g₁₂ g₂₃
theorem Function.Exact.of_ladder_addEquiv_of_exact' {X₁ : Type u_8} {X₂ : Type u_9} {X₃ : Type u_10} {Y₁ : Type u_11} {Y₂ : Type u_12} {Y₃ : Type u_13} [] [] [] [] [] [] (e₁ : X₁ ≃+ Y₁) (e₂ : X₂ ≃+ Y₂) (e₃ : X₃ ≃+ Y₃) {f₁₂ : X₁ →+ X₂} {f₂₃ : X₂ →+ X₃} {g₁₂ : Y₁ →+ Y₂} {g₂₃ : Y₂ →+ Y₃} (comm₁₂ : g₁₂.comp e₁ = (↑e₂).comp f₁₂) (comm₂₃ : g₂₃.comp e₂ = (↑e₃).comp f₂₃) (H : Function.Exact g₁₂ g₂₃) :
Function.Exact f₁₂ f₂₃
theorem Function.Exact.iff_of_ladder_addEquiv {X₁ : Type u_8} {X₂ : Type u_9} {X₃ : Type u_10} {Y₁ : Type u_11} {Y₂ : Type u_12} {Y₃ : Type u_13} [] [] [] [] [] [] (e₁ : X₁ ≃+ Y₁) (e₂ : X₂ ≃+ Y₂) (e₃ : X₃ ≃+ Y₃) {f₁₂ : X₁ →+ X₂} {f₂₃ : X₂ →+ X₃} {g₁₂ : Y₁ →+ Y₂} {g₂₃ : Y₂ →+ Y₃} (comm₁₂ : g₁₂.comp e₁ = (↑e₂).comp f₁₂) (comm₂₃ : g₂₃.comp e₂ = (↑e₃).comp f₂₃) :
Function.Exact g₁₂ g₂₃ Function.Exact f₁₂ f₂₃
theorem LinearMap.exact_iff {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [] [] [] [] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} :
Function.Exact f g
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} [] [] [] [] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h1 : g ∘ₗ f = 0) (h2 : ) :
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} [] [] [] [] [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) :
Function.Exact f g
theorem LinearMap.exact_subtype_mkQ {R : Type u_8} {N : Type u_10} [] [] [Module R N] (Q : ) :
Function.Exact Q.subtype Q.mkQ
theorem LinearMap.exact_map_mkQ_range {R : Type u_8} {M : Type u_9} {N : Type u_10} [] [] [] [Module R M] [Module R N] (f : M →ₗ[R] N) :
Function.Exact f .mkQ
theorem LinearMap.exact_subtype_ker_map {R : Type u_8} {N : Type u_10} {P : Type u_11} [] [] [] [Module R N] [Module R P] (g : N →ₗ[R] P) :
Function.Exact .subtype 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} [] [] [] [] [] [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.linearMap_ker_eq {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [] [] [] [] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (hfg : 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} [] [] [] [] [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} [] [] [] [] [] [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.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} [] [] [] [] [] [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.Exact f (i ∘ₗ g) Function.Exact f 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} [] [] [] [] [] [] [] [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₂₃
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} [] [] [] [] [] [] [] [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₂₃
noncomputable def Function.Exact.splitSurjectiveEquiv {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [] [] [] [] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact f g) (hf : ) :
{ l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id } { e : N ≃ₗ[R] M × P // f = e.symm ∘ₗ g = ∘ₗ 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.
Instances For
noncomputable def Function.Exact.splitInjectiveEquiv {R : Type u_8} {M : Type u_9} {N : Type u_10} {P : Type u_11} [] [] [] [] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact f g) (hg : ) :
{ l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id } { e : N ≃ₗ[R] M × P // f = e.symm ∘ₗ g = ∘ₗ 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.
Instances For
theorem Function.Exact.split_tfae' {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [] [] [] [] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact f 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 ∘ₗ g = ∘ₗ e].TFAE
theorem Function.Exact.split_tfae {R : Type u_8} {M : Type u_9} {N : Type u_10} {P : Type u_11} [] [] [] [] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact f g) (hf : ) (hg : ) :
[∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id, ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id, ∃ (e : N ≃ₗ[R] M × P), f = e.symm ∘ₗ g = ∘ₗ e].TFAE

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

theorem Function.Exact.inr_fst {R : Type u_1} {M : Type u_2} {N : Type u_4} [] [] [] [Module R M] [Module R N] :
theorem Function.Exact.inl_snd {R : Type u_1} {M : Type u_2} {N : Type u_4} [] [] [] [Module R M] [Module R N] :
theorem Function.Exact.exact_mapQ_iff {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [Ring R] [] [] [] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (hfg : Function.Exact f g) {p : } {q : } {r : } (hpq : p ) (hqr : q ) :
Function.Exact (p.mapQ q f hpq) (q.mapQ r g hqr)

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