Strongly transcendental elements

In this file, we provide basic properties for strongly transcendental elements in an algebra. This is a relatively niche notion, but is useful for proving Zarkisi's main theorem.

Reference

• https://stacks.math.columbia.edu/tag/00PZ

def IsStronglyTranscendental (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x : S) : Prop

We say that x : S is strongly transcendental over R if forall u : S and all p : R[X], p(x) * u = 0 → p * u = 0. If S is a domain, and R ⊆ S, this is equivalent to the image of x in Frac(S) being transcendental over R. See IsStronglyTranscendental.iff_of_isFractionRing.

Equations

• IsStronglyTranscendental R x = ∀ (u : S) (p : Polynomial R), (Polynomial.aeval x) p * u = 0 → Polynomial.map (algebraMap R S) p * Polynomial.C u = 0

theorem IsStronglyTranscendental.transcendental {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} (h : IsStronglyTranscendental R x) [FaithfulSMul R S] : Transcendental R x

theorem isStronglyTranscendental_iff_of_field {R : Type u_1} [CommRing R] {K : Type u_4} [Field K] [Algebra R K] [FaithfulSMul R K] {x : K} : IsStronglyTranscendental R x ↔ Transcendental R x

theorem IsStronglyTranscendental.of_map {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] {x : S} {f : S →ₐ[R] T} (hf : Function.Injective ⇑f) (h : IsStronglyTranscendental R (f x)) : IsStronglyTranscendental R x

theorem IsStronglyTranscendental.of_isLocalization {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] (M : Submonoid S) [IsLocalization M T] [IsScalarTower R S T] {x : S} (h : IsStronglyTranscendental R x) : IsStronglyTranscendental R ((algebraMap S T) x)

theorem IsStronglyTranscendental.of_isLocalization_left {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] (M : Submonoid R) [IsLocalization M S] [IsScalarTower R S T] {x : T} (h : IsStronglyTranscendental R x) : IsStronglyTranscendental S x

theorem IsStronglyTranscendental.restrictScalars {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {x : T} (h : IsStronglyTranscendental S x) : IsStronglyTranscendental R x

theorem IsStronglyTranscendental.of_surjective_left {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {x : T} (h : IsStronglyTranscendental R x) (H : Function.Surjective ⇑(algebraMap R S)) : IsStronglyTranscendental S x

theorem IsStronglyTranscendental.iff_of_isLocalization {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] {M : Submonoid S} (hM : M ≤ nonZeroDivisors S) [IsLocalization M T] [IsScalarTower R S T] {x : S} : IsStronglyTranscendental R ((algebraMap S T) x) ↔ IsStronglyTranscendental R x

theorem IsStronglyTranscendental.iff_of_isFractionRing {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (K : Type u_4) [Field K] [Algebra R K] [Algebra S K] [IsScalarTower R S K] [FaithfulSMul R S] [IsFractionRing S K] {x : S} : IsStronglyTranscendental R x ↔ Transcendental R ((algebraMap S K) x)

theorem IsStronglyTranscendental.of_transcendental {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {K : Type u_4} [Field K] [Algebra R K] [Algebra S K] [IsScalarTower R S K] [FaithfulSMul R S] [FaithfulSMul S K] {x : S} (H : Transcendental R ((algebraMap S K) x)) : IsStronglyTranscendental R x

theorem isStronglyTranscendental_mk_of_mem_minimalPrimes {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsReduced S] {x : S} (hx : IsStronglyTranscendental R x) (q : Ideal S) (hq : q ∈ minimalPrimes S) : IsStronglyTranscendental R ((Ideal.Quotient.mk q) x)

Stacks Tag 00Q0