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) [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
• algebra : Algebra (MvPolynomial self.vars 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 self.vars R) S = ↑(MvPolynomial.aeval self.val)

@[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

• P.Ring = MvPolynomial P.vars R

def Algebra.Generators.σ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : 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 : 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 : Generators R S) (s : S) : (MvPolynomial.aeval P.val) (P.σ 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] : IsScalarTower R₀ P.Ring 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) : (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 : 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 : 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 : 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)) : 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_σ' := ⋯, algebraMap_eq := ⋯ }

@[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) : (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)) : (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)) : 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] : 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) : 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 : adjoin R s = ⊤) : 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] : 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_σ' := ⋯, algebraMap_eq := ⋯ }

@[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_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_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

@[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

noncomputable def Algebra.Generators.toExtension {R : Type u} {S : Type v} [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.

Equations

• P.toExtension = { Ring := P.Ring, commRing := MvPolynomial.instCommRingMvPolynomial, algebra₁ := MvPolynomial.algebra, algebra₂ := P.algebra, isScalarTower := ⋯, σ := P.σ, algebraMap_σ := ⋯ }

@[simp]

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

@[simp]

theorem Algebra.Generators.toExtension_Ring {R : Type u} {S : Type v} [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} [CommRing R] [CommRing S] [Algebra R S] (P : 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 : 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 : 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] : 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) : (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

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

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) : 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 : 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) : (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 : 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) : 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_σ' := ⋯, algebraMap_eq := ⋯ }

@[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) : (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 : 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.

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

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

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

Equations

• P.reindex e = { vars := ι, val := P.val ∘ ⇑e, σ' := ⇑(MvPolynomial.rename ⇑e.symm) ∘ P.σ, aeval_val_σ' := ⋯, algebraMap_eq := ⋯ }

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.

• 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_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') : 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 : 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) : (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 : 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) : 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 : 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) : 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 : 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') : ↑(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 : 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) : (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 : 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

• 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 : 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

• 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 : 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 : Generators R S) (n : P.vars) : (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 : Generators R S) : (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 : 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

• 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 : 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

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

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) : (Q.toComp P).toAlgHom = MvPolynomial.rename Sum.inr

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

• 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 : Generators S T) (P : Generators R S) (i : (Q.comp P).vars) : (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} [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) : (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} [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) : (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} [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) : (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} [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) : Function.Surjective ⇑(Q.ofComp P).toAlgHom

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) : P.Hom (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 : 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 : 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') : 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 : 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') : 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 : 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} [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') : (f.comp g).toExtensionHom = f.toExtensionHom.comp g.toExtensionHom

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) : f.toExtensionHom.toAlgHom x = f.toAlgHom x

@[reducible, inline]

noncomputable abbrev Algebra.Generators.ker {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : 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 : Generators R S) : P.ker = RingHom.ker (MvPolynomial.aeval P.val)

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) : (MvPolynomial.aeval P.val) x = 0

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) : 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} [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

• Q.kerCompPreimage P x = ⟨Finsupp.sum ↑x fun (n : Q.vars →₀ ℕ) (r : S) => (MvPolynomial.rename Sum.inr) (P.σ r) * (MvPolynomial.monomial (Finsupp.mapDomain Sum.inl n)) 1, ⋯⟩

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) : 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} [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) : (Q.comp P).ker = Ideal.map (Q.toComp P).toAlgHom P.ker ⊔ Ideal.comap (Q.ofComp P).toAlgHom Q.ker