Documentation

Mathlib.RingTheory.FinitePresentation

Finiteness conditions in commutative algebra #

In this file we define several notions of finiteness that are common in commutative algebra.

Main declarations #

class Algebra.FinitePresentation (R : Type w₁) (A : Type w₂) [CommSemiring R] [Semiring A] [Algebra R A] :

An algebra over a commutative semiring is Algebra.FinitePresentation if it is the quotient of a polynomial ring in n variables by a finitely generated ideal.

Instances
    theorem Algebra.FinitePresentation.out {R : Type w₁} {A : Type w₂} [CommSemiring R] [Semiring A] [Algebra R A] [self : Algebra.FinitePresentation R A] :
    ∃ (n : ) (f : MvPolynomial (Fin n) R →ₐ[R] A), Function.Surjective f (RingHom.ker f.toRingHom).FG

    A finitely presented algebra is of finite type.

    Equations
    • =

    An algebra over a Noetherian ring is finitely generated if and only if it is finitely presented.

    theorem Algebra.FinitePresentation.equiv {R : Type w₁} {A : Type w₂} {B : Type w₃} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra.FinitePresentation R A] (e : A ≃ₐ[R] B) :

    If e : A ≃ₐ[R] B and A is finitely presented, then so is B.

    The ring of polynomials in finitely many variables is finitely presented.

    Equations
    • =

    R is finitely presented as R-algebra.

    Equations
    • =

    R[X] is finitely presented as R-algebra.

    Equations
    • =
    theorem Algebra.FinitePresentation.quotient {R : Type w₁} {A : Type w₂} [CommRing R] [CommRing A] [Algebra R A] {I : Ideal A} (h : I.FG) [Algebra.FinitePresentation R A] :

    The quotient of a finitely presented algebra by a finitely generated ideal is finitely presented.

    theorem Algebra.FinitePresentation.of_surjective {R : Type w₁} {A : Type w₂} {B : Type w₃} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] {f : A →ₐ[R] B} (hf : Function.Surjective f) (hker : (RingHom.ker f.toRingHom).FG) [Algebra.FinitePresentation R A] :

    If f : A →ₐ[R] B is surjective with finitely generated kernel and A is finitely presented, then so is B.

    theorem Algebra.FinitePresentation.iff {R : Type w₁} {A : Type w₂} [CommRing R] [CommRing A] [Algebra R A] :
    Algebra.FinitePresentation R A ∃ (n : ) (I : Ideal (MvPolynomial (Fin n) R)) (x : (MvPolynomial (Fin n) R I) ≃ₐ[R] A), I.FG
    theorem Algebra.FinitePresentation.iff_quotient_mvPolynomial' {R : Type w₁} {A : Type w₂} [CommRing R] [CommRing A] [Algebra R A] :
    Algebra.FinitePresentation R A ∃ (ι : Type u_1) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] A), Function.Surjective f (RingHom.ker f.toRingHom).FG

    An algebra is finitely presented if and only if it is a quotient of a polynomial ring whose variables are indexed by a fintype by a finitely generated ideal.

    If A is a finitely presented R-algebra, then MvPolynomial (Fin n) A is finitely presented as R-algebra.

    If A is an R-algebra and S is an A-algebra, both finitely presented, then S is finitely presented as R-algebra.

    theorem Algebra.FinitePresentation.ker_fg_of_mvPolynomial {R : Type w₁} {A : Type w₂} [CommRing R] [CommRing A] [Algebra R A] {n : } (f : MvPolynomial (Fin n) R →ₐ[R] A) (hf : Function.Surjective f) [Algebra.FinitePresentation R A] :
    (RingHom.ker f.toRingHom).FG

    This is used to prove the strictly stronger ker_fg_of_surjective. Use it instead.

    theorem Algebra.FinitePresentation.ker_fG_of_surjective {R : Type w₁} {A : Type w₂} {B : Type w₃} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (f : A →ₐ[R] B) (hf : Function.Surjective f) [Algebra.FinitePresentation R A] [Algebra.FinitePresentation R B] :
    (RingHom.ker f.toRingHom).FG

    If f : A →ₐ[R] B is a surjection between finitely-presented R-algebras, then the kernel of f is finitely generated.

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

    A ring morphism A →+* B is of RingHom.FinitePresentation if B is finitely presented as A-algebra.

    Equations
    Instances For
      theorem RingHom.FiniteType.of_finitePresentation {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {f : A →+* B} (hf : f.FinitePresentation) :
      f.FiniteType
      theorem RingHom.FinitePresentation.id (A : Type u_1) [CommRing A] :
      (RingHom.id A).FinitePresentation
      theorem RingHom.FinitePresentation.comp_surjective {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] {f : A →+* B} {g : B →+* C} (hf : f.FinitePresentation) (hg : Function.Surjective g) (hker : (RingHom.ker g).FG) :
      (g.comp f).FinitePresentation
      theorem RingHom.FinitePresentation.of_surjective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) (hf : Function.Surjective f) (hker : (RingHom.ker f).FG) :
      f.FinitePresentation
      theorem RingHom.FinitePresentation.of_finiteType {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsNoetherianRing A] {f : A →+* B} :
      f.FiniteType f.FinitePresentation
      theorem RingHom.FinitePresentation.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.FinitePresentation) (hf : f.FinitePresentation) :
      (g.comp f).FinitePresentation
      theorem RingHom.FinitePresentation.of_comp_finiteType {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] (f : A →+* B) {g : B →+* C} (hg : (g.comp f).FinitePresentation) (hf : f.FiniteType) :
      g.FinitePresentation
      def AlgHom.FinitePresentation {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 of AlgHom.FinitePresentation if it is of finite presentation as ring morphism. In other words, if B is finitely presented as A-algebra.

      Equations
      • f.FinitePresentation = f.FinitePresentation
      Instances For
        theorem AlgHom.FiniteType.of_finitePresentation {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 : f.FinitePresentation) :
        f.FiniteType
        theorem AlgHom.FinitePresentation.id (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] :
        (AlgHom.id R A).FinitePresentation
        theorem AlgHom.FinitePresentation.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.FinitePresentation) (hf : f.FinitePresentation) :
        (g.comp f).FinitePresentation
        theorem AlgHom.FinitePresentation.comp_surjective {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} (hf : f.FinitePresentation) (hg : Function.Surjective g) (hker : (RingHom.ker g.toRingHom).FG) :
        (g.comp f).FinitePresentation
        theorem AlgHom.FinitePresentation.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) (hker : (RingHom.ker f.toRingHom).FG) :
        f.FinitePresentation
        theorem AlgHom.FinitePresentation.of_finiteType {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [IsNoetherianRing A] {f : A →ₐ[R] B} :
        f.FiniteType f.FinitePresentation
        theorem AlgHom.FinitePresentation.of_comp_finiteType {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).FinitePresentation) (h' : f.FiniteType) :
        g.FinitePresentation