Documentation

Mathlib.RingTheory.Finiteness.Basic

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] :

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) :

(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) :

(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_iSup {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_3} [Finite ι] (N : ι → Submodule R M) (h : ∀ (i : ι), (N i).FG) :

instance Submodule.instSemilatticeSupSubtypeFG {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :

SemilatticeSup { P : Submodule R M // P.FG }

Equations

One or more equations did not get rendered due to their size.

instance Submodule.instInhabitedSubtypeFG {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :

Inhabited { P : Submodule R M // P.FG }

Equations

Submodule.instInhabitedSubtypeFG = { default := ⟨⊥, ⋯⟩ }

theorem Submodule.fg_pi {R : Type u_1} [Semiring R] {ι : Type u_5} {M : ι → Type u_6} [Finite ι] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {p : (i : ι) → Submodule R (M i)} (hsb : ∀ (i : ι), (p i).FG) :

(pi Set.univ p).FG

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

@[simp]

theorem Submodule.fg_range {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 σ] [Module.Finite R M] (f : M →ₛₗ[σ] P) :

Maps from a finite module have a finite range.

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_map_iff {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} :

(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 : f.ker = ⊥) {N : Submodule R M} (hfn : (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) :

⊤.FG ↔ N.FG

The top submodule of another submodule N is FG iff N is FG.

See also Module.Finite.fg_top.

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) :

See also Module.Finite.equiv_iff.

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 (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] [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.stabilizes_of_iSup_eq {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Submodule R M} (hM' : M'.FG) (N : ℕ →o Submodule R M) (H : iSup ⇑N = M') :

∃ (n : ℕ), M' = N n

theorem Submodule.fg_iff_compact {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (s : Submodule R M) :

s.FG ↔ CompleteLattice.IsCompactElement s

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) :

Module.Finite R M ↔ Module.Finite S P

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] [Module.Finite R M] (f : M →ₗ[R] N) :

Module.Finite R ↥f.range

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_pi {R : Type u_1} [Semiring R] {ι : Type u_6} (M : ι → Type u_7) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Module.Finite R ((i : ι) → M i)] (i : ι) :

Module.Finite R (M i)

theorem Module.Finite.pi_iff {R : Type u_1} [Semiring R] {ι : Type u_6} {M : ι → Type u_7} [Finite ι] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] :

Module.Finite R ((i : ι) → M i) ↔ ∀ (i : ι), Module.Finite R (M i)

theorem Ideal.fg_top (R : Type u_1) [Semiring R] :

instance Module.Finite.self (R : Type u_1) [Semiring R] :

Module.Finite R R

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) :

Module.Finite R M ↔ Module.Finite R N

instance Module.Finite.instMulOpposite {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] :

Module.Finite R Mᵐᵒᵖ

instance Module.Finite.ulift {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] :

Module.Finite R (ULift.{u_6, u_4} 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} :

Module.Finite R ↥N ↔ N.FG

A submodule is finite as a module iff it is finitely generated.

theorem Module.Finite.of_fg {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} :

N.FG → Module.Finite R ↥N

A finitely-generated submodule is finite as a module.

theorem Submodule.FG.of_finite {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

A submodule that is finite as a module is finitely generated.

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 ↥(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.id (A : Type u_1) [CommRing A] :

(RingHom.id A).Finite

theorem RingHom.Finite.of_surjective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) (hf : Function.Surjective ⇑f) :

theorem RingEquiv.finite {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (e : A ≃+* B) :

e.toRingHom.Finite

theorem RingHom.Finite.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] {g : B →+* C} {f : A →+* B} (hg : g.Finite) (hf : f.Finite) :

(g.comp f).Finite

theorem RingHom.Finite.of_comp_finite {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] {f : A →+* B} {g : B →+* C} (h : (g.comp f).Finite) :

theorem AlgHom.Finite.id (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] :

(AlgHom.id R A).Finite

theorem AlgHom.Finite.comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B] [Algebra R C] {g : B →ₐ[R] C} {f : A →ₐ[R] B} (hg : g.Finite) (hf : f.Finite) :

(g.comp f).Finite

theorem AlgHom.Finite.of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : Function.Surjective ⇑f) :

theorem AlgHom.Finite.of_comp_finite {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B] [Algebra R C] {f : A →ₐ[R] B} {g : B →ₐ[R] C} (h : (g.comp 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] :

Module.Finite { c : R // 0 ≤ c } E

If a module is finite over a linearly ordered ring, then it is also finite over the non-negative scalars.