Generators of algebras

Main definition

• Algebra.Generators: A family of generators of a R-algebra S consists of

  1. vars: The type of variables.
  2. val : vars → S: The assignment of each variable to a value.
  3. σ: A set-theoretic section of the induced R-algebra homomorphism R[X] → S, where we write R[X] for R[vars].

• Algebra.Generators.Hom: Given a commuting square

  R --→ P = R[X] ---→ S
  |                   |
  ↓                   ↓
  R' -→ P' = R'[X'] → S
  

  A hom between P and P' is an assignment X → P' such that the arrows commute.

• Algebra.Generators.Cotangent: The cotangent space wrt P = R[X] → S, i.e. the space I/I² with I being the kernel of the presentation.

TODOs

Currently, Lean does not see through the vars field of terms of Generators R S obtained from constructions, e.g. composition. This causes fragile and cumbersome proofs, because simp and rw often don't work properly. Generators R S (and Presentation R S, etc.) should be refactored in a way that makes these equalities reducibly def-eq, for example by unbundling the vars field or making the field globally reducible in constructions using unification hints.

structure Algebra.Generators (R : Type u) (S : Type v) (ι : Type w) [CommRing R] [CommRing S] [Algebra R S] : Type (max (max u v) w)

A family of generators of a R-algebra S consists of

1. vars: The type of variables.
2. val : vars → S: The assignment of each variable to a value in S.
3. σ: A section of R[X] → S.

• val : ι → S

  The assignment of each variable to a value in S.

• σ' : S → MvPolynomial ι R

  A section of R[X] → S.

• aeval_val_σ' (s : S) : (MvPolynomial.aeval self.val) (self.σ' s) = s
• algebra : Algebra (MvPolynomial ι R) S

  An R[X]-algebra instance on S. The default is the one induced by the map R[X] → S, but this causes a diamond if there is an existing instance.

• algebraMap_eq : algebraMap (MvPolynomial ι R) S = ↑(MvPolynomial.aeval self.val)

@[reducible, inline]

abbrev Algebra.Generators.Ring {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) : Type (max w u)

The polynomial ring wrt a family of generators.

instance Algebra.Generators.instRing {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) : Algebra P.Ring S

def Algebra.Generators.σ {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) : S → P.Ring

The designated section of wrt a family of generators.

def Algebra.Generators.Simps.σ {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) : S → P.Ring

See Note [custom simps projection]

@[simp]

theorem Algebra.Generators.aeval_val_σ {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) (s : S) : (MvPolynomial.aeval P.val) (P.σ s) = s

instance Algebra.Generators.instIsScalarTowerRing {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) {R₀ : Type u_1} [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] : IsScalarTower R₀ P.Ring S

@[simp]

theorem Algebra.Generators.algebraMap_apply {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) (x : P.Ring) : (algebraMap P.Ring S) x = (MvPolynomial.aeval P.val) x

@[simp]

theorem Algebra.Generators.σ_smul {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) (x y : S) : P.σ x • y = x * y

theorem Algebra.Generators.σ_injective {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) : Function.Injective P.σ

theorem Algebra.Generators.algebraMap_surjective {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) : Function.Surjective ⇑(algebraMap P.Ring S)

noncomputable def Algebra.Generators.ofSurjective {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (val : ι → S) (h : Function.Surjective ⇑(MvPolynomial.aeval val)) : Generators R S ι

Construct Generators from an assignment I → S such that R[X] → S is surjective.

@[simp]

theorem Algebra.Generators.ofSurjective_val {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (val : ι → S) (h : Function.Surjective ⇑(MvPolynomial.aeval val)) (a✝ : ι) : (ofSurjective val h).val a✝ = val a✝

noncomputable def Algebra.Generators.ofSurjectiveAlgebraMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (h : Function.Surjective ⇑(algebraMap R S)) : Generators R S PEmpty.{w + 1}

If algebraMap R S is surjective, the empty type generates S.

noncomputable def Algebra.Generators.id {R : Type u} [CommRing R] : Generators R R PEmpty.{w + 1}

The canonical generators for R as an R-algebra.

noncomputable def Algebra.Generators.ofAlgHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {I : Type u_1} (f : MvPolynomial I R →ₐ[R] S) (h : Function.Surjective ⇑f) : Generators R S I

Construct Generators from an assignment I → S such that R[X] → S is surjective.

noncomputable def Algebra.Generators.ofSet {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {s : Set S} (hs : adjoin R s = ⊤) : Generators R S ↑s

Construct Generators from a family of generators of S.

noncomputable def Algebra.Generators.self (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Generators R S S

The Generators containing the whole algebra, which induces the canonical map R[S] → S.

@[simp]

theorem Algebra.Generators.self_algebra_algebraMap (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Algebra.algebraMap = (MvPolynomial.aeval _root_.id).toRingHom

@[simp]

theorem Algebra.Generators.self_algebra_smul (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (c : MvPolynomial S R) (x : S) : SMul.smul c x = (MvPolynomial.aeval _root_.id).toRingHom c * x

@[simp]

theorem Algebra.Generators.self_σ (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (n : S) : (self R S).σ n = MvPolynomial.X n

@[simp]

theorem Algebra.Generators.self_val (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (a : S) : (self R S).val a = _root_.id a

noncomputable def Algebra.Generators.toExtension {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) : Extension R S

The extension R[X₁,...,Xₙ] → S given a family of generators.

@[simp]

theorem Algebra.Generators.toExtension_algebra₂ {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) : P.toExtension.algebra₂ = P.instRing

@[simp]

theorem Algebra.Generators.toExtension_commRing {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) : P.toExtension.commRing = MvPolynomial.instCommRingMvPolynomial

@[simp]

theorem Algebra.Generators.toExtension_σ {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) (a✝ : S) : P.toExtension.σ a✝ = P.σ a✝

@[simp]

theorem Algebra.Generators.toExtension_Ring {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) : P.toExtension.Ring = P.Ring

@[simp]

theorem Algebra.Generators.toExtension_algebra₁ {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) : P.toExtension.algebra₁ = MvPolynomial.algebra

noncomputable def Algebra.Generators.localizationAway {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : Generators R S Unit

If S is the localization of R away from r, we obtain a canonical generator mapping to the inverse of r.

@[simp]

theorem Algebra.Generators.localizationAway_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] (x✝ : Unit) : (localizationAway r).val x✝ = IsLocalization.Away.invSelf r

theorem Algebra.Generators.localizationAway_σ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] (s : S) : (localizationAway r).σ s = MvPolynomial.C (IsLocalization.Away.sec r s).1 * MvPolynomial.X () ^ (IsLocalization.Away.sec r s).2

noncomputable def Algebra.Generators.comp {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} {T : Type u_2} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) : Generators R T (ι' ⊕ ι)

Given two families of generators S[X] → T and R[Y] → S, we may construct the family of generators R[X, Y] → T.

@[simp]

theorem Algebra.Generators.comp_val {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} {T : Type u_2} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) (a✝ : ι' ⊕ ι) : (Q.comp P).val a✝ = Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) a✝

theorem Algebra.Generators.comp_σ {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} {T : Type u_2} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) (x : T) : (Q.comp P).σ x = Finsupp.sum (Q.σ x) fun (n : ι' →₀ ℕ) (r : S) => (MvPolynomial.rename Sum.inr) (P.σ r) * (MvPolynomial.monomial (Finsupp.mapDomain Sum.inl n)) 1

noncomputable def Algebra.Generators.extendScalars {R : Type u} (S : Type v) {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_2} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (P : Generators R T ι) : Generators S T ι

If R → S → T is a tower of algebras, a family of generators R[X] → T gives a family of generators S[X] → T.

@[simp]

theorem Algebra.Generators.extendScalars_val {R : Type u} (S : Type v) {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_2} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (P : Generators R T ι) (a✝ : ι) : (extendScalars S P).val a✝ = P.val a✝

noncomputable def Algebra.Generators.baseChange {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_2} [CommRing T] [Algebra R T] (P : Generators R S ι) : Generators T (TensorProduct R T S) ι

If P is a family of generators of S over R and T is an R-algebra, we obtain a natural family of generators of T ⊗[R] S over T.

@[simp]

theorem Algebra.Generators.baseChange_val {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_2} [CommRing T] [Algebra R T] (P : Generators R S ι) (x : ι) : P.baseChange.val x = 1 ⊗ₜ[R] P.val x

noncomputable def Algebra.Generators.reindex {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} (P : Generators R S ι') (e : ι ≃ ι') : Generators R S ι

Given generators P and an equivalence ι ≃ P.vars, these are the induced generators indexed by ι.

theorem Algebra.Generators.reindex_val {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} (P : Generators R S ι') (e : ι ≃ ι') : (P.reindex e).val = P.val ∘ ⇑e

noncomputable def Algebra.Generators.naive {R : Type u} [CommRing R] {σ : Type u_2} {I : Ideal (MvPolynomial σ R)} (s : MvPolynomial σ R ⧸ I → MvPolynomial σ R := Function.surjInv ⋯) (hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x := by apply Function.surjInv_eq) : Generators R (MvPolynomial σ R ⧸ I) σ

The naive generators for a quotient R[Xᵢ] ⧸ I. If the definitional equality of the section matters, it can be explicitly provided.

@[simp]

theorem Algebra.Generators.naive_val {R : Type u} [CommRing R] {σ : Type u_2} {I : Ideal (MvPolynomial σ R)} (s : MvPolynomial σ R ⧸ I → MvPolynomial σ R := Function.surjInv ⋯) (hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x := by apply Function.surjInv_eq) (i : σ) : (naive s hs).val i = (Ideal.Quotient.mk I) (MvPolynomial.X i)

@[simp]

theorem Algebra.Generators.naive_σ {R : Type u} [CommRing R] {σ : Type u_2} {I : Ideal (MvPolynomial σ R)} (s : MvPolynomial σ R ⧸ I → MvPolynomial σ R) (hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x) : (naive s hs).σ = s

structure Algebra.Generators.Hom {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Generators R' S' ι') [Algebra S S'] : Type (max (max u_1 u_3) w)

Given a commuting square R --→ P = R[X] ---→ S | | ↓ ↓ R' -→ P' = R'[X'] → S A hom between P and P' is an assignment I → P' such that the arrows commute. Also see Algebra.Generators.Hom.equivAlgHom.

• val : ι → P'.Ring

  The assignment of each variable in I to a value in P' = R'[X'].

• aeval_val (i : ι) : (MvPolynomial.aeval P'.val) (self.val i) = (algebraMap S S') (P.val i)

theorem Algebra.Generators.Hom.ext_iff {R : Type u} {S : Type v} {ι : Type w} {inst✝ : CommRing R} {inst✝¹ : CommRing S} {inst✝² : Algebra R S} {P : Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} {inst✝³ : CommRing R'} {inst✝⁴ : CommRing S'} {inst✝⁵ : Algebra R' S'} {P' : Generators R' S' ι'} {inst✝⁶ : Algebra S S'} {x y : P.Hom P'} : x = y ↔ x.val = y.val

theorem Algebra.Generators.Hom.ext {R : Type u} {S : Type v} {ι : Type w} {inst✝ : CommRing R} {inst✝¹ : CommRing S} {inst✝² : Algebra R S} {P : Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} {inst✝³ : CommRing R'} {inst✝⁴ : CommRing S'} {inst✝⁵ : Algebra R' S'} {P' : Generators R' S' ι'} {inst✝⁶ : Algebra S S'} {x y : P.Hom P'} (val : x.val = y.val) : x = y

noncomputable def Algebra.Generators.Hom.toAlgHom {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S' ι'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') : P.Ring →ₐ[R] P'.Ring

A hom between two families of generators gives an algebra homomorphism between the polynomial rings.

@[simp]

theorem Algebra.Generators.Hom.algebraMap_toAlgHom {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S' ι'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : P.Hom P') (x : P.Ring) : (MvPolynomial.aeval P'.val) (f.toAlgHom x) = (algebraMap S S') ((MvPolynomial.aeval P.val) x)

@[simp]

theorem Algebra.Generators.Hom.toAlgHom_X {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S' ι'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') (i : ι) : f.toAlgHom (MvPolynomial.X i) = f.val i

theorem Algebra.Generators.Hom.toAlgHom_C {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S' ι'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') (r : R) : f.toAlgHom (MvPolynomial.C r) = MvPolynomial.C ((algebraMap R R') r)

theorem Algebra.Generators.Hom.toAlgHom_monomial {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S' ι'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') (v : ι →₀ ℕ) (r : R) : f.toAlgHom ((MvPolynomial.monomial v) r) = r • v.prod fun (x1 : ι) (x2 : ℕ) => f.val x1 ^ x2

noncomputable def Algebra.Generators.Hom.equivAlgHom {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S' ι'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] : P.Hom P' ≃ { f : P.Ring →ₐ[R] P'.Ring // ∀ (x : P.Ring), (MvPolynomial.aeval P'.val) (f x) = (algebraMap S S') ((MvPolynomial.aeval P.val) x) }

Giving a hom between two families of generators is equivalent to giving an algebra homomorphism between the polynomial rings.

@[simp]

theorem Algebra.Generators.Hom.equivAlgHom_apply_coe {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S' ι'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : P.Hom P') : ↑(equivAlgHom f) = f.toAlgHom

@[simp]

theorem Algebra.Generators.Hom.equivAlgHom_symm_apply_val {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S' ι'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : { f : P.Ring →ₐ[R] P'.Ring // ∀ (x : P.Ring), (MvPolynomial.aeval P'.val) (f x) = (algebraMap S S') ((MvPolynomial.aeval P.val) x) }) (i : ι) : (equivAlgHom.symm f).val i = ↑f (MvPolynomial.X i)

def Algebra.Generators.defaultHom {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Generators R' S' ι') [Algebra S S'] : P.Hom P'

The hom from P to P' given by the designated section of P'.

@[simp]

theorem Algebra.Generators.defaultHom_val {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Generators R' S' ι') [Algebra S S'] (a✝ : ι) : (P.defaultHom P').val a✝ = (P'.σ ∘ ⇑(algebraMap S S') ∘ P.val) a✝

instance Algebra.Generators.instInhabitedHom {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Generators R' S' ι') [Algebra S S'] : Inhabited (P.Hom P')

noncomputable def Algebra.Generators.Hom.id {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) : P.Hom P

The identity hom.

@[simp]

theorem Algebra.Generators.Hom.id_val {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) (n : ι) : (Hom.id P).val n = MvPolynomial.X n

@[simp]

theorem Algebra.Generators.Hom.toAlgHom_id {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) : (Hom.id P).toAlgHom = AlgHom.id R P.Ring

noncomputable def Algebra.Generators.Hom.comp {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S' ι'} {R'' : Type u_4} {S'' : Type u_5} {ι'' : Type u_6} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Generators R'' S'' ι''} [Algebra R' R''] [Algebra R' S''] [Algebra S S'] [Algebra S' S''] [Algebra S S''] [IsScalarTower R' R'' S''] [IsScalarTower R' S' S''] [IsScalarTower S S' S''] (f : P'.Hom P'') (g : P.Hom P') : P.Hom P''

The composition of two homs.

@[simp]

theorem Algebra.Generators.Hom.comp_val {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S' ι'} {R'' : Type u_4} {S'' : Type u_5} {ι'' : Type u_6} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Generators R'' S'' ι''} [Algebra R' R''] [Algebra R' S''] [Algebra S S'] [Algebra S' S''] [Algebra S S''] [IsScalarTower R' R'' S''] [IsScalarTower R' S' S''] [IsScalarTower S S' S''] (f : P'.Hom P'') (g : P.Hom P') (x : ι) : (f.comp g).val x = (MvPolynomial.aeval f.val) (g.val x)

@[simp]

theorem Algebra.Generators.Hom.comp_id {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S' ι'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : P.Hom P') : f.comp (Hom.id P) = f

@[simp]

theorem Algebra.Generators.Hom.id_comp {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Generators R' S' ι') [Algebra S S'] (f : P.Hom P') : (Hom.id P').comp f = f

@[simp]

theorem Algebra.Generators.Hom.toAlgHom_comp_apply {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Generators R' S' ι') {R'' : Type u_4} {S'' : Type u_5} {ι'' : Type u_6} [CommRing R''] [CommRing S''] [Algebra R'' S''] (P'' : Generators R'' S'' ι'') [Algebra R R'] [Algebra R' R''] [Algebra R' S''] [Algebra S S'] [Algebra S' S''] [Algebra S S''] [Algebra R R''] [IsScalarTower R R' R''] [IsScalarTower R' R'' S''] [IsScalarTower R' S' S''] [IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P'') (x : P.Ring) : (g.comp f).toAlgHom x = g.toAlgHom (f.toAlgHom x)

noncomputable def Algebra.Generators.toComp {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_3} {T : Type u_7} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) : P.Hom (Q.comp P)

Given families of generators X ⊆ T over S and Y ⊆ S over R, there is a map of generators R[Y] → R[X, Y].

@[simp]

theorem Algebra.Generators.toComp_val {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_3} {T : Type u_7} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) (i : ι) : (Q.toComp P).val i = MvPolynomial.X (Sum.inr i)

theorem Algebra.Generators.toComp_toAlgHom {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_3} {T : Type u_7} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) : (Q.toComp P).toAlgHom = MvPolynomial.rename Sum.inr

noncomputable def Algebra.Generators.ofComp {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_3} {T : Type u_7} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) : (Q.comp P).Hom Q

Given families of generators X ⊆ T over S and Y ⊆ S over R, there is a map of generators R[X, Y] → S[X].

@[simp]

theorem Algebra.Generators.ofComp_val {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_3} {T : Type u_7} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) (i : ι' ⊕ ι) : (Q.ofComp P).val i = Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ P.val) i

theorem Algebra.Generators.ofComp_toAlgHom_monomial_sumElim {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_3} {T : Type u_7} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) (v₁ : ι' →₀ ℕ) (v₂ : ι →₀ ℕ) (a : R) : (Q.ofComp P).toAlgHom ((MvPolynomial.monomial (v₁.sumElim v₂)) a) = (MvPolynomial.monomial v₁) ((MvPolynomial.aeval P.val) ((MvPolynomial.monomial v₂) a))

theorem Algebra.Generators.toComp_toAlgHom_monomial {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_3} {T : Type u_7} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) (j : ι →₀ ℕ) (a : R) : (Q.toComp P).toAlgHom ((MvPolynomial.monomial j) a) = (MvPolynomial.monomial (Finsupp.sumElim 0 j)) a

@[simp]

theorem Algebra.Generators.toAlgHom_ofComp_rename {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_3} {T : Type u_7} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) (p : P.Ring) : (Q.ofComp P).toAlgHom ((MvPolynomial.rename Sum.inr) p) = MvPolynomial.C ((algebraMap P.Ring S) p)

theorem Algebra.Generators.toAlgHom_ofComp_surjective {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_3} {T : Type u_7} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) : Function.Surjective ⇑(Q.ofComp P).toAlgHom

noncomputable def Algebra.Generators.toExtendScalars {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_7} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (P : Generators R T ι) : P.Hom (extendScalars S P)

Given families of generators X ⊆ T, there is a map R[X] → S[X].

@[simp]

theorem Algebra.Generators.toExtendScalars_val {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_7} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (P : Generators R T ι) (n : ι) : P.toExtendScalars.val n = MvPolynomial.X n

noncomputable def Algebra.Generators.Hom.toExtensionHom {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S' ι'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : P.Hom P') : P.toExtension.Hom P'.toExtension

Reinterpret a hom between generators as a hom between extensions.

@[simp]

theorem Algebra.Generators.Hom.toExtensionHom_toRingHom {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S' ι'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : P.Hom P') : f.toExtensionHom.toRingHom = f.toAlgHom.toRingHom

@[simp]

theorem Algebra.Generators.Hom.toExtensionHom_id {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) : (Hom.id P).toExtensionHom = Extension.Hom.id P.toExtension

@[simp]

theorem Algebra.Generators.Hom.toExtensionHom_comp {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Generators R' S' ι') {R'' : Type u_4} {S'' : Type u_5} {ι'' : Type u_6} [CommRing R''] [CommRing S''] [Algebra R'' S''] (P'' : Generators R'' S'' ι'') [Algebra R R'] [Algebra R' R''] [Algebra R' S''] [Algebra S S'] [Algebra S' S''] [Algebra S S''] [Algebra R S'] [IsScalarTower R S S'] [Algebra R R''] [Algebra R S''] [IsScalarTower R R'' S''] [IsScalarTower R S S''] [IsScalarTower R' R'' S''] [IsScalarTower R' S' S''] [IsScalarTower S S' S''] [IsScalarTower R R' R''] [IsScalarTower R R' S'] (f : P'.Hom P'') (g : P.Hom P') : (f.comp g).toExtensionHom = f.toExtensionHom.comp g.toExtensionHom

theorem Algebra.Generators.Hom.toExtensionHom_toAlgHom_apply {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Generators R' S' ι') [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : P.Hom P') (x : P.toExtension.Ring) : f.toExtensionHom.toAlgHom x = f.toAlgHom x

@[reducible, inline]

noncomputable abbrev Algebra.Generators.ker {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) : Ideal P.Ring

The kernel of a presentation.

theorem Algebra.Generators.ker_eq_ker_aeval_val {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) : P.ker = RingHom.ker (MvPolynomial.aeval P.val)

theorem Algebra.Generators.aeval_val_eq_zero {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S ι} {x : P.Ring} (hx : x ∈ P.ker) : (MvPolynomial.aeval P.val) x = 0

theorem Algebra.Generators.ker_naive {R : Type u} [CommRing R] {σ : Type u_8} {I : Ideal (MvPolynomial σ R)} (s : MvPolynomial σ R ⧸ I → MvPolynomial σ R) (hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x) : (naive s hs).ker = I

theorem Algebra.Generators.map_toComp_ker {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_3} {T : Type u_7} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) : Ideal.map (Q.toComp P).toAlgHom P.ker = RingHom.ker (Q.ofComp P).toAlgHom

noncomputable def Algebra.Generators.kerCompPreimage {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_3} {T : Type u_7} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) (x : ↥Q.ker) : ↥(Q.comp P).ker

Given R[X] → S and S[Y] → T, this is the lift of an element in ker(S[Y] → T) to ker(R[X][Y] → S[Y] → T) constructed from P.σ.

theorem Algebra.Generators.ofComp_kerCompPreimage {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_3} {T : Type u_7} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) (x : ↥Q.ker) : (Q.ofComp P).toAlgHom ↑(Q.kerCompPreimage P x) = ↑x

theorem Algebra.Generators.map_ofComp_ker {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_3} {T : Type u_7} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) : Ideal.map (Q.ofComp P).toAlgHom (Q.comp P).ker = Q.ker

theorem Algebra.Generators.ker_comp_eq_sup {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_3} {T : Type u_7} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T ι') (P : Generators R S ι) : (Q.comp P).ker = Ideal.map (Q.toComp P).toAlgHom P.ker ⊔ Ideal.comap (Q.ofComp P).toAlgHom Q.ker