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]
:
instance
Submodule.instSemilatticeSupSubtypeFG
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
Submodule.FG.map
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_3}
{P : Type u_4}
[Semiring S]
[AddCommMonoid P]
[Module S P]
{σ : R →+* S}
[RingHomSurjective σ]
(f : M →ₛₗ[σ] 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]
{S : Type u_3}
{P : Type u_4}
[Semiring S]
[AddCommMonoid P]
[Module S P]
{σ : R →+* S}
[RingHomSurjective σ]
(f : M →ₛₗ[σ] P)
(hf : Function.Injective ⇑f)
{N : Submodule R M}
(hfn : (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 : (map f N).FG)
:
N.FG
theorem
Submodule.fg_restrictScalars
{R : Type u_4}
{S : Type u_5}
{M : Type u_6}
[CommSemiring R]
[Semiring S]
[Algebra R S]
[AddCommMonoid M]
[Module S M]
[Module R M]
[IsScalarTower R S M]
(N : Submodule S M)
(hfin : N.FG)
(h : Function.Surjective ⇑(algebraMap R S))
:
(restrictScalars R N).FG
theorem
Submodule.FG.of_restrictScalars
(R : Type u_4)
{A : Type u_5}
{M : Type u_6}
[Semiring R]
[Semiring A]
[AddCommMonoid M]
[SMul R A]
[Module R M]
[Module A M]
[IsScalarTower R A M]
(S : Submodule A M)
(hS : (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
Module.Finite.instIsCoatomicSubmodule
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Finite R M]
:
IsCoatomic (Submodule R M)
@[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
theorem
Module.Finite.of_surjective
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_7}
{P : Type u_6}
[Semiring S]
[AddCommMonoid P]
[Module S P]
{σ : R →+* S}
[RingHomSurjective σ]
[hM : Module.Finite R M]
(f : M →ₛₗ[σ] P)
(hf : Function.Surjective ⇑f)
:
Module.Finite S P
theorem
LinearMap.finite_iff_of_bijective
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_7}
{P : Type u_6}
[Semiring S]
[AddCommMonoid P]
[Module S P]
{σ : R →+* S}
[RingHomSurjective σ]
(f : M →ₛₗ[σ] P)
(hf : Function.Bijective ⇑f)
:
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)
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.
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.
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)
theorem
Module.Finite.of_restrictScalars_finite
(R : Type u_6)
(A : Type u_7)
(M : Type u_8)
[Semiring R]
[Semiring A]
[AddCommMonoid M]
[Module R M]
[Module A M]
[SMul 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)
:
instance
Module.Finite.ulift
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Finite R M]
:
theorem
Module.Finite.iff_fg
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{N : Submodule R M}
:
instance
Module.Finite.bot
(R : Type u_1)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Module.Finite R ↥⊥
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 ↥⊤
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.
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.
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}
[CommSemiring A₁]
[CommSemiring B₁]
[CommSemiring A₂]
[Semiring 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.
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.
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
instance
instModuleFinite
{R : Type u_1}
{E : Type u_2}
[Ring R]
[LinearOrder R]
[IsOrderedRing R]
[AddCommMonoid E]
[Module R E]
[Module.Finite R E]
:
If a module is finite over a linearly ordered ring, then it is also finite over the non-negative scalars.