Documentation

Mathlib.RingTheory.AlgebraicIndependent.Defs

Algebraic Independence #

This file defines algebraic independence of a family of elements of an R algebra.

Main definitions #

Main results #

We show that algebraic independence is preserved under injective maps of the indices.

References #

def AlgebraicIndependent {ι : Type u_1} (R : Type u_3) {A : Type u_5} (x : ιA) [CommRing R] [CommRing A] [Algebra R A] :

AlgebraicIndependent R x states the family of elements x is algebraically independent over R, meaning that the canonical map out of the multivariable polynomial ring is injective.

Stacks Tag 030E ((1))

Equations
Instances For
    @[reducible, inline]
    abbrev AlgebraicIndepOn {ι : Type u_1} (R : Type u_3) {A : Type u_5} (x : ιA) [CommRing R] [CommRing A] [Algebra R A] (s : Set ι) :

    AlgebraicIndepOn R v s states that the elements in the family v that are indexed by the elements of s are algebraically independent over R.

    Equations
    Instances For
      theorem algebraicIndependent_iff {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] :
      AlgebraicIndependent R x ∀ (p : MvPolynomial ι R), (MvPolynomial.aeval x) p = 0p = 0
      theorem AlgebraicIndependent.eq_zero_of_aeval_eq_zero {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (h : AlgebraicIndependent R x) (p : MvPolynomial ι R) :
      (MvPolynomial.aeval x) p = 0p = 0
      theorem AlgebraicIndependent.of_comp {ι : Type u_1} {R : Type u_3} {A : Type u_5} {A' : Type u_6} {x : ιA} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (f : A →ₐ[R] A') (hfv : AlgebraicIndependent R (f x)) :
      theorem AlgebraicIndependent.comp {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (f : ι'ι) (hf : Function.Injective f) :
      theorem AlgebraicIndependent.coe_range {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :
      theorem algebraicIndependent_equiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (e : ι ι') {f : ι'A} :
      theorem algebraicIndependent_equiv' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (e : ι ι') {f : ι'A} {g : ιA} (h : f e = g) :
      theorem AlgebraicIndependent.of_subtype_range {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_7} {f : ιA} (hf : Function.Injective f) :

      Alias of the forward direction of algebraicIndependent_subtype_range.

      theorem algebraicIndependent_image {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_7} {s : Set ι} {f : ιA} (hf : Set.InjOn f s) :
      (AlgebraicIndependent R fun (x : s) => f x) AlgebraicIndependent R fun (x : ↑(f '' s)) => x
      def AlgebraicIndependent.aevalEquiv {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :

      Canonical isomorphism between polynomials and the subalgebra generated by algebraically independent elements.

      Equations
      Instances For
        @[simp]
        theorem AlgebraicIndependent.aevalEquiv_apply_coe {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (a✝ : MvPolynomial ι R) :
        (hx.aevalEquiv a✝) = (MvPolynomial.aeval x) a✝
        theorem AlgebraicIndependent.algebraMap_aevalEquiv {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (p : MvPolynomial ι R) :
        def AlgebraicIndependent.repr {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :

        The canonical map from the subalgebra generated by an algebraic independent family into the polynomial ring.

        Equations
        Instances For
          @[simp]
          theorem AlgebraicIndependent.aeval_repr {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (p : (Algebra.adjoin R (Set.range x))) :
          (MvPolynomial.aeval x) (hx.repr p) = p
          theorem AlgebraicIndependent.aeval_comp_repr {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ιA} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :
          def IsTranscendenceBasis {ι : Type u_1} (R : Type u_3) {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (x : ιA) :

          A family is a transcendence basis if it is a maximal algebraically independent subset.

          Stacks Tag 030E ((4))

          Equations
          Instances For
            theorem isTranscendenceBasis_equiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (e : ι ι') {f : ι'A} :
            theorem isTranscendenceBasis_equiv' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (e : ι ι') {f : ι'A} {g : ιA} (h : f e = g) :
            theorem IsTranscendenceBasis.of_subtype_range {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_7} {f : ιA} (hf : Function.Injective f) :

            Alias of the forward direction of isTranscendenceBasis_subtype_range.

            theorem isTranscendenceBasis_image {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_7} {s : Set ι} {f : ιA} (hf : Set.InjOn f s) :
            (IsTranscendenceBasis R fun (x : s) => f x) IsTranscendenceBasis R fun (x : ↑(f '' s)) => x