Subalgebras that are finitely generated as submodules #
theorem
Subalgebra.fg_bot_toSubmodule
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
(Subalgebra.toSubmodule ⊥).FG
instance
Subalgebra.finite_bot
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
Module.Finite R ↥⊥
Equations
- ⋯ = ⋯
theorem
Submodule.fg_unit
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(I : (Submodule R A)ˣ)
:
(↑I).FG
theorem
Submodule.fg_of_isUnit
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{I : Submodule R A}
(hI : IsUnit I)
:
I.FG
theorem
Submodule.FG.mul
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{M N : Submodule R A}
(hm : M.FG)
(hn : N.FG)
:
(M * N).FG
theorem
Submodule.FG.pow
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{M : Submodule R A}
(h : M.FG)
(n : ℕ)
:
(M ^ n).FG