Local properties about linear maps #
In this file, we show that injectivity, surjectivity, bijectivity and exactness of linear maps are local properties. More precisely, we show that these can be checked at maximal ideals and on standard covers.
theorem
injective_of_isLocalized_maximal
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5)
[(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
[(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)]
(f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P)
[∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)]
(Nₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_6)
[(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)]
[(P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)]
(g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P)
[∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (g P)]
(F : M →ₗ[R] N)
(H : ∀ (P : Ideal R) [inst : P.IsMaximal], Function.Injective ⇑((IsLocalizedModule.map P.primeCompl (f P) (g P)) F))
:
theorem
surjective_of_isLocalized_maximal
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5)
[(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
[(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)]
(f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P)
[∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)]
(Nₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_6)
[(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)]
[(P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)]
(g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P)
[∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (g P)]
(F : M →ₗ[R] N)
(H : ∀ (P : Ideal R) [inst : P.IsMaximal], Function.Surjective ⇑((IsLocalizedModule.map P.primeCompl (f P) (g P)) F))
:
theorem
bijective_of_isLocalized_maximal
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5)
[(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
[(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)]
(f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P)
[∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)]
(Nₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_6)
[(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)]
[(P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)]
(g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P)
[∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (g P)]
(F : M →ₗ[R] N)
(H : ∀ (P : Ideal R) [inst : P.IsMaximal], Function.Bijective ⇑((IsLocalizedModule.map P.primeCompl (f P) (g P)) F))
:
theorem
exact_of_isLocalized_maximal
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{L : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
[AddCommMonoid L]
[Module R L]
(Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5)
[(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
[(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)]
(f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P)
[∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)]
(Nₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_6)
[(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)]
[(P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)]
(g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P)
[∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (g P)]
(Lₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_7)
[(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)]
[(P : Ideal R) → [inst : P.IsMaximal] → Module R (Lₚ P)]
(h : (P : Ideal R) → [inst : P.IsMaximal] → L →ₗ[R] Lₚ P)
[∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (h P)]
(F : M →ₗ[R] N)
(G : N →ₗ[R] L)
(H :
∀ (J : Ideal R) [inst : J.IsMaximal],
Function.Exact ⇑((IsLocalizedModule.map J.primeCompl (f J) (g J)) F)
⇑((IsLocalizedModule.map J.primeCompl (g J) (h J)) G))
:
Function.Exact ⇑F ⇑G
theorem
injective_of_localized_maximal
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(f : M →ₗ[R] N)
(h : ∀ (J : Ideal R) [inst : J.IsMaximal], Function.Injective ⇑((LocalizedModule.map J.primeCompl) f))
:
theorem
surjective_of_localized_maximal
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(f : M →ₗ[R] N)
(h : ∀ (J : Ideal R) [inst : J.IsMaximal], Function.Surjective ⇑((LocalizedModule.map J.primeCompl) f))
:
theorem
bijective_of_localized_maximal
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(f : M →ₗ[R] N)
(h : ∀ (J : Ideal R) [inst : J.IsMaximal], Function.Bijective ⇑((LocalizedModule.map J.primeCompl) f))
:
theorem
exact_of_localized_maximal
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{L : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
[AddCommMonoid L]
[Module R L]
(f : M →ₗ[R] N)
(g : N →ₗ[R] L)
(h :
∀ (J : Ideal R) [inst : J.IsMaximal],
Function.Exact ⇑((LocalizedModule.map J.primeCompl) f) ⇑((LocalizedModule.map J.primeCompl) g))
:
Function.Exact ⇑f ⇑g
theorem
injective_of_isLocalized_span
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(s : Set R)
(spn : Ideal.span s = ⊤)
(Mₚ : ↑s → Type u_5)
[(r : ↑s) → AddCommMonoid (Mₚ r)]
[(r : ↑s) → Module R (Mₚ r)]
(f : (r : ↑s) → M →ₗ[R] Mₚ r)
[∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)]
(Nₚ : ↑s → Type u_6)
[(r : ↑s) → AddCommMonoid (Nₚ r)]
[(r : ↑s) → Module R (Nₚ r)]
(g : (r : ↑s) → N →ₗ[R] Nₚ r)
[∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (g r)]
(F : M →ₗ[R] N)
(H : ∀ (r : ↑s), Function.Injective ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F))
:
theorem
surjective_of_isLocalized_span
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(s : Set R)
(spn : Ideal.span s = ⊤)
(Mₚ : ↑s → Type u_5)
[(r : ↑s) → AddCommMonoid (Mₚ r)]
[(r : ↑s) → Module R (Mₚ r)]
(f : (r : ↑s) → M →ₗ[R] Mₚ r)
[∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)]
(Nₚ : ↑s → Type u_6)
[(r : ↑s) → AddCommMonoid (Nₚ r)]
[(r : ↑s) → Module R (Nₚ r)]
(g : (r : ↑s) → N →ₗ[R] Nₚ r)
[∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (g r)]
(F : M →ₗ[R] N)
(H : ∀ (r : ↑s), Function.Surjective ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F))
:
theorem
bijective_of_isLocalized_span
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(s : Set R)
(spn : Ideal.span s = ⊤)
(Mₚ : ↑s → Type u_5)
[(r : ↑s) → AddCommMonoid (Mₚ r)]
[(r : ↑s) → Module R (Mₚ r)]
(f : (r : ↑s) → M →ₗ[R] Mₚ r)
[∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)]
(Nₚ : ↑s → Type u_6)
[(r : ↑s) → AddCommMonoid (Nₚ r)]
[(r : ↑s) → Module R (Nₚ r)]
(g : (r : ↑s) → N →ₗ[R] Nₚ r)
[∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (g r)]
(F : M →ₗ[R] N)
(H : ∀ (r : ↑s), Function.Bijective ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F))
:
theorem
exact_of_isLocalized_span
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{L : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
[AddCommMonoid L]
[Module R L]
(s : Set R)
(spn : Ideal.span s = ⊤)
(Mₚ : ↑s → Type u_5)
[(r : ↑s) → AddCommMonoid (Mₚ r)]
[(r : ↑s) → Module R (Mₚ r)]
(f : (r : ↑s) → M →ₗ[R] Mₚ r)
[∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)]
(Nₚ : ↑s → Type u_6)
[(r : ↑s) → AddCommMonoid (Nₚ r)]
[(r : ↑s) → Module R (Nₚ r)]
(g : (r : ↑s) → N →ₗ[R] Nₚ r)
[∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (g r)]
(Lₚ : ↑s → Type u_7)
[(r : ↑s) → AddCommMonoid (Lₚ r)]
[(r : ↑s) → Module R (Lₚ r)]
(h : (r : ↑s) → L →ₗ[R] Lₚ r)
[∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (h r)]
(F : M →ₗ[R] N)
(G : N →ₗ[R] L)
(H :
∀ (r : ↑s),
Function.Exact ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)
⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G))
:
Function.Exact ⇑F ⇑G
theorem
injective_of_localized_span
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(s : Set R)
(spn : Ideal.span s = ⊤)
(f : M →ₗ[R] N)
(h : ∀ (r : ↑s), Function.Injective ⇑((LocalizedModule.map (Submonoid.powers ↑r)) f))
:
theorem
surjective_of_localized_span
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(s : Set R)
(spn : Ideal.span s = ⊤)
(f : M →ₗ[R] N)
(h : ∀ (r : ↑s), Function.Surjective ⇑((LocalizedModule.map (Submonoid.powers ↑r)) f))
:
theorem
bijective_of_localized_span
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(s : Set R)
(spn : Ideal.span s = ⊤)
(f : M →ₗ[R] N)
(h : ∀ (r : ↑s), Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers ↑r)) f))
:
theorem
exact_of_localized_span
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{L : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
[AddCommMonoid L]
[Module R L]
(s : Set R)
(spn : Ideal.span s = ⊤)
(f : M →ₗ[R] N)
(g : N →ₗ[R] L)
(h :
∀ (r : ↑s),
Function.Exact ⇑((LocalizedModule.map (Submonoid.powers ↑r)) f) ⇑((LocalizedModule.map (Submonoid.powers ↑r)) g))
:
Function.Exact ⇑f ⇑g