Basic results on finitely generated (sub)modules #
This file contains the basic results on Submodule.FG and Module.Finite that do not need heavy
further imports.
theorem
Submodule.fg_bot
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
⊥.FG
theorem
Submodule.fg_span
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
(hs : s.Finite)
:
(Submodule.span R s).FG
theorem
Submodule.fg_span_singleton
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(x : M)
:
(Submodule.span R {x}).FG
theorem
Submodule.FG.sup
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{N₁ N₂ : Submodule R M}
(hN₁ : N₁.FG)
(hN₂ : N₂.FG)
:
(N₁ ⊔ N₂).FG
theorem
Submodule.fg_finset_sup
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{ι : Type u_3}
(s : Finset ι)
(N : ι → Submodule R M)
(h : ∀ i ∈ s, (N i).FG)
:
(s.sup N).FG
theorem
Submodule.fg_biSup
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{ι : Type u_3}
(s : Finset ι)
(N : ι → Submodule R M)
(h : ∀ i ∈ s, (N i).FG)
:
(⨆ i ∈ s, N i).FG
theorem
Submodule.fg_pi
{R : Type u_1}
[Semiring R]
{ι : Type u_4}
{M : ι → Type u_5}
[Finite ι]
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R (M i)]
{p : (i : ι) → Submodule R (M i)}
(hsb : ∀ (i : ι), (p i).FG)
:
(Submodule.pi Set.univ p).FG
theorem
Submodule.FG.map
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{P : Type u_3}
[AddCommMonoid P]
[Module R P]
(f : M →ₗ[R] P)
{N : Submodule R M}
(hs : N.FG)
:
(Submodule.map f N).FG
theorem
Submodule.fg_of_fg_map_injective
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{P : Type u_3}
[AddCommMonoid P]
[Module R P]
(f : M →ₗ[R] P)
(hf : Function.Injective ⇑f)
{N : Submodule R M}
(hfn : (Submodule.map f N).FG)
:
N.FG
theorem
Submodule.fg_of_fg_map
{R : Type u_4}
{M : Type u_5}
{P : Type u_6}
[Ring R]
[AddCommGroup M]
[Module R M]
[AddCommGroup P]
[Module R P]
(f : M →ₗ[R] P)
(hf : LinearMap.ker f = ⊥)
{N : Submodule R M}
(hfn : (Submodule.map f N).FG)
:
N.FG
theorem
Submodule.fg_top
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(N : Submodule R M)
:
theorem
Submodule.fg_of_linearEquiv
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{P : Type u_3}
[AddCommMonoid P]
[Module R P]
(e : M ≃ₗ[R] P)
(h : ⊤.FG)
:
⊤.FG
theorem
Submodule.fg_induction
(R : Type u_4)
(M : Type u_5)
[Semiring R]
[AddCommMonoid M]
[Module R M]
(P : Submodule R M → Prop)
(h₁ : ∀ (x : M), P (Submodule.span R {x}))
(h₂ : ∀ (M₁ M₂ : Submodule R M), P M₁ → P M₂ → P (M₁ ⊔ M₂))
(N : Submodule R M)
(hN : N.FG)
:
P N
theorem
Submodule.fg_restrictScalars
{R : Type u_4}
{S : Type u_5}
{M : Type u_6}
[CommSemiring R]
[Semiring S]
[Algebra R S]
[AddCommGroup M]
[Module S M]
[Module R M]
[IsScalarTower R S M]
(N : Submodule S M)
(hfin : N.FG)
(h : Function.Surjective ⇑(algebraMap R S))
:
(Submodule.restrictScalars R N).FG
theorem
Submodule.FG.of_restrictScalars
(R : Type u_4)
{A : Type u_5}
{M : Type u_6}
[CommSemiring R]
[Semiring A]
[AddCommMonoid M]
[Algebra R A]
[Module R M]
[Module A M]
[IsScalarTower R A M]
(S : Submodule A M)
(hS : (Submodule.restrictScalars R S).FG)
:
S.FG
theorem
Submodule.fg_iff_compact
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(s : Submodule R M)
:
Finitely generated submodules are precisely compact elements in the submodule lattice.
@[instance 100]
instance
Module.Finite.of_finite
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Finite M]
:
Module.Finite R M
Equations
- ⋯ = ⋯
theorem
Module.Finite.of_surjective
{R : Type u_1}
{M : Type u_4}
{N : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
[hM : Module.Finite R M]
(f : M →ₗ[R] N)
(hf : Function.Surjective ⇑f)
:
Module.Finite R N
instance
Module.Finite.quotient
(R : Type u_6)
{A : Type u_7}
{M : Type u_8}
[Semiring R]
[AddCommGroup M]
[Ring A]
[Module A M]
[Module R M]
[SMul R A]
[IsScalarTower R A M]
[Module.Finite R M]
(N : Submodule A M)
:
Module.Finite R (M ⧸ N)
Equations
- ⋯ = ⋯
instance
Module.Finite.range
{R : Type u_1}
{M : Type u_4}
{N : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
{F : Type u_6}
[FunLike F M N]
[SemilinearMapClass F (RingHom.id R) M N]
[Module.Finite R M]
(f : F)
:
Module.Finite R ↥(LinearMap.range f)
The range of a linear map from a finite module is finite.
Equations
- ⋯ = ⋯
instance
Module.Finite.map
{R : Type u_1}
{M : Type u_4}
{N : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(p : Submodule R M)
[Module.Finite R ↥p]
(f : M →ₗ[R] N)
:
Module.Finite R ↥(Submodule.map f p)
Pushforwards of finite submodules are finite.
Equations
- ⋯ = ⋯
instance
Module.Finite.pi
{R : Type u_1}
[Semiring R]
{ι : Type u_6}
{M : ι → Type u_7}
[Finite ι]
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R (M i)]
[h : ∀ (i : ι), Module.Finite R (M i)]
:
Module.Finite R ((i : ι) → M i)
Equations
- ⋯ = ⋯
theorem
Module.Finite.of_restrictScalars_finite
(R : Type u_6)
(A : Type u_7)
(M : Type u_8)
[CommSemiring R]
[Semiring A]
[AddCommMonoid M]
[Module R M]
[Module A M]
[Algebra R A]
[IsScalarTower R A M]
[hM : Module.Finite R M]
:
Module.Finite A M
theorem
Module.Finite.equiv
{R : Type u_1}
{M : Type u_4}
{N : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
[Module.Finite R M]
(e : M ≃ₗ[R] N)
:
Module.Finite R N
theorem
Module.Finite.equiv_iff
{R : Type u_1}
{M : Type u_4}
{N : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(e : M ≃ₗ[R] N)
:
Module.Finite R M ↔ Module.Finite R N
instance
Module.Finite.ulift
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Finite R M]
:
Equations
- ⋯ = ⋯
theorem
Module.Finite.iff_fg
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{N : Submodule R M}
:
Module.Finite R ↥N ↔ N.FG
instance
Module.Finite.bot
(R : Type u_1)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Module.Finite R ↥⊥
Equations
- ⋯ = ⋯
instance
Module.Finite.top
(R : Type u_1)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Finite R M]
:
Module.Finite R ↥⊤
Equations
- ⋯ = ⋯
theorem
Module.Finite.span_of_finite
(R : Type u_1)
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{A : Set M}
(hA : A.Finite)
:
Module.Finite R ↥(Submodule.span R A)
The submodule generated by a finite set is R-finite.
instance
Module.Finite.span_singleton
(R : Type u_1)
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(x : M)
:
Module.Finite R ↥(Submodule.span R {x})
The submodule generated by a single element is R-finite.
Equations
- ⋯ = ⋯
instance
Module.Finite.span_finset
(R : Type u_1)
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(s : Finset M)
:
Module.Finite R ↥(Submodule.span R ↑s)
The submodule generated by a finset is R-finite.
Equations
- ⋯ = ⋯
theorem
Module.Finite.trans
{R : Type u_6}
(A : Type u_7)
(M : Type u_8)
[Semiring R]
[Semiring A]
[Module R A]
[AddCommMonoid M]
[Module R M]
[Module A M]
[IsScalarTower R A M]
[Module.Finite R A]
[Module.Finite A M]
:
Module.Finite R M
theorem
Module.Finite.of_equiv_equiv
{A₁ : Type u_6}
{B₁ : Type u_7}
{A₂ : Type u_8}
{B₂ : Type u_9}
[CommRing A₁]
[CommRing B₁]
[CommRing A₂]
[CommRing B₂]
[Algebra A₁ B₁]
[Algebra A₂ B₂]
(e₁ : A₁ ≃+* A₂)
(e₂ : B₁ ≃+* B₂)
(he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁))
[Module.Finite A₁ B₁]
:
Module.Finite A₂ B₂
instance
Submodule.finite_sup
{R : Type u_1}
{V : Type u_2}
[Ring R]
[AddCommGroup V]
[Module R V]
(S₁ S₂ : Submodule R V)
[h₁ : Module.Finite R ↥S₁]
[h₂ : Module.Finite R ↥S₂]
:
Module.Finite R ↥(S₁ ⊔ S₂)
The sup of two fg submodules is finite. Also see Submodule.FG.sup.
Equations
- ⋯ = ⋯
instance
Submodule.finite_finset_sup
{R : Type u_2}
{V : Type u_3}
[Ring R]
[AddCommGroup V]
[Module R V]
{ι : Type u_1}
(s : Finset ι)
(S : ι → Submodule R V)
[∀ (i : ι), Module.Finite R ↥(S i)]
:
Module.Finite R ↥(s.sup S)
The submodule generated by a finite supremum of finite dimensional submodules is finite-dimensional.
Note that strictly this only needs ∀ i ∈ s, FiniteDimensional K (S i), but that doesn't
work well with typeclass search.
Equations
- ⋯ = ⋯
theorem
RingHom.Finite.of_surjective
{A : Type u_1}
{B : Type u_2}
[CommRing A]
[CommRing B]
(f : A →+* B)
(hf : Function.Surjective ⇑f)
:
f.Finite