Mathlib.RingTheory.Finiteness.Basic

Submodule.fg_bot theorem

: (⊥ : Submodule R M).FG

Full source

theorem fg_bot : (⊥ : Submodule R M).FG :=
  ⟨∅, by rw [Finset.coe_empty, span_empty]⟩

Zero Submodule is Finitely Generated

Informal description

The zero submodule $\{0\}$ of an $R$-module $M$ is finitely generated.

Submodule.fg_span theorem

{s : Set M} (hs : s.Finite) : FG (span R s)

Full source

theorem fg_span {s : Set M} (hs : s.Finite) : FG (span R s) :=
  ⟨hs.toFinset, by rw [hs.coe_toFinset]⟩

Finite Span Implies Finitely Generated Submodule

Informal description

For any finite subset $s$ of an $R$-module $M$, the submodule $\text{span}_R(s)$ is finitely generated.

Submodule.fg_span_singleton theorem

(x : M) : FG (R ∙ x)

Full source

theorem fg_span_singleton (x : M) : FG (R ∙ x) :=
  fg_span (finite_singleton x)

Cyclic submodules are finitely generated

Informal description

For any element $x$ of an $R$-module $M$, the cyclic submodule $R \cdot x$ (the span of the singleton set $\{x\}$) is finitely generated.

Submodule.FG.sup theorem

{N₁ N₂ : Submodule R M} (hN₁ : N₁.FG) (hN₂ : N₂.FG) : (N₁ ⊔ N₂).FG

Full source

theorem FG.sup {N₁ N₂ : Submodule R M} (hN₁ : N₁.FG) (hN₂ : N₂.FG) : (N₁ ⊔ N₂).FG :=
  let ⟨t₁, ht₁⟩ := fg_def.1 hN₁
  let ⟨t₂, ht₂⟩ := fg_def.1 hN₂
  fg_def.2 ⟨t₁ ∪ t₂, ht₁.1.union ht₂.1, by rw [span_union, ht₁.2, ht₂.2]⟩

Supremum of Finitely Generated Submodules is Finitely Generated

Informal description

For any two finitely generated submodules $N_1$ and $N_2$ of an $R$-module $M$, their supremum $N_1 \sqcup N_2$ is also finitely generated.

Submodule.fg_finset_sup theorem

{ι : Type*} (s : Finset ι) (N : ι → Submodule R M) (h : ∀ i ∈ s, (N i).FG) : (s.sup N).FG

Full source

theorem fg_finset_sup {ι : Type*} (s : Finset ι) (N : ι → Submodule R M) (h : ∀ i ∈ s, (N i).FG) :
    (s.sup N).FG :=
  Finset.sup_induction fg_bot (fun _ ha _ hb => ha.sup hb) h

Finite Supremum of Finitely Generated Submodules is Finitely Generated

Informal description

Let $M$ be a module over a ring $R$, $\iota$ be a type, and $s$ be a finite set of elements of $\iota$. For each $i \in s$, let $N_i$ be a finitely generated submodule of $M$. Then the supremum of the submodules $N_i$ for $i \in s$ is also finitely generated.

Submodule.fg_biSup theorem

{ι : Type*} (s : Finset ι) (N : ι → Submodule R M) (h : ∀ i ∈ s, (N i).FG) : (⨆ i ∈ s, N i).FG

Full source

theorem fg_biSup {ι : Type*} (s : Finset ι) (N : ι → Submodule R M) (h : ∀ i ∈ s, (N i).FG) :
    (⨆ i ∈ s, N i).FG := by simpa only [Finset.sup_eq_iSup] using fg_finset_sup s N h

Finite Bounded Supremum of Finitely Generated Submodules is Finitely Generated

Informal description

Let $M$ be a module over a ring $R$, $\iota$ be a type, and $s$ be a finite subset of $\iota$. For each $i \in s$, let $N_i$ be a finitely generated submodule of $M$. Then the supremum $\bigsqcup_{i \in s} N_i$ is also finitely generated.

Submodule.fg_iSup theorem

{ι : Sort*} [Finite ι] (N : ι → Submodule R M) (h : ∀ i, (N i).FG) : (iSup N).FG

Full source

theorem fg_iSup {ι : Sort*} [Finite ι] (N : ι → Submodule R M) (h : ∀ i, (N i).FG) :
    (iSup N).FG := by
  cases nonempty_fintype (PLift ι)
  simpa [iSup_plift_down] using fg_biSup Finset.univ (N ∘ PLift.down) fun i _ => h i.down

Finite Supremum of Finitely Generated Submodules is Finitely Generated

Informal description

Let $M$ be a module over a ring $R$, and let $\iota$ be a finite index type. For each $i \in \iota$, let $N_i$ be a finitely generated submodule of $M$. Then the supremum $\bigsqcup_{i \in \iota} N_i$ is also finitely generated.

