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.

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.

• vars : Type w

  The type of variables.

• val : self.vars → S

  The assignment of each variable to a value in S.

• σ' : S → MvPolynomial self.vars R

  A section of R[X] → S.

• aeval_val_σ' (s : S) : (MvPolynomial.aeval self.val) (self.σ' s) = s

@[reducible, inline]

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

The polynomial ring wrt a family of generators.

Equations

• P.Ring = MvPolynomial P.vars R

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

The designated section of wrt a family of generators.

Equations

• P.σ = P.σ'

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

See Note [custom simps projection]

Equations

• Algebra.Generators.Simps.σ P = P.σ

@[simp]

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

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

Equations

• P.instRing = (MvPolynomial.aeval P.val).toAlgebra

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

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

@[simp]

theorem Algebra.Generators.algebraMap_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.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} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) (x y : S) : P.σ x • y = x * y

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

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

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

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

Equations

• Algebra.Generators.ofSurjective val h = { vars := vars, val := val, σ' := fun (x : S) => ⋯.choose, aeval_val_σ' := ⋯ }

@[simp]

theorem Algebra.Generators.ofSurjective_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {vars : Type u_1} (val : vars → S) (h : Function.Surjective ⇑(MvPolynomial.aeval val)) (a✝ : vars) : (Algebra.Generators.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 : vars → S) (h : Function.Surjective ⇑(MvPolynomial.aeval val)) : (Algebra.Generators.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)) : Algebra.Generators R S

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

Equations

• Algebra.Generators.ofSurjectiveAlgebraMap h = Algebra.Generators.ofSurjective PEmpty.elim ⋯

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

The canonical generators for R as an R-algebra.

Equations

• Algebra.Generators.id = Algebra.Generators.ofSurjectiveAlgebraMap ⋯

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) : Algebra.Generators R S

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

Equations

• Algebra.Generators.ofAlgHom f h = Algebra.Generators.ofSurjective (⇑f ∘ MvPolynomial.X) ⋯

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

Construct Generators from a family of generators of S.

Equations

• Algebra.Generators.ofSet hs = Algebra.Generators.ofSurjective Subtype.val ⋯

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

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

Equations

• Algebra.Generators.self R S = { vars := S, val := id, σ' := MvPolynomial.X, aeval_val_σ' := ⋯ }

@[simp]

theorem Algebra.Generators.self_vars (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : (Algebra.Generators.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) : (Algebra.Generators.self R S).val a = id a

@[simp]

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

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

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

Equations

• P.toExtension = Algebra.Extension.mk P.Ring P.σ ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def Algebra.Generators.localizationAway {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : Algebra.Generators 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.

@[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) : (Algebra.Generators.localizationAway r).val x✝ = IsLocalization.Away.invSelf r

theorem Algebra.Generators.localizationAway_vars {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : (Algebra.Generators.localizationAway r).vars = Unit

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) : (Algebra.Generators.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} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) : Algebra.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.

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 : Algebra.Generators S T) (P : Algebra.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 : Algebra.Generators S T) (P : Algebra.Generators R S) (x : T) : (Q.comp P).σ x = Finsupp.sum (Q.σ x) fun (n : Q.vars →₀ ℕ) (r : S) => (MvPolynomial.rename Sum.inr) (P.σ r) * (MvPolynomial.monomial (Finsupp.mapDomain Sum.inl n)) 1

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 : Algebra.Generators S T) (P : Algebra.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 : Algebra.Generators R T) : Algebra.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.

Equations

• Algebra.Generators.extendScalars S P = { vars := P.vars, val := P.val, σ' := fun (x : T) => (MvPolynomial.map (algebraMap R S)) (P.σ x), aeval_val_σ' := ⋯ }

@[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 : Algebra.Generators R T) (a✝ : P.vars) : (Algebra.Generators.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 : Algebra.Generators R T) : (Algebra.Generators.extendScalars S P).vars = P.vars

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 : Algebra.Generators R S) : Algebra.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.

Equations

• P.baseChange = Algebra.Generators.ofSurjective (fun (x : P.vars) => 1 ⊗ₜ[R] P.val x) ⋯

@[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 : Algebra.Generators R S) (x : P.vars) : P.baseChange.val x = 1 ⊗ₜ[R] P.val x

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 : Algebra.Generators R S) : P.baseChange.vars = P.vars

structure Algebra.Generators.Hom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Algebra.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.vars → P'.Ring

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

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

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

Equations

• f.toAlgHom = MvPolynomial.aeval f.val

@[simp]

theorem Algebra.Generators.Hom.algebraMap_toAlgHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.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} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Generators R' S'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') (i : P.vars) : f.toAlgHom (MvPolynomial.X i) = f.val i

theorem Algebra.Generators.Hom.toAlgHom_C {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.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} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.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 : Algebra.Generators R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.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 : Algebra.Generators R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Generators R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : P.Hom P') : ↑(Algebra.Generators.Hom.equivAlgHom f) = f.toAlgHom

@[simp]

theorem Algebra.Generators.Hom.equivAlgHom_symm_apply_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.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) : (Algebra.Generators.Hom.equivAlgHom.symm f).val i = ↑f (MvPolynomial.X i)

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

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

Equations

• P.defaultHom P' = { val := P'.σ ∘ ⇑(algebraMap S S') ∘ P.val, aeval_val := ⋯ }

@[simp]

theorem Algebra.Generators.defaultHom_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Algebra.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 : Algebra.Generators R S) {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Algebra.Generators R' S') [Algebra S S'] : Inhabited (P.Hom P')

Equations

• P.instInhabitedHom P' = { default := P.defaultHom P' }

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

The identity hom.

Equations

• Algebra.Generators.Hom.id P = { val := MvPolynomial.X, aeval_val := ⋯ }

@[simp]

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

@[simp]

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

noncomputable def Algebra.Generators.Hom.comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Generators R' S'} {R'' : Type u_4} {S'' : Type u_5} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Algebra.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

• f.comp g = { val := fun (x : P.vars) => (MvPolynomial.aeval f.val) (g.val x), aeval_val := ⋯ }

@[simp]

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

• Q.toComp P = { val := fun (i : P.vars) => MvPolynomial.X (Sum.inr i), aeval_val := ⋯ }

@[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 : Algebra.Generators S T) (P : Algebra.Generators R S) (i : P.vars) : (Q.toComp P).val i = MvPolynomial.X (Sum.inr i)

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 : Algebra.Generators S T) (P : Algebra.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

• Q.ofComp P = { val := fun (i : (Q.comp P).vars) => Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ P.val) i, aeval_val := ⋯ }

@[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 : Algebra.Generators S T) (P : Algebra.Generators R S) (i : (Q.comp P).vars) : (Q.ofComp P).val i = Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ P.val) i

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 : Algebra.Generators R T) : P.Hom (Algebra.Generators.extendScalars S P)

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

Equations

• P.toExtendScalars = { val := MvPolynomial.X, aeval_val := ⋯ }

@[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 : Algebra.Generators R T) (n : P.vars) : P.toExtendScalars.val n = MvPolynomial.X n

noncomputable def Algebra.Generators.Hom.toExtensionHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.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.

Equations

• f.toExtensionHom = { toRingHom := f.toAlgHom.toRingHom, toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }

@[simp]

theorem Algebra.Generators.Hom.toExtensionHom_toRingHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.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} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) : (Algebra.Generators.Hom.id P).toExtensionHom = Algebra.Extension.Hom.id P.toExtension

@[simp]

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

@[reducible, inline]

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

The kernel of a presentation.

Equations

• P.ker = P.toExtension.ker

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