Documentation

Mathlib.RingTheory.Extension.Generators

Generators of algebras #

Main definition #

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) [CommRing R] [CommRing S] [Algebra R S] :
Type (max (max u v) (w + 1))

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.
@[reducible, inline]
abbrev Algebra.Generators.Ring {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) :
Type (max w u)

The polynomial ring wrt a family of generators.

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

The designated section of wrt a family of generators.

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

See Note [custom simps projection]

Equations
@[simp]
theorem Algebra.Generators.aeval_val_σ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) (s : S) :
instance Algebra.Generators.instIsScalarTowerRing {R : Type u} {S : Type v} [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] :
@[simp]
theorem Algebra.Generators.algebraMap_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) (x : P.Ring) :
@[simp]
theorem Algebra.Generators.σ_smul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) (x y : S) :
P.σ x y = x * y
noncomputable def Algebra.Generators.ofSurjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {vars : Type u_1} (val : varsS) (h : Function.Surjective (MvPolynomial.aeval val)) :

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

Equations
@[simp]
theorem Algebra.Generators.ofSurjective_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {vars : Type u_1} (val : varsS) (h : Function.Surjective (MvPolynomial.aeval val)) (a✝ : vars) :
(ofSurjective val h).val a✝ = val a✝
theorem Algebra.Generators.ofSurjective_vars {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {vars : Type u_1} (val : varsS) (h : Function.Surjective (MvPolynomial.aeval val)) :
(ofSurjective val h).vars = vars
noncomputable def Algebra.Generators.ofSurjectiveAlgebraMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (h : Function.Surjective (algebraMap R S)) :

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

Equations
noncomputable def Algebra.Generators.id {R : Type u} [CommRing R] :

The canonical generators for R as an R-algebra.

Equations
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) :

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

Equations
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 = ) :

Construct Generators from a family of generators of S.

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

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

Equations
@[simp]
theorem Algebra.Generators.self_σ (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (n : S) :
@[simp]
theorem Algebra.Generators.self_vars (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :
(self R S).vars = S
@[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} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) :

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

Equations
@[simp]
@[simp]
theorem Algebra.Generators.toExtension_σ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) (a✝ : S) :
P.toExtension.σ a✝ = P.σ a✝
noncomputable def Algebra.Generators.localizationAway {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] :

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

Equations
  • One or more equations did not get rendered due to their size.
noncomputable def Algebra.Generators.comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T) (P : Generators R S) :

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Algebra.Generators.comp_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T) (P : Generators R S) (a✝ : Q.vars P.vars) :
(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} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T) (P : Generators R S) (x : T) :
theorem Algebra.Generators.comp_vars {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T) (P : Generators R S) :
(Q.comp P).vars = (Q.vars P.vars)
noncomputable def Algebra.Generators.extendScalars {R : Type u} (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (P : Generators R 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.

Equations
@[simp]
theorem Algebra.Generators.extendScalars_val {R : Type u} (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (P : Generators R T) (a✝ : P.vars) :
(extendScalars S P).val a✝ = P.val a✝
theorem Algebra.Generators.extendScalars_vars {R : Type u} (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (P : Generators R T) :
noncomputable def Algebra.Generators.baseChange {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] (P : Generators R 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.

Equations
@[simp]
theorem Algebra.Generators.baseChange_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] (P : Generators R S) (x : P.vars) :
theorem Algebra.Generators.baseChange_vars {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] (P : Generators R S) :
noncomputable def Algebra.Generators.reindex {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) {ι : Type u_1} (e : ι P.vars) :

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

Equations
theorem Algebra.Generators.reindex_vars {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) {ι : Type u_1} (e : ι P.vars) :
(P.reindex e).vars = ι
theorem Algebra.Generators.reindex_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) {ι : Type u_1} (e : ι P.vars) :
(P.reindex e).val = P.val e
structure Algebra.Generators.Hom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) {R' : Type u_1} {S' : Type u_2} [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.

theorem Algebra.Generators.Hom.ext_iff {R : Type u} {S : Type v} {inst✝ : CommRing R} {inst✝¹ : CommRing S} {inst✝² : Algebra R S} {P : Generators R S} {R' : Type u_1} {S' : Type u_2} {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} {inst✝ : CommRing R} {inst✝¹ : CommRing S} {inst✝² : Algebra R S} {P : Generators R S} {R' : Type u_1} {S' : Type u_2} {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} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') :

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

Equations
@[simp]
theorem Algebra.Generators.Hom.algebraMap_toAlgHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S} {R' : Type u_1} {S' : Type u_2} [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) :
@[simp]
theorem Algebra.Generators.Hom.toAlgHom_X {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') (i : P.vars) :
theorem Algebra.Generators.Hom.toAlgHom_C {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') (r : R) :
theorem Algebra.Generators.Hom.toAlgHom_monomial {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') (v : P.vars →₀ ) (r : R) :
f.toAlgHom ((MvPolynomial.monomial v) r) = r v.prod fun (x1 : P.vars) (x2 : ) => f.val x1 ^ x2
noncomputable def Algebra.Generators.Hom.equivAlgHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S} {R' : Type u_1} {S' : Type u_2} [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.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Algebra.Generators.Hom.equivAlgHom_apply_coe {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S} {R' : Type u_1} {S' : Type u_2} [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') :
@[simp]
theorem Algebra.Generators.Hom.equivAlgHom_symm_apply_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S} {R' : Type u_1} {S' : Type u_2} [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 : P.vars) :
def Algebra.Generators.defaultHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) {R' : Type u_1} {S' : Type u_2} [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'.

Equations
@[simp]
theorem Algebra.Generators.defaultHom_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Generators R' S') [Algebra S S'] (a✝ : P.vars) :
(P.defaultHom P').val a✝ = (P'.σ (algebraMap S S') P.val) a✝
instance Algebra.Generators.instInhabitedHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Generators R' S') [Algebra S S'] :
Inhabited (P.Hom P')
Equations
noncomputable def Algebra.Generators.Hom.id {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) :
P.Hom P

The identity hom.

Equations
@[simp]
theorem Algebra.Generators.Hom.id_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) (n : P.vars) :
@[simp]
noncomputable def Algebra.Generators.Hom.comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S'} {R'' : Type u_4} {S'' : Type u_5} [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.

Equations
@[simp]
theorem Algebra.Generators.Hom.comp_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Generators R' S'} {R'' : Type u_4} {S'' : Type u_5} [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 : P.vars) :
(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} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S} {R' : Type u_2} {S' : Type u_1} [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} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) {R' : Type u_2} {S' : Type u_1} [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} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) {R' : Type u_2} {S' : Type u_4} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Generators R' S') {R'' : Type u_1} {S'' : Type u_3} [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} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [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].

Equations
@[simp]
theorem Algebra.Generators.toComp_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T) (P : Generators R S) (i : P.vars) :
theorem Algebra.Generators.toComp_toAlgHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_2} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T) (P : Generators R S) :
noncomputable def Algebra.Generators.ofComp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [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].

Equations
@[simp]
theorem Algebra.Generators.ofComp_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T) (P : Generators R S) (i : (Q.comp P).vars) :
theorem Algebra.Generators.ofComp_toAlgHom_monomial_sumElim {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_2} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T) (P : Generators R S) (v₁ : Q.vars →₀ ) (v₂ : P.vars →₀ ) (a : R) :
theorem Algebra.Generators.toComp_toAlgHom_monomial {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_2} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T) (P : Generators R S) (j : P.vars →₀ ) (a : R) :
@[simp]
theorem Algebra.Generators.toAlgHom_ofComp_rename {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_2} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T) (P : Generators R S) (p : P.Ring) :
theorem Algebra.Generators.toAlgHom_ofComp_surjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_2} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T) (P : Generators R S) :
noncomputable def Algebra.Generators.toExtendScalars {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (P : Generators R T) :

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

Equations
@[simp]
theorem Algebra.Generators.toExtendScalars_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (P : Generators R T) (n : P.vars) :
noncomputable def Algebra.Generators.Hom.toExtensionHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S} {R' : Type u_1} {S' : Type u_2} [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') :

Reinterpret a hom between generators as a hom between extensions.

Equations
@[simp]
theorem Algebra.Generators.Hom.toExtensionHom_toRingHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S} {R' : Type u_1} {S' : Type u_2} [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') :
@[simp]
theorem Algebra.Generators.Hom.toExtensionHom_comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) {R' : Type u_4} {S' : Type u_1} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Generators R' S') {R'' : Type u_2} {S'' : Type u_3} [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') :
theorem Algebra.Generators.Hom.toExtensionHom_toAlgHom_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) {R' : Type u_2} {S' : Type u_1} [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) :
@[reducible, inline]
noncomputable abbrev Algebra.Generators.ker {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S) :

The kernel of a presentation.

Equations
theorem Algebra.Generators.aeval_val_eq_zero {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Generators R S} {x : P.Ring} (hx : x P.ker) :
theorem Algebra.Generators.map_toComp_ker {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_2} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T) (P : Generators R S) :
noncomputable def Algebra.Generators.kerCompPreimage {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [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.σ.

Equations
theorem Algebra.Generators.ofComp_kerCompPreimage {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {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 : Q.ker) :
(Q.ofComp P).toAlgHom (Q.kerCompPreimage P x) = x
theorem Algebra.Generators.map_ofComp_ker {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_2} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T) (P : Generators R S) :
theorem Algebra.Generators.ker_comp_eq_sup {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_2} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Generators S T) (P : Generators R S) :