Submodule.fg_pi theorem

 {ι : Type*} {M : ι → Type*} [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

Full source

theorem fg_pi {ι : Type*} {M : ι → Type*} [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 := by
  classical
    simp_rw [fg_def] at hsb ⊢
    choose t htf hts using hsb
    refine
      ⟨⋃ i, (LinearMap.single R _ i) '' t i, Set.finite_iUnion fun i => (htf i).image _, ?_⟩
    -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 changed `span_image` into `span_image _`
    simp_rw [span_iUnion, span_image _, hts, Submodule.iSup_map_single]

Finite Product of Finitely Generated Submodules is Finitely Generated

Informal description

Let $\iota$ be a finite index type, and for each $i \in \iota$, let $M_i$ be an $R$-module with a finitely generated submodule $p_i \subseteq M_i$. Then the submodule of functions $f \colon \iota \to \prod_{i \in \iota} M_i$ such that $f(i) \in p_i$ for all $i \in \iota$ is finitely generated.

Submodule.FG.map theorem

{N : Submodule R M} (hs : N.FG) : (N.map f).FG

Full source

theorem FG.map {N : Submodule R M} (hs : N.FG) : (N.map f).FG :=
  let ⟨t, ht⟩ := fg_def.1 hs
  fg_def.2 ⟨f '' t, ht.1.image _, by rw [span_image, ht.2]⟩

Image of a Finitely Generated Submodule under a Linear Map is Finitely Generated

Informal description

Let $N$ be a finitely generated submodule of an $R$-module $M$, and let $f : M \to P$ be a linear map. Then the image submodule $f(N)$ is also finitely generated.

Submodule.fg_of_fg_map_injective theorem

(hf : Function.Injective f) {N : Submodule R M} (hfn : (N.map f).FG) : N.FG

Full source

theorem fg_of_fg_map_injective (hf : Function.Injective f) {N : Submodule R M}
    (hfn : (N.map f).FG) : N.FG :=
  let ⟨t, ht⟩ := hfn
  ⟨t.preimage f fun _ _ _ _ h => hf h,
    Submodule.map_injective_of_injective hf <| by
      rw [map_span, Finset.coe_preimage, Set.image_preimage_eq_inter_range,
        Set.inter_eq_self_of_subset_left, ht]
      rw [← LinearMap.range_coe, ← span_le, ht, ← map_top]
      exact map_mono le_top⟩

Finitely Generated Submodule under Injective Linear Map

Informal description

Let $f : M \to P$ be an injective linear map between $R$-modules, and let $N$ be a submodule of $M$. If the image submodule $f(N)$ is finitely generated, then $N$ is also finitely generated.

Submodule.fg_of_fg_map theorem

 {R M P : Type*} [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 : (N.map f).FG) : N.FG

Full source

theorem fg_of_fg_map {R M P : Type*} [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 : (N.map f).FG) : N.FG :=
  fg_of_fg_map_injective f (LinearMap.ker_eq_bot.1 hf) hfn

Finitely Generated Submodule under Injective Linear Map Implies Finitely Generated Domain

Informal description

Let $R$ be a ring, and let $M$ and $P$ be $R$-modules. Given a linear map $f : M \to P$ with trivial kernel (i.e., $f$ is injective), and a submodule $N$ of $M$ such that the image submodule $f(N)$ is finitely generated, then $N$ itself is finitely generated.

Submodule.fg_top theorem

(N : Submodule R M) : (⊤ : Submodule R N).FG ↔ N.FG

Full source

theorem fg_top (N : Submodule R M) : (⊤ : Submodule R N).FG ↔ N.FG :=
  ⟨fun h => N.range_subtype ▸ map_top N.subtype ▸ h.map _, fun h =>
    fg_of_fg_map_injective N.subtype Subtype.val_injective <| by rwa [map_top, range_subtype]⟩

Finitely Generated Top Submodule iff Submodule is Finitely Generated

Informal description

For any submodule $N$ of an $R$-module $M$, the top submodule of $N$ (i.e., $N$ itself) is finitely generated if and only if $N$ is finitely generated as a submodule of $M$.

Submodule.fg_of_linearEquiv theorem

(e : M ≃ₗ[R] P) (h : (⊤ : Submodule R P).FG) : (⊤ : Submodule R M).FG

Full source

theorem fg_of_linearEquiv (e : M ≃ₗ[R] P) (h : (⊤ : Submodule R P).FG) : (⊤ : Submodule R M).FG :=
  e.symm.range ▸ map_top (e.symm : P →ₗ[R] M) ▸ h.map _

Finitely Generated Module via Linear Equivalence

Informal description

Let $R$ be a ring and $M$, $P$ be $R$-modules. Given a linear equivalence $e: M \simeq P$ and that the top submodule of $P$ (i.e., $P$ itself) is finitely generated, then the top submodule of $M$ (i.e., $M$ itself) is also finitely generated.

Submodule.fg_induction theorem

 (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M] (P : Submodule R M → Prop)
  (h₁ : ∀ x, P (Submodule.span R { x })) (h₂ : ∀ M₁ M₂, P M₁ → P M₂ → P (M₁ ⊔ M₂)) (N : Submodule R M) (hN : N.FG) : P N

Full source

theorem fg_induction (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M]
    (P : Submodule R M → Prop) (h₁ : ∀ x, P (Submodule.span R {x}))
    (h₂ : ∀ M₁ M₂, P M₁ → P M₂ → P (M₁ ⊔ M₂)) (N : Submodule R M) (hN : N.FG) : P N := by
  classical
    obtain ⟨s, rfl⟩ := hN
    induction s using Finset.induction with
    | empty =>
      rw [Finset.coe_empty, Submodule.span_empty, ← Submodule.span_zero_singleton]
      exact h₁ _
    | insert _ _ _ ih =>
      rw [Finset.coe_insert, Submodule.span_insert]
      exact h₂ _ _ (h₁ _) ih

Induction Principle for Finitely Generated Submodules

Informal description

Let $R$ be a semiring and $M$ an $R$-module. For any predicate $P$ on submodules of $M$, if: 1. $P$ holds for the span of every singleton set $\{x\}$ where $x \in M$, and 2. $P$ holds for the supremum $M_1 \sqcup M_2$ of any two submodules $M_1, M_2$ whenever $P$ holds for both $M_1$ and $M_2$, then $P$ holds for every finitely generated submodule $N$ of $M$.

Submodule.fg_restrictScalars theorem

 {R S M : Type*} [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)) :
  (Submodule.restrictScalars R N).FG

Full source

theorem fg_restrictScalars {R S M : Type*} [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)) :
    (Submodule.restrictScalars R N).FG := by
  obtain ⟨X, rfl⟩ := hfin
  use X
  exact (Submodule.restrictScalars_span R S h (X : Set M)).symm

Finitely Generated Submodule under Restriction of Scalars with Surjective Algebra Map

Informal description

Let $R$ be a commutative semiring, $S$ a semiring with an $R$-algebra structure, and $M$ an $S$-module that is also an $R$-module via restriction of scalars, such that the scalar multiplication is compatible (i.e., $[IsScalarTower R S M]$ holds). Given a finitely generated $S$-submodule $N$ of $M$ and a surjective algebra map from $R$ to $S$, the restricted $R$-submodule of $N$ is also finitely generated.

Submodule.FG.of_restrictScalars theorem

 (R) {A M} [Semiring R] [Semiring A] [AddCommMonoid M] [SMul R A] [Module R M] [Module A M] [IsScalarTower R A M]
  (S : Submodule A M) (hS : (S.restrictScalars R).FG) : S.FG

Full source

lemma FG.of_restrictScalars (R) {A M} [Semiring R] [Semiring A] [AddCommMonoid M]
    [SMul R A] [Module R M] [Module A M] [IsScalarTower R A M] (S : Submodule A M)
    (hS : (S.restrictScalars R).FG) : S.FG := by
  obtain ⟨s, e⟩ := hS
  refine ⟨s, Submodule.restrictScalars_injective R _ _ (le_antisymm ?_ ?_)⟩
  · show Submodule.span A s ≤ S
    have := Submodule.span_le.mp e.le
    rwa [Submodule.span_le]
  · rw [← e]
    exact Submodule.span_le_restrictScalars _ _ _

Finitely Generated Submodule under Compatible Restriction of Scalars

Informal description

Let $R$ be a semiring and $A$ a semiring with a scalar multiplication by $R$. Let $M$ be an $A$-module that is also an $R$-module via restriction of scalars, such that the scalar multiplication is compatible (i.e., $r \cdot (a \cdot m) = (r \cdot a) \cdot m$ for all $r \in R$, $a \in A$, $m \in M$). If the restriction of an $A$-submodule $S$ of $M$ to an $R$-submodule is finitely generated, then $S$ itself is finitely generated as an $A$-submodule.

Submodule.FG.stabilizes_of_iSup_eq theorem

{M' : Submodule R M} (hM' : M'.FG) (N : ℕ →o Submodule R M) (H : iSup N = M') : ∃ n, M' = N n

Full source

theorem FG.stabilizes_of_iSup_eq {M' : Submodule R M} (hM' : M'.FG) (N : ℕℕ →o Submodule R M)
    (H : iSup N = M') : ∃ n, M' = N n := by
  obtain ⟨S, hS⟩ := hM'
  have : ∀ s : S, ∃ n, (s : M) ∈ N n := fun s =>
    (Submodule.mem_iSup_of_chain N s).mp
      (by
        rw [H, ← hS]
        exact Submodule.subset_span s.2)
  choose f hf using this
  use S.attach.sup f
  apply le_antisymm
  · conv_lhs => rw [← hS]
    rw [Submodule.span_le]
    intro s hs
    exact N.2 (Finset.le_sup <| S.mem_attach ⟨s, hs⟩) (hf _)
  · rw [← H]
    exact le_iSup _ _

Stabilization of Finitely Generated Submodules under Supremum Condition

Informal description

Let $M'$ be a finitely generated submodule of an $R$-module $M$, and let $N : \mathbb{N} \to_o \mathrm{Submodule}\, R\, M$ be an order homomorphism from the natural numbers to the submodules of $M$ (ordered by inclusion). If the supremum of the submodules $N(n)$ over all $n \in \mathbb{N}$ equals $M'$, then there exists some natural number $n$ such that $M' = N(n)$.

Submodule.fg_iff_compact theorem

(s : Submodule R M) : s.FG ↔ CompleteLattice.IsCompactElement s

Full source

/-- Finitely generated submodules are precisely compact elements in the submodule lattice. -/
theorem fg_iff_compact (s : Submodule R M) : s.FG ↔ CompleteLattice.IsCompactElement s := by
  classical
    -- Introduce shorthand for span of an element
    let sp : M → Submodule R M := fun a => span R {a}
    -- Trivial rewrite lemma; a small hack since simp (only) & rw can't accomplish this smoothly.
    have supr_rw : ∀ t : Finset M, ⨆ x ∈ t, sp x = ⨆ x ∈ (↑t : Set M), sp x := fun t => by rfl
    constructor
    · rintro ⟨t, rfl⟩
      rw [span_eq_iSup_of_singleton_spans, ← supr_rw, ← Finset.sup_eq_iSup t sp]
      apply CompleteLattice.isCompactElement_finsetSup
      exact fun n _ => singleton_span_isCompactElement n
    · intro h
      -- s is the Sup of the spans of its elements.
      have sSup' : s = sSup (sp '' ↑s) := by
        rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]
      -- by h, s is then below (and equal to) the sup of the spans of finitely many elements.
      obtain ⟨u, ⟨huspan, husup⟩⟩ := h (sp '' ↑s) (le_of_eq sSup')
      have ssup : s = u.sup id := by
        suffices u.sup id ≤ s from le_antisymm husup this
        rw [sSup', Finset.sup_id_eq_sSup]
        exact sSup_le_sSup huspan
      obtain ⟨t, -, rfl⟩ := Finset.subset_set_image_iff.mp huspan
      rw [Finset.sup_image, Function.id_comp, Finset.sup_eq_iSup, supr_rw, ←
        span_eq_iSup_of_singleton_spans, eq_comm] at ssup
      exact ⟨t, ssup⟩

Finitely Generated Submodules are Compact Elements

Informal description

A submodule $s$ of an $R$-module $M$ is finitely generated if and only if it is a compact element in the complete lattice of submodules of $M$.

Module.Finite.instIsCoatomicSubmodule instance

[Module.Finite R M] : IsCoatomic (Submodule R M)

Full source

instance [Module.Finite R M] : IsCoatomic (Submodule R M) :=
  CompleteLattice.coatomic_of_top_compact <| by rwa [← fg_iff_compact, ← finite_def]

The Lattice of Submodules of a Finitely Generated Module is Coatomic

Informal description

For any finitely generated module $M$ over a semiring $R$, the lattice of submodules of $M$ is coatomic.

Module.Finite.of_finite instance

[Finite M] : Module.Finite R M

Full source

instance (priority := 100) of_finite [Finite M] : Module.Finite R M := by
  cases nonempty_fintype M
  exact ⟨⟨Finset.univ, by rw [Finset.coe_univ]; exact Submodule.span_univ⟩⟩

Finite Modules are Finitely Generated

Informal description

Every finite module $M$ over a semiring $R$ is finitely generated.

Module.Finite.of_surjective theorem

[hM : Module.Finite R M] (f : M →ₛₗ[σ] P) (hf : Surjective f) : Module.Finite S P

Full source

theorem of_surjective [hM : Module.Finite R M] (f : M →ₛₗ[σ] P) (hf : Surjective f) :
    Module.Finite S P :=
  ⟨by
    rw [← LinearMap.range_eq_top.2 hf, ← Submodule.map_top]
    exact hM.1.map f⟩

Surjective Linear Map Preserves Finite Generation

Informal description

Let $R$ and $S$ be semirings, and let $M$ and $P$ be modules over $R$ and $S$ respectively, with a linear map $f: M \to P$ between them. If $M$ is finitely generated as an $R$-module and $f$ is surjective, then $P$ is finitely generated as an $S$-module.

LinearMap.finite_iff_of_bijective theorem

(f : M →ₛₗ[σ] P) (hf : Function.Bijective f) : Module.Finite R M ↔ Module.Finite S P

Full source

theorem _root_.LinearMap.finite_iff_of_bijective (f : M →ₛₗ[σ] P) (hf : Function.Bijective f) :
    Module.FiniteModule.Finite R M ↔ Module.Finite S P :=
  ⟨fun _ ↦ of_surjective f hf.surjective, fun _ ↦ ⟨fg_of_fg_map_injective f hf.injective <| by
    rwa [Submodule.map_top, LinearMap.range_eq_top.2 hf.surjective, ← Module.finite_def]⟩⟩

Bijective Linear Map Preserves Finite Generation

Informal description

Let $R$ and $S$ be semirings, and let $M$ and $P$ be modules over $R$ and $S$ respectively. Given a bijective linear map $f: M \to P$, the module $M$ is finitely generated over $R$ if and only if the module $P$ is finitely generated over $S$.

Module.Finite.quotient instance

 (R) {A M} [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)

Full source

instance quotient (R) {A M} [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) :=
  Module.Finite.of_surjective (N.mkQ.restrictScalars R) N.mkQ_surjective

Finite Generation of Quotient Modules

Informal description

For a semiring $R$, a ring $A$, and an $A$-module $M$ that is also an $R$-module with compatible scalar multiplication, if $M$ is finitely generated as an $R$-module, then for any $A$-submodule $N$ of $M$, the quotient module $M/N$ is also finitely generated as an $R$-module.

Module.Finite.range instance

 {F : Type*} [FunLike F M N] [SemilinearMapClass F (RingHom.id R) M N] [Module.Finite R M] (f : F) :
  Module.Finite R (LinearMap.range f)

Full source

/-- The range of a linear map from a finite module is finite. -/
instance range {F : Type*} [FunLike F M N] [SemilinearMapClass F (RingHom.id R) M N]
    [Module.Finite R M] (f : F) : Module.Finite R (LinearMap.range f) :=
  of_surjective (SemilinearMapClass.semilinearMap f).rangeRestrict
    fun ⟨_, y, hy⟩ => ⟨y, Subtype.ext hy⟩

Finite Generation of the Range of a Linear Map

Informal description

For any finitely generated module $M$ over a semiring $R$ and any linear map $f \colon M \to N$, the range of $f$ is also a finitely generated $R$-module.

Module.Finite.map instance

(p : Submodule R M) [Module.Finite R p] (f : M →ₗ[R] N) : Module.Finite R (p.map f)

Full source

/-- Pushforwards of finite submodules are finite. -/
instance map (p : Submodule R M) [Module.Finite R p] (f : M →ₗ[R] N) : Module.Finite R (p.map f) :=
  of_surjective (f.restrict fun _ => Submodule.mem_map_of_mem) fun ⟨_, _, hy, hy'⟩ =>
    ⟨⟨_, hy⟩, Subtype.ext hy'⟩

Finite Generation is Preserved under Linear Maps

Informal description

Let $R$ be a semiring, and let $M$ and $N$ be modules over $R$. If a submodule $p$ of $M$ is finitely generated as an $R$-module and $f: M \to N$ is a linear map, then the image of $p$ under $f$ is also finitely generated as an $R$-module.

Module.Finite.pi instance

 {ι : Type*} {M : ι → Type*} [_root_.Finite ι] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
  [h : ∀ i, Module.Finite R (M i)] : Module.Finite R (∀ i, M i)

Full source

instance pi {ι : Type*} {M : ι → Type*} [_root_.Finite ι] [∀ i, AddCommMonoid (M i)]
    [∀ i, Module R (M i)] [h : ∀ i, Module.Finite R (M i)] : Module.Finite R (∀ i, M i) :=
  ⟨by
    rw [← Submodule.pi_top]
    exact Submodule.fg_pi fun i => (h i).1⟩

Finite Product of Finitely Generated Modules is Finitely Generated

Informal description

For a finite index type $\iota$ and a family of $R$-modules $M_i$ indexed by $\iota$, if each $M_i$ is finitely generated as an $R$-module, then the product module $\prod_{i \in \iota} M_i$ is also finitely generated as an $R$-module.

Module.Finite.self instance

: Module.Finite R R

Full source

instance self : Module.Finite R R :=
  ⟨⟨{1}, by simpa only [Finset.coe_singleton] using Ideal.span_singleton_one⟩⟩

A Semiring is Finitely Generated as a Module over Itself

Informal description

For any semiring $R$, the module $R$ over itself is finitely generated.

Module.Finite.of_restrictScalars_finite theorem

 (R A M : Type*) [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

Full source

theorem of_restrictScalars_finite (R A M : Type*) [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 := by
  rw [finite_def, Submodule.fg_def] at hM ⊢
  obtain ⟨S, hSfin, hSgen⟩ := hM
  refine ⟨S, hSfin, eq_top_iff.2 ?_⟩
  have := Submodule.span_le_restrictScalars R A S
  rw [hSgen] at this
  exact this

Finite Generation Preserved Under Restriction of Scalars

Informal description

Let $R$ and $A$ be semirings, and let $M$ be an $A$-module that is also an $R$-module via restriction of scalars. Suppose there is a scalar multiplication action of $R$ on $A$ making $M$ a tower of modules (i.e., $r \cdot (a \cdot m) = (r \cdot a) \cdot m$ for all $r \in R$, $a \in A$, $m \in M$). If $M$ is finitely generated as an $R$-module, then $M$ is also finitely generated as an $A$-module.

Module.Finite.equiv theorem

[Module.Finite R M] (e : M ≃ₗ[R] N) : Module.Finite R N

Full source

theorem equiv [Module.Finite R M] (e : M ≃ₗ[R] N) : Module.Finite R N :=
  of_surjective (e : M →ₗ[R] N) e.surjective

Linear Equivalence Preserves Finite Generation of Modules

Informal description

Let $M$ and $N$ be modules over a semiring $R$. If $M$ is finitely generated as an $R$-module and there exists a linear equivalence $e: M \simeq N$ of $R$-modules, then $N$ is also finitely generated as an $R$-module.

Module.Finite.equiv_iff theorem

(e : M ≃ₗ[R] N) : Module.Finite R M ↔ Module.Finite R N

Full source

theorem equiv_iff (e : M ≃ₗ[R] N) : Module.FiniteModule.Finite R M ↔ Module.Finite R N :=
  ⟨fun _ ↦ equiv e, fun _ ↦ equiv e.symm⟩

Linear Equivalence Preserves Finite Generation of Modules (Bidirectional)

Informal description

Let $M$ and $N$ be modules over a semiring $R$, and let $e: M \simeq N$ be a linear equivalence of $R$-modules. Then $M$ is finitely generated as an $R$-module if and only if $N$ is finitely generated as an $R$-module.

Module.Finite.ulift instance

[Module.Finite R M] : Module.Finite R (ULift M)

Full source

instance ulift [Module.Finite R M] : Module.Finite R (ULift M) := equiv ULift.moduleEquiv.symm

Finite Generation of Lifted Modules

Informal description

For any finitely generated module $M$ over a semiring $R$, the lifted module $\text{ULift}\, M$ is also finitely generated over $R$.

Module.Finite.iff_fg theorem

{N : Submodule R M} : Module.Finite R N ↔ N.FG

Full source

theorem iff_fg {N : Submodule R M} : Module.FiniteModule.Finite R N ↔ N.FG := Module.finite_def.trans N.fg_top

Equivalence of Module Finiteness and Submodule Finiteness for Submodules

Informal description

Let $R$ be a semiring and $N$ be a submodule of an $R$-module $M$. Then $N$ is finitely generated as an $R$-module if and only if $N$ is finitely generated as a submodule of $M$.

Module.Finite.bot instance

: Module.Finite R (⊥ : Submodule R M)

Full source

instance bot : Module.Finite R (⊥ : Submodule R M) := iff_fg.mpr fg_bot

Finitely Generated Zero Submodule

Informal description

The zero submodule $\{0\}$ of an $R$-module $M$ is finitely generated as an $R$-module.

Module.Finite.top instance

[Module.Finite R M] : Module.Finite R (⊤ : Submodule R M)

Full source

instance top [Module.Finite R M] : Module.Finite R (⊤ : Submodule R M) := iff_fg.mpr fg_top

Finitely Generated Module Implies Finitely Generated Top Submodule

Informal description

For any finitely generated $R$-module $M$, the top submodule (i.e., $M$ itself) is finitely generated as an $R$-module.

Module.Finite.span_of_finite theorem

{A : Set M} (hA : Set.Finite A) : Module.Finite R (Submodule.span R A)

Full source

/-- The submodule generated by a finite set is `R`-finite. -/
theorem span_of_finite {A : Set M} (hA : Set.Finite A) :
    Module.Finite R (Submodule.span R A) :=
  ⟨(Submodule.fg_top _).mpr ⟨hA.toFinset, hA.coe_toFinset.symm ▸ rfl⟩⟩

Finite Span Implies Finitely Generated Module

Informal description

For any finite subset $A$ of an $R$-module $M$, the submodule generated by $A$ (i.e., the $R$-linear span of $A$) is finitely generated as an $R$-module.

Module.Finite.span_singleton instance

(x : M) : Module.Finite R (R ∙ x)

Full source

/-- The submodule generated by a single element is `R`-finite. -/
instance span_singleton (x : M) : Module.Finite R (R ∙ x) :=
  Module.Finite.span_of_finite R <| Set.finite_singleton _

Finite Generation of Cyclic Submodules

Informal description

For any element $x$ in an $R$-module $M$, the cyclic submodule $R \cdot x$ generated by $x$ is finitely generated as an $R$-module.

Module.Finite.span_finset instance

(s : Finset M) : Module.Finite R (span R (s : Set M))

Full source

/-- The submodule generated by a finset is `R`-finite. -/
instance span_finset (s : Finset M) : Module.Finite R (span R (s : Set M)) :=
  ⟨(Submodule.fg_top _).mpr ⟨s, rfl⟩⟩

Finite Span of a Finset is Finitely Generated

Informal description

For any semiring $R$, any $R$-module $M$, and any finite subset $s$ of $M$, the submodule $\text{span}_R(s)$ is finitely generated as an $R$-module.

Module.Finite.trans theorem

 {R : Type*} (A M : Type*) [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

Full source

theorem trans {R : Type*} (A M : Type*) [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
  | ⟨⟨s, hs⟩⟩, ⟨⟨t, ht⟩⟩ =>
    ⟨Submodule.fg_def.2
        ⟨Set.image2 (· • ·) (↑s : Set A) (↑t : Set M),
          Set.Finite.image2 _ s.finite_toSet t.finite_toSet, by
          rw [Set.image2_smul, Submodule.span_smul_of_span_eq_top hs (↑t : Set M), ht,
            Submodule.restrictScalars_top]⟩⟩

Transitivity of Finite Generation for Modules via Scalar Tower

Informal description

Let $R$ be a semiring, $A$ a semiring with an $R$-module structure, and $M$ an additive commutative monoid with both $R$-module and $A$-module structures, such that the actions are compatible via the scalar tower condition. If $A$ is finitely generated as an $R$-module and $M$ is finitely generated as an $A$-module, then $M$ is finitely generated as an $R$-module.

Module.Finite.of_equiv_equiv theorem

 {A₁ B₁ A₂ B₂ : Type*} [CommSemiring A₁] [CommSemiring B₁] [CommSemiring A₂] [Semiring B₂] [Algebra A₁ B₁]
  [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂) (e₂ : B₁ ≃+* B₂)
  (he : RingHom.comp (algebraMap A₂ B₂) ↑e₁ = RingHom.comp ↑e₂ (algebraMap A₁ B₁)) [Module.Finite A₁ B₁] :
  Module.Finite A₂ B₂

Full source

lemma of_equiv_equiv {A₁ B₁ A₂ B₂ : Type*} [CommSemiring A₁] [CommSemiring B₁]
    [CommSemiring A₂] [Semiring B₂] [Algebra A₁ B₁] [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂)
    (e₂ : B₁ ≃+* B₂)
    (he : RingHom.comp (algebraMap A₂ B₂) ↑e₁ = RingHom.comp ↑e₂ (algebraMap A₁ B₁))
    [Module.Finite A₁ B₁] : Module.Finite A₂ B₂ := by
  letI := e₁.toRingHom.toAlgebra
  letI := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
  haveI : IsScalarTower A₁ A₂ B₁ := IsScalarTower.of_algebraMap_eq
    (fun x ↦ by simp [RingHom.algebraMap_toAlgebra])
  let e : B₁ ≃ₐ[A₂] B₂ :=
    { e₂ with
      commutes' := fun r ↦ by
        simpa [RingHom.algebraMap_toAlgebra] using DFunLike.congr_fun he.symm (e₁.symm r) }
  haveI := Module.Finite.of_restrictScalars_finite A₁ A₂ B₁
  exact Module.Finite.equiv e.toLinearEquiv

Finite Generation Preserved Under Ring Isomorphism of Algebras

Informal description

Let $A_1, B_1$ be commutative semirings and $A_2, B_2$ be commutative semirings with $B_2$ also a semiring. Suppose there are algebra structures $B_1$ over $A_1$ and $B_2$ over $A_2$. Given ring isomorphisms $e_1: A_1 \simeq A_2$ and $e_2: B_1 \simeq B_2$ such that the following diagram commutes: \[ \begin{tikzcd} A_1 \arrow{r}{\text{algebraMap}} \arrow{d}{e_1} & B_1 \arrow{d}{e_2} \\ A_2 \arrow{r}{\text{algebraMap}} & B_2 \end{tikzcd} \] If $B_1$ is finitely generated as an $A_1$-module, then $B_2$ is finitely generated as an $A_2$-module.

Submodule.finite_sup instance

 (S₁ S₂ : Submodule R V) [h₁ : Module.Finite R S₁] [h₂ : Module.Finite R S₂] : Module.Finite R (S₁ ⊔ S₂ : Submodule R V)

Full source

/-- The sup of two fg submodules is finite. Also see `Submodule.FG.sup`. -/
instance finite_sup (S₁ S₂ : Submodule R V) [h₁ : Module.Finite R S₁]
    [h₂ : Module.Finite R S₂] : Module.Finite R (S₁ ⊔ S₂ : Submodule R V) := by
  rw [finite_def] at *
  exact (fg_top _).2 (((fg_top S₁).1 h₁).sup ((fg_top S₂).1 h₂))

Finite Generation of the Supremum of Two Finitely Generated Submodules

Informal description

For any two finitely generated submodules $S_1$ and $S_2$ of an $R$-module $V$, their supremum $S_1 \sqcup S_2$ is also finitely generated as an $R$-module.

Submodule.finite_finset_sup instance

 {ι : Type*} (s : Finset ι) (S : ι → Submodule R V) [∀ i, Module.Finite R (S i)] :
  Module.Finite R (s.sup S : Submodule R V)

Full source

/-- 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. -/
instance finite_finset_sup {ι : Type*} (s : Finset ι) (S : ι → Submodule R V)
    [∀ i, Module.Finite R (S i)] : Module.Finite R (s.sup S : Submodule R V) := by
  refine
    @Finset.sup_induction _ _ _ _ s S (fun i => Module.Finite R ↑i) (Module.Finite.bot R V)
      ?_ fun i _ => by infer_instance
  intro S₁ hS₁ S₂ hS₂
  exact Submodule.finite_sup S₁ S₂

Finite Generation of the Supremum of Finitely Generated Submodules over a Finite Index Set

Informal description

For any finite set $s$ and a family of submodules $(S_i)_{i \in s}$ of an $R$-module $V$, if each $S_i$ is finitely generated as an $R$-module, then the supremum $\bigsqcup_{i \in s} S_i$ is also finitely generated as an $R$-module.

RingHom.Finite.id theorem

: Finite (RingHom.id A)

Full source

theorem id : Finite (RingHom.id A) :=
  Module.Finite.self A

Finite Property of the Identity Ring Homomorphism

Informal description

The identity ring homomorphism $\mathrm{id}_A \colon A \to A$ is finite.

RingHom.Finite.of_surjective theorem

(f : A →+* B) (hf : Surjective f) : f.Finite

Full source

theorem of_surjective (f : A →+* B) (hf : Surjective f) : f.Finite :=
  letI := f.toAlgebra
  Module.Finite.of_surjective (Algebra.linearMap A B) hf

Surjective Ring Homomorphisms are Finite

Informal description

Let $f \colon A \to B$ be a surjective ring homomorphism. Then $f$ is finite, i.e., $B$ is finitely generated as an $A$-module under the scalar multiplication induced by $f$.

RingHom.Finite.comp theorem

{g : B →+* C} {f : A →+* B} (hg : g.Finite) (hf : f.Finite) : (g.comp f).Finite

Full source

theorem comp {g : B →+* C} {f : A →+* B} (hg : g.Finite) (hf : f.Finite) : (g.comp f).Finite := by
  algebraize [f, g, g.comp f]
  exact Module.Finite.trans B C

Composition of Finite Ring Homomorphisms is Finite

Informal description

Let $f \colon A \to B$ and $g \colon B \to C$ be finite ring homomorphisms. Then the composition $g \circ f \colon A \to C$ is also finite.

RingHom.Finite.of_comp_finite theorem

{f : A →+* B} {g : B →+* C} (h : (g.comp f).Finite) : g.Finite

Full source

theorem of_comp_finite {f : A →+* B} {g : B →+* C} (h : (g.comp f).Finite) : g.Finite := by
  algebraize [f, g, g.comp f]
  exact Module.Finite.of_restrictScalars_finite A B C

Finite Property of Composition Implies Finite Property of Second Homomorphism

Informal description

Let $f \colon A \to B$ and $g \colon B \to C$ be ring homomorphisms. If the composition $g \circ f \colon A \to C$ is finite (i.e., $C$ is finitely generated as an $A$-module under the scalar multiplication induced by $g \circ f$), then $g$ is finite (i.e., $C$ is finitely generated as a $B$-module under the scalar multiplication induced by $g$).

AlgHom.Finite.id theorem

: Finite (AlgHom.id R A)

Full source

theorem id : Finite (AlgHom.id R A) :=
  RingHom.Finite.id A

Finite Property of the Identity Algebra Homomorphism

Informal description

The identity algebra homomorphism $\mathrm{id}_A \colon A \to A$ over a base ring $R$ is finite.

AlgHom.Finite.comp theorem

{g : B →ₐ[R] C} {f : A →ₐ[R] B} (hg : g.Finite) (hf : f.Finite) : (g.comp f).Finite

Full source

theorem comp {g : B →ₐ[R] C} {f : A →ₐ[R] B} (hg : g.Finite) (hf : f.Finite) : (g.comp f).Finite :=
  RingHom.Finite.comp hg hf

Composition of Finite Algebra Homomorphisms is Finite

Informal description

Let $R$ be a commutative ring, and let $A$, $B$, and $C$ be $R$-algebras. Given finite algebra homomorphisms $f \colon A \to B$ and $g \colon B \to C$ over $R$, their composition $g \circ f \colon A \to C$ is also finite.

AlgHom.Finite.of_surjective theorem

(f : A →ₐ[R] B) (hf : Surjective f) : f.Finite

Full source

theorem of_surjective (f : A →ₐ[R] B) (hf : Surjective f) : f.Finite :=
  RingHom.Finite.of_surjective f.toRingHom hf

Surjective Algebra Homomorphisms are Finite

Informal description

Let $R$ be a commutative ring, and let $A$ and $B$ be $R$-algebras. Given a surjective algebra homomorphism $f \colon A \to B$ over $R$, then $f$ is finite, i.e., $B$ is finitely generated as an $A$-module under the scalar multiplication induced by $f$.

AlgHom.Finite.of_comp_finite theorem

{f : A →ₐ[R] B} {g : B →ₐ[R] C} (h : (g.comp f).Finite) : g.Finite

Full source

theorem of_comp_finite {f : A →ₐ[R] B} {g : B →ₐ[R] C} (h : (g.comp f).Finite) : g.Finite :=
  RingHom.Finite.of_comp_finite h

Finite Property of Composition Implies Finite Property of Second Algebra Homomorphism

Informal description

Let $R$ be a commutative ring, and let $A$, $B$, and $C$ be $R$-algebras. Given algebra homomorphisms $f \colon A \to B$ and $g \colon B \to C$ over $R$, if the composition $g \circ f \colon A \to C$ is finite (i.e., $C$ is finitely generated as an $A$-module under the scalar multiplication induced by $g \circ f$), then $g$ is finite (i.e., $C$ is finitely generated as a $B$-module under the scalar multiplication induced by $g$).