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
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}
:
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.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✝