Documentation

Mathlib.RingTheory.Finiteness

Finiteness conditions in commutative algebra #

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

Main declarations #

Main results #

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

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

Equations
Instances For
    theorem Submodule.fg_def {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} :
    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 : Submodule.FG N) (hin : N I N) :
    r, r - 1 I ∀ (n : M), n Nr 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 : Submodule.FG N) (hin : N I N) :
    r, r I ∀ (n : M), n Nr n = n
    theorem Submodule.fg_bot {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :
    theorem Subalgebra.fg_bot_toSubmodule {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] :
    Submodule.FG (Subalgebra.toSubmodule )
    theorem Submodule.fg_unit {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] (I : (Submodule R A)ˣ) :
    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) :
    theorem Submodule.fg_span {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} (hs : Set.Finite s) :
    theorem Submodule.fg_span_singleton {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
    theorem Submodule.FG.sup {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N₁ : Submodule R M} {N₂ : Submodule R M} (hN₁ : Submodule.FG N₁) (hN₂ : Submodule.FG N₂) :
    Submodule.FG (N₁ N₂)
    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 : ι), i sSubmodule.FG (N i)) :
    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 : ι), i sSubmodule.FG (N i)) :
    Submodule.FG (⨆ (i : ι) (_ : i s), N i)
    theorem Submodule.fg_iSup {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} [Finite ι] (N : ιSubmodule R M) (h : ∀ (i : ι), Submodule.FG (N i)) :
    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 : Submodule.FG N) :
    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.FG (Submodule.map f N)) :
    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.FG (Submodule.map f N)) :
    theorem Submodule.fg_top {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) :
    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 : Submodule.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 : Submodule.FG sb) (hsc : Submodule.FG sc) :
    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 : ι), Submodule.FG (p i)) :
    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.FG (Submodule.map f s)) (hs2 : Submodule.FG (s LinearMap.ker f)) :

    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 MProp) (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 : Submodule.FG N) :
    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 : Submodule.FG (LinearMap.ker f)) (hf2 : Submodule.FG (LinearMap.ker g)) (hsur : Function.Surjective f) :

    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 : Submodule.FG N) (h : Function.Surjective ↑(algebraMap R S)) :
    theorem Submodule.FG.stablizes_of_iSup_eq {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Submodule R M} (hM' : Submodule.FG M') (N : →o Submodule R M) (H : iSup N = M') :
    n, M' = N n

    Finitely generated submodules are precisely compact elements in the submodule lattice.

    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 : Submodule.FG p) (hq : Submodule.FG q) :
    theorem Submodule.FG.mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {M : Submodule R A} {N : Submodule R A} (hm : Submodule.FG M) (hn : Submodule.FG N) :
    theorem Submodule.FG.pow {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {M : Submodule R A} (h : Submodule.FG M) (n : ) :
    def Ideal.FG {R : Type u_1} [Semiring R] (I : Ideal R) :

    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
    Instances For
      theorem Ideal.FG.map {R : Type u_3} {S : Type u_4} [Semiring R] [Semiring S] {I : Ideal R} (h : Ideal.FG I) (f : R →+* S) :

      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 : Ideal.FG (RingHom.ker f)) (hg : Ideal.FG (RingHom.ker g)) (hsur : Function.Surjective f) :
      class Module.Finite (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] :

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

      Instances
        theorem Module.Finite.exists_fin' (R : Type u_6) (M : Type u_7) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] :
        n f, Function.Surjective f
        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) :
        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) :

        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 { x // x p }] (f : M →ₗ[R] N) :

        Pushforwards of finite submodules are finite.

        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] :
        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] :
        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) :
        theorem Module.Finite.trans {R : Type u_6} (A : Type u_7) (M : Type u_8) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [Module.Finite R A] [Module.Finite A M] :

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

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

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

          Equations
          Instances For
            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 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 : RingHom.Finite g) (hf : RingHom.Finite f) :
            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 : RingHom.Finite (RingHom.comp g f)) :
            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) :

            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
            Instances For
              theorem AlgHom.Finite.id (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] :
              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 : AlgHom.Finite g) (hf : AlgHom.Finite f) :
              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 : AlgHom.Finite (AlgHom.comp g f)) :