Finiteness conditions in commutative algebra

In this file we define a notion of finiteness that is common in commutative algebra.

Main declarations

• Submodule.FG, Ideal.FG These express that some object is finitely generated as submodule over some base ring.

• Module.Finite, RingHom.Finite, AlgHom.Finite all of these express that some object is finitely generated as module over some base ring.

Main results

• exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul is Nakayama's lemma, in the following form: if N is a finitely generated submodule of an ambient R-module M and I is an ideal of R such that N ⊆ IN, then there exists r ∈ 1 + I such that rN = 0.

def Submodule.FG {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) : Prop

A submodule of M is finitely generated if it is the span of a finite subset of M.

Equations

• N.FG = ∃ (S : Finset M), Submodule.span R ↑S = N

theorem Submodule.fg_def {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} : N.FG ↔ ∃ (S : Set M), S.Finite ∧ Submodule.span R S = N

theorem Submodule.fg_iff_addSubmonoid_fg {M : Type u_2} [AddCommMonoid M] (P : Submodule ℕ M) : P.FG ↔ P.FG

theorem Submodule.fg_iff_add_subgroup_fg {G : Type u_3} [AddCommGroup G] (P : Submodule ℤ G) : P.FG ↔ P.toAddSubgroup.FG

theorem Submodule.fg_iff_exists_fin_generating_family {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} : N.FG ↔ ∃ (n : ℕ) (s : Fin n → M), Submodule.span R (Set.range s) = N

theorem Submodule.fg_iff_exists_finite_generating_family {A : Type u} [Semiring A] {M : Type v} [AddCommMonoid M] [Module A M] {N : Submodule A M} : N.FG ↔ ∃ (G : Type w) (_ : Finite G) (g : G → M), Submodule.span A (Set.range g) = N

theorem Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul {R : Type u_3} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) (hn : N.FG) (hin : N ≤ I • N) : ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0

Nakayama's Lemma. Atiyah-Macdonald 2.5, Eisenbud 4.7, Matsumura 2.2, Stacks 00DV

theorem Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul {R : Type u_3} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) (hn : N.FG) (hin : N ≤ I • N) : ∃ r ∈ I, ∀ n ∈ N, r • n = n

theorem Submodule.fg_bot {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] : ⊥.FG

theorem Subalgebra.fg_bot_toSubmodule {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] : (Subalgebra.toSubmodule ⊥).FG

theorem Submodule.fg_unit {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] (I : (Submodule R A)ˣ) : (↑I).FG

theorem Submodule.fg_of_isUnit {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] {I : Submodule R A} (hI : IsUnit I) : I.FG

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) : (Submodule.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) : (Submodule.span 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) : (iSup N).FG

theorem Submodule.FG.map {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {P : Type u_3} [AddCommMonoid P] [Module R P] (f : M →ₗ[R] 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] {P : Type u_3} [AddCommMonoid P] [Module R P] (f : M →ₗ[R] P) (hf : Function.Injective ⇑f) {N : Submodule R M} (hfn : (Submodule.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 : (Submodule.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

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) : ⊤.FG

theorem Submodule.FG.prod {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {P : Type u_3} [AddCommMonoid P] [Module R P] {sb : Submodule R M} {sc : Submodule R P} (hsb : sb.FG) (hsc : sc.FG) : (sb.prod sc).FG

theorem Submodule.fg_pi {R : Type u_1} [Semiring R] {ι : Type u_4} {M : ι → Type u_5} [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

theorem Submodule.fg_of_fg_map_of_fg_inf_ker {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) {s : Submodule R M} (hs1 : (Submodule.map f s).FG) (hs2 : (s ⊓ LinearMap.ker f).FG) : s.FG

If 0 → M' → M → M'' → 0 is exact and M' and M'' are finitely generated then so is M.

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 (Submodule.span 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_ker_comp {R : Type u_4} {M : Type u_5} {N : Type u_6} {P : Type u_7} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (hf1 : (LinearMap.ker f).FG) (hf2 : (LinearMap.ker g).FG) (hsur : Function.Surjective ⇑f) : (LinearMap.ker (g ∘ₗ f)).FG

The kernel of the composition of two linear maps is finitely generated if both kernels are and the first morphism is surjective.

theorem Submodule.fg_restrictScalars {R : Type u_4} {S : Type u_5} {M : Type u_6} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommGroup 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

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.

theorem Submodule.exists_fg_le_eq_rTensor_inclusion {R : Type u_4} {M : Type u_5} {N : Type u_6} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {I : Submodule R N} (x : TensorProduct R (↥I) M) : ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I) (y : TensorProduct R (↥J) M), x = (LinearMap.rTensor M (Submodule.inclusion hle)) y

Every x : I ⊗ M is the image of some y : J ⊗ M, where J ≤ I is finitely generated, under the tensor product of J.inclusion ‹J ≤ I› : J → I and the identity M → M.

theorem Submodule.FG.map₂ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) {p : Submodule R M} {q : Submodule R N} (hp : p.FG) (hq : q.FG) : (Submodule.map₂ f p q).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

def Ideal.FG {R : Type u_1} [Semiring R] (I : Ideal R) : Prop

An ideal of R is finitely generated if it is the span of a finite subset of R.

This is defeq to Submodule.FG, but unfolds more nicely.

Equations

• I.FG = ∃ (S : Finset R), Ideal.span ↑S = I

theorem Ideal.FG.map {R : Type u_3} {S : Type u_4} [Semiring R] [Semiring S] {I : Ideal R} (h : I.FG) (f : R →+* S) : (Ideal.map f I).FG

The image of a finitely generated ideal is finitely generated.

This is the Ideal version of Submodule.FG.map.

theorem Ideal.fg_ker_comp {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommRing R] [CommRing S] [CommRing A] (f : R →+* S) (g : S →+* A) (hf : (RingHom.ker f).FG) (hg : (RingHom.ker g).FG) (hsur : Function.Surjective ⇑f) : (RingHom.ker (g.comp f)).FG

theorem Ideal.exists_radical_pow_le_of_fg {R : Type u_3} [CommSemiring R] (I : Ideal R) (h : I.radical.FG) : ∃ (n : ℕ), I.radical ^ n ≤ I

theorem Ideal.exists_pow_le_of_le_radical_of_fg_radical {R : Type u_3} [CommSemiring R] {I J : Ideal R} (hIJ : I ≤ J.radical) (hJ : J.radical.FG) : ∃ (k : ℕ), I ^ k ≤ J

@[deprecated Ideal.exists_pow_le_of_le_radical_of_fg_radical]

theorem Ideal.exists_pow_le_of_le_radical_of_fG {R : Type u_3} [CommSemiring R] {I J : Ideal R} (hIJ : I ≤ J.radical) (hJ : J.radical.FG) : ∃ (k : ℕ), I ^ k ≤ J

Alias of Ideal.exists_pow_le_of_le_radical_of_fg_radical.

theorem Ideal.exists_pow_le_of_le_radical_of_fg {R : Type u_3} [CommSemiring R] {I J : Ideal R} (h' : I ≤ J.radical) (h : I.FG) : ∃ (n : ℕ), I ^ n ≤ J

class Module.Finite (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : Prop

A module over a semiring is Finite if it is finitely generated as a module.

• out : ⊤.FG

  A module over a semiring is Finite if it is finitely generated as a module.

theorem Module.Finite.out {R : Type u_1} {M : Type u_4} {inst✝ : Semiring R} {inst✝¹ : AddCommMonoid M} {inst✝² : Module R M} [self : Module.Finite R M] : ⊤.FG

A module over a semiring is Finite if it is finitely generated as a module.

theorem Module.finite_def {R : Type u_6} {M : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] : Module.Finite R M ↔ ⊤.FG

theorem Module.Finite.iff_addMonoid_fg {M : Type u_6} [AddCommMonoid M] : Module.Finite ℕ M ↔ AddMonoid.FG M

theorem Module.Finite.iff_addGroup_fg {G : Type u_6} [AddCommGroup G] : Module.Finite ℤ G ↔ AddGroup.FG G

theorem Module.Finite.exists_fin {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : ∃ (n : ℕ) (s : Fin n → M), Submodule.span R (Set.range s) = ⊤

See also Module.Finite.exists_fin'.

theorem Module.Finite.exists_fin' (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), Function.Surjective ⇑f

theorem Module.Finite.exists_comp_eq_id_of_projective (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Module.Projective R M] : ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M) (g : M →ₗ[R] Fin n → R), Function.Surjective ⇑f ∧ Function.Injective ⇑g ∧ f ∘ₗ g = LinearMap.id

theorem Module.finite_of_finite (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Finite R] [Module.Finite R M] : Finite M

@[deprecated Module.finite_of_finite]

theorem FiniteDimensional.finite_of_finite (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Finite R] [Module.Finite R M] : Finite M

Alias of Module.finite_of_finite.

@[deprecated Module.finite_of_finite]

theorem FiniteDimensional.fintypeOfFintype (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Finite R] [Module.Finite R M] : Finite M

A finite dimensional vector space over a finite field is finite

@[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

Equations

• ⋯ = ⋯

theorem Module.finite_iff_finite {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Finite R] : Module.Finite R M ↔ Finite M

A module over a finite ring has finite dimension iff it is finite.

theorem Module.Finite.of_surjective {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [hM : Module.Finite R M] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) : Module.Finite R N

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)

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem Module.Finite.of_restrictScalars_finite (R : Type u_6) (A : Type u_7) (M : Type u_8) [CommSemiring R] [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] [Algebra R A] [IsScalarTower R A M] [hM : Module.Finite R M] : Module.Finite A M

instance Module.Finite.prod {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [hM : Module.Finite R M] [hN : Module.Finite R N] : Module.Finite R (M × N)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

instance Module.Finite.bot (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : Module.Finite R ↥⊥

Equations

• ⋯ = ⋯

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 ↥⊤

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯

theorem Set.Finite.submoduleSpan (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Finite R] {s : Set M} (hs : s.Finite) : (↑(Submodule.span R s)).Finite

theorem Module.Finite.Module.End.isNilpotent_iff_of_finite {R : Type u_6} {M : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] {f : Module.End R M} : IsNilpotent f ↔ ∀ (m : M), ∃ (n : ℕ), (f ^ n) m = 0

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} [CommRing A₁] [CommRing B₁] [CommRing A₂] [CommRing 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₂

noncomputable def instModuleTensorProduct (R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] : Module A (TensorProduct R A M)

Porting note: reminding Lean about this instance for Module.Finite.base_change

Equations

• instModuleTensorProduct R A M = TensorProduct.leftModule

instance Module.Finite.base_change (R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [h : Module.Finite R M] : Module.Finite A (TensorProduct R A M)

Equations

• ⋯ = ⋯

instance Module.Finite.tensorProduct (R : Type u_1) (M : Type u_4) (N : Type u_5) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [hM : Module.Finite R M] [hN : Module.Finite R N] : Module.Finite R (TensorProduct R M N)

Equations

• ⋯ = ⋯

theorem Module.Finite.finite_basis {R : Type u_6} {M : Type u_7} [Semiring R] [Nontrivial R] [AddCommMonoid M] [Module R M] {ι : Type u_8} [Module.Finite R M] (b : Basis ι R M) : Finite ι

If a free module is finite, then any arbitrary basis is finite.

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.

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯

instance Submodule.finite_iSup {R : Type u_2} {V : Type u_3} [Ring R] [AddCommGroup V] [Module R V] {ι : Sort u_1} [Finite ι] (S : ι → Submodule R V) [∀ (i : ι), Module.Finite R ↥(S i)] : Module.Finite R ↥(⨆ (i : ι), S i)

The submodule generated by a supremum of finite dimensional submodules, indexed by a finite sort is finite-dimensional.

Equations

• ⋯ = ⋯

instance Module.Finite.finsupp {R : Type u_2} {V : Type u_3} [Ring R] [AddCommGroup V] [Module R V] {ι : Type u_1} [Finite ι] [Module.Finite R V] : Module.Finite R (ι →₀ V)

Equations

• ⋯ = ⋯

def RingHom.Finite {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) : Prop

A ring morphism A →+* B is Finite if B is finitely generated as A-module.

Equations

• f.Finite = Module.Finite A B

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) : f.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) : g.Finite

def AlgHom.Finite {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) : Prop

An algebra morphism A →ₐ[R] B is finite if it is finite as ring morphism. In other words, if B is finitely generated as A-module.

Equations

• f.Finite = 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) : f.Finite

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) : g.Finite

instance Subalgebra.finite_bot {F : Type u_1} {E : Type u_2} [CommSemiring F] [Semiring E] [Algebra F E] : Module.Finite F ↥⊥

Equations

• ⋯ = ⋯

theorem Module.exists_isPrincipal_quotient_of_finite (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M] : ∃ (N : Submodule R M), N ≠ ⊤ ∧ ⊤.IsPrincipal

theorem Module.exists_surjective_quotient_of_finite (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M] : ∃ (I : Ideal R) (f : M →ₗ[R] R ⧸ I), I ≠ ⊤ ∧ Function.Surjective ⇑f

instance instNontrivialTensorProduct (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M] : Nontrivial (TensorProduct R M M)

Equations

• ⋯ = ⋯