Mathlib.RingTheory.Finiteness.Subalgebra

Subalgebra.fg_bot_toSubmodule theorem

: (⊥ : Subalgebra R A).toSubmodule.FG

Full source

theorem fg_bot_toSubmodule : (⊥ : Subalgebra R A).toSubmodule.FG :=
  ⟨{1}, by simp [Algebra.toSubmodule_bot, one_eq_span]⟩

Bottom Subalgebra's Submodule is Finitely Generated

Informal description

The submodule corresponding to the bottom element $\bot$ in the lattice of subalgebras of an $R$-algebra $A$ is finitely generated.

Subalgebra.finite_bot instance

: Module.Finite R (⊥ : Subalgebra R A)

Full source

instance finite_bot : Module.Finite R (⊥ : Subalgebra R A) :=
  Module.Finite.range (Algebra.linearMap R A)

Finite Generation of the Bottom Subalgebra as a Module

Informal description

The bottom subalgebra $\bot$ of an algebra $A$ over a commutative semiring $R$ is finitely generated as an $R$-module.

Submodule.fg_unit theorem

{R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] (I : (Submodule R A)ˣ) : (I : Submodule R A).FG

Full source

theorem fg_unit {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] (I : (Submodule R A)ˣ) :
    (I : Submodule R A).FG := by
  obtain ⟨T, T', hT, hT', one_mem⟩ := mem_span_mul_finite_of_mem_mul (I.mul_inv ▸ one_le.mp le_rfl)
  refine ⟨T, span_eq_of_le _ hT ?_⟩
  rw [← one_mul I, ← mul_one (span R (T : Set A))]
  conv_rhs => rw [← I.inv_mul, ← mul_assoc]
  refine mul_le_mul_left (le_trans ?_ <| mul_le_mul_right <| span_le.mpr hT')
  rwa [Units.val_one, span_mul_span, one_le]

Invertible Submodules are Finitely Generated

Informal description

Let $R$ be a commutative semiring and $A$ a semiring equipped with an $R$-algebra structure. For any invertible element $I$ in the multiplicative monoid of $R$-submodules of $A$, the submodule $I$ is finitely generated as an $R$-module.

Submodule.fg_of_isUnit theorem

{R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] {I : Submodule R A} (hI : IsUnit I) : I.FG

Full source

theorem fg_of_isUnit {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] {I : Submodule R A}
    (hI : IsUnit I) : I.FG :=
  fg_unit hI.unit

Invertible Submodules are Finitely Generated

Informal description

Let $R$ be a commutative semiring and $A$ a semiring equipped with an $R$-algebra structure. For any invertible $R$-submodule $I$ of $A$, $I$ is finitely generated as an $R$-module.

Submodule.FG.mul theorem

(hm : M.FG) (hn : N.FG) : (M * N).FG

Full source

theorem FG.mul (hm : M.FG) (hn : N.FG) : (M * N).FG := by
  rw [mul_eq_map₂]; exact hm.map₂ _ hn

Product of Finitely Generated Submodules is Finitely Generated

Informal description

Let $R$ be a commutative semiring, and let $A$ be a semiring with an $R$-algebra structure. Given two finitely generated $R$-submodules $M$ and $N$ of $A$, their product submodule $M \cdot N$ is also finitely generated.

Submodule.FG.pow theorem

(h : M.FG) (n : ℕ) : (M ^ n).FG

Full source

theorem FG.pow (h : M.FG) (n : ℕ) : (M ^ n).FG :=
  Nat.recOn n ⟨{1}, by simp [one_eq_span]⟩ fun n ih => by simpa [pow_succ] using ih.mul h

Finite Generation of Powers of a Finitely Generated Submodule

Informal description

Let $R$ be a commutative semiring, and let $A$ be a semiring with an $R$-algebra structure. If an $R$-submodule $M$ of $A$ is finitely generated, then for any natural number $n$, the $n$-th power submodule $M^n$ is also finitely generated.