Documentation

Mathlib.Algebra.Exact

Exactness of a pair #

TODO : #

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 : 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 : MN} {g : NP} [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 : MN} {g : NP} [Zero P] (h1 : g f = 0) (h2 : ∀ (x : N), g x = 0x Set.range f) :
    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 : Function.Exact f g) (inj : Function.Injective g') (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 Set.range f) :
    theorem AddMonoidHom.exact_iff {M : Type u_2} {N : Type u_4} {P : Type u_6} [AddGroup M] [AddGroup N] [AddGroup P] {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} [AddGroup M] [AddGroup N] [AddGroup P] {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} [AddGroup M] [AddGroup N] [AddGroup P] {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} [AddGroup M] [AddGroup N] [AddGroup P] {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} [AddGroup M] [AddGroup N] [AddGroup P] {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} [AddCommMonoid X₁] [AddCommMonoid X₂] [AddCommMonoid X₃] [AddCommMonoid Y₁] [AddCommMonoid Y₂] [AddCommMonoid Y₃] (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} [AddCommMonoid X₁] [AddCommMonoid X₂] [AddCommMonoid X₃] [AddCommMonoid Y₁] [AddCommMonoid Y₂] [AddCommMonoid Y₃] (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} [AddCommMonoid X₁] [AddCommMonoid X₂] [AddCommMonoid X₃] [AddCommMonoid Y₁] [AddCommMonoid Y₂] [AddCommMonoid Y₃] (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} [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} :
    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 = 0x LinearMap.range f) :
    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.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) :
    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 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₂₃
    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₂₃
    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.
    Instances For
      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.
      Instances For
        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.