Exactness of a pair #
For two maps
f : M → Nandg : N → P, withZero P,Function.Exact f gsays thatSet.range f = Set.preimage g {0}For additive maps
f : M →+ Nandg : N →+ P,Exact f gsays thatrange f = ker gFor linear maps
f : M →ₗ[R] Nandg : N →ₗ[R] P,Exact f gsays thatrange f = ker g
TODO : #
generalize to
SemilinearMap, evenSemilinearMapClassadd the multiplicative case (
Function.Exactwill becomeFunction.AddExact?)
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)
:
theorem
Function.Exact.comp_injective
{M : Type u_2}
{N : Type u_4}
{P : Type u_6}
{P' : Type u_7}
{f : M → N}
{g : N → P}
(g' : P → P')
[Zero P]
[Zero P']
(exact : Function.Exact f g)
(inj : Function.Injective g')
(h0 : g' 0 = 0)
:
Function.Exact f (g' ∘ g)
theorem
AddMonoidHom.exact_iff_of_surjective_of_bijective_of_injective
{M₁ : Type u_8}
{M₂ : Type u_9}
{M₃ : Type u_10}
{N₁ : Type u_11}
{N₂ : Type u_12}
{N₃ : Type u_13}
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid N₁]
[AddCommMonoid N₂]
[AddCommMonoid N₃]
(f : M₁ →+ M₂)
(g : M₂ →+ M₃)
(f' : N₁ →+ N₂)
(g' : N₂ →+ N₃)
(τ₁ : M₁ →+ N₁)
(τ₂ : M₂ →+ N₂)
(τ₃ : M₃ →+ N₃)
(comm₁₂ : f'.comp τ₁ = τ₂.comp f)
(comm₂₃ : g'.comp τ₂ = τ₃.comp g)
(h₁ : Function.Surjective ⇑τ₁)
(h₂ : Function.Bijective ⇑τ₂)
(h₃ : Function.Injective ⇑τ₃)
:
Function.Exact ⇑f ⇑g ↔ Function.Exact ⇑f' ⇑g'
When we have a commutative diagram from a sequence of two maps to another,
such that the left vertical map is surjective, the middle vertical map is bijective and the right
vertical map is injective, then the upper row is exact iff the lower row is.
See ShortComplex.exact_iff_of_epi_of_isIso_of_mono in the file
Algebra.Homology.ShortComplex.Exact for the categorical version of this result.
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
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
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
LinearMap.exact_subtype_mkQ
{R : Type u_8}
{N : Type u_10}
[CommRing R]
[AddCommGroup N]
[Module R N]
(Q : Submodule R N)
:
Function.Exact ⇑Q.subtype ⇑Q.mkQ
theorem
LinearMap.exact_map_mkQ_range
{R : Type u_8}
{M : Type u_9}
{N : Type u_10}
[CommRing R]
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(f : M →ₗ[R] N)
:
Function.Exact ⇑f ⇑(LinearMap.range f).mkQ
theorem
LinearMap.exact_subtype_ker_map
{R : Type u_8}
{N : Type u_10}
{P : Type u_11}
[CommRing R]
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(g : N →ₗ[R] P)
:
Function.Exact ⇑(LinearMap.ker g).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}
[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)
:
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)
:
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)
:
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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
:
Function.Exact ⇑(LinearMap.inr R M N) ⇑(LinearMap.fst R M N)
theorem
Function.Exact.inl_snd
{R : Type u_1}
{M : Type u_2}
{N : Type u_4}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
:
Function.Exact ⇑(LinearMap.inl R M N) ⇑(LinearMap.snd R M 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]
[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.
theorem
LinearMap.exact_iff_of_surjective_of_bijective_of_injective
{R : Type u_1}
[Ring R]
{M₁ : Type u_8}
{M₂ : Type u_9}
{M₃ : Type u_10}
{N₁ : Type u_11}
{N₂ : Type u_12}
{N₃ : Type u_13}
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid N₁]
[AddCommMonoid N₂]
[AddCommMonoid N₃]
[Module R M₁]
[Module R M₂]
[Module R M₃]
[Module R N₁]
[Module R N₂]
[Module R N₃]
(f : M₁ →ₗ[R] M₂)
(g : M₂ →ₗ[R] M₃)
(f' : N₁ →ₗ[R] N₂)
(g' : N₂ →ₗ[R] N₃)
(τ₁ : M₁ →ₗ[R] N₁)
(τ₂ : M₂ →ₗ[R] N₂)
(τ₃ : M₃ →ₗ[R] N₃)
(comm₁₂ : f' ∘ₗ τ₁ = τ₂ ∘ₗ f)
(comm₂₃ : g' ∘ₗ τ₂ = τ₃ ∘ₗ g)
(h₁ : Function.Surjective ⇑τ₁)
(h₂ : Function.Bijective ⇑τ₂)
(h₃ : Function.Injective ⇑τ₃)
:
Function.Exact ⇑f ⇑g ↔ Function.Exact ⇑f' ⇑g'
When we have a commutative diagram from a sequence of two linear maps to another,
such that the left vertical map is surjective, the middle vertical map is bijective and the right
vertical map is injective, then the upper row is exact iff the lower row is.
See ShortComplex.exact_iff_of_epi_of_isIso_of_mono in the file
Algebra.Homology.ShortComplex.Exact for the categorical version of this result.
theorem
LinearMap.surjective_range_liftQ
{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}
(h : LinearMap.range f ≤ LinearMap.ker g)
(hg : Function.Surjective ⇑g)
:
Function.Surjective ⇑((LinearMap.range f).liftQ g h)
theorem
LinearMap.ker_eq_bot_range_liftQ_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}
(h : LinearMap.range f ≤ LinearMap.ker g)
:
LinearMap.ker ((LinearMap.range f).liftQ g h) = ⊥ ↔ LinearMap.ker g = LinearMap.range f
theorem
LinearMap.injective_range_liftQ_of_exact
{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}
(h : Function.Exact ⇑f ⇑g)
:
Function.Injective ⇑((LinearMap.range f).liftQ g ⋯)
noncomputable def
Function.Exact.linearEquivOfSurjective
{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}
(h : Function.Exact ⇑f ⇑g)
(hg : Function.Surjective ⇑g)
:
(N ⧸ LinearMap.range f) ≃ₗ[R] P
The linear equivalence (N ⧸ LinearMap.range f) ≃ₗ[A] P associated to
an exact sequence M → N → P → 0 of R-modules.
Equations
- h.linearEquivOfSurjective hg = LinearEquiv.ofBijective ((LinearMap.range f).liftQ g ⋯) ⋯
Instances For
@[simp]
theorem
Function.Exact.linearEquivOfSurjective_apply
{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}
(h : Function.Exact ⇑f ⇑g)
(hg : Function.Surjective ⇑g)
(a✝ : N ⧸ LinearMap.range f)
:
(h.linearEquivOfSurjective hg) a✝ = ((LinearMap.range f).liftQ g ⋯) a✝