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

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

noncomputable 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

Equations

• ⋯ = ⋯

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 : S) (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_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

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

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_σ {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

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

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_1 : CommRing S} {inst_2 : Algebra R S} {P : Algebra.Generators R S} {R' : Type u_1} {S' : Type u_2} {inst_3 : CommRing R'} {inst_4 : CommRing S'} {inst_5 : Algebra R' S'} {P' : Algebra.Generators R' S'} {inst_6 : Algebra S S'} {x y : P.Hom P'}, x.val = y.val → x = y

@[simp]

theorem Algebra.Generators.Hom.aeval_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'] (self : P.Hom P') (i : P.vars) : (MvPolynomial.aeval P'.val) (self.val i) = (algebraMap S S') (P.val i)

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

@[reducible, inline]

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 = RingHom.ker (algebraMap P.Ring S)

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)

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

The cotangent space of a presentation. This is a type synonym so that P = R[X] can act on it through the action of S without creating a diamond.

Equations

• P.Cotangent = P.ker.Cotangent

noncomputable instance Algebra.Generators.instAddCommGroupCotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) : AddCommGroup P.Cotangent

Equations

• P.instAddCommGroupCotangent = inferInstanceAs (AddCommGroup P.ker.Cotangent)

def Algebra.Generators.Cotangent.of {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} (x : P.ker.Cotangent) : P.Cotangent

The identity map P.ker.Cotangent → P.Cotangent into the type synonym.

Equations

• Algebra.Generators.Cotangent.of x = x

def Algebra.Generators.Cotangent.val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} (x : P.Cotangent) : P.ker.Cotangent

The identity map P.Cotangent → P.ker.Cotangent from the type synonym.

Equations

• x.val = x

theorem Algebra.Generators.Cotangent.ext {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} {x : P.Cotangent} {y : P.Cotangent} (e : x.val = y.val) : x = y

@[simp]

theorem Algebra.Generators.Cotangent.val_add {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} (x : P.Cotangent) (y : P.Cotangent) : (x + y).val = x.val + y.val

@[simp]

theorem Algebra.Generators.Cotangent.val_zero {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} : Algebra.Generators.Cotangent.val 0 = 0

@[simp]

theorem Algebra.Generators.Cotangent.of_add {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} (w : P.ker.Cotangent) (z : P.ker.Cotangent) : Algebra.Generators.Cotangent.of (w + z) = Algebra.Generators.Cotangent.of w + Algebra.Generators.Cotangent.of z

@[simp]

theorem Algebra.Generators.Cotangent.of_zero {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} : Algebra.Generators.Cotangent.of 0 = 0

@[simp]

theorem Algebra.Generators.Cotangent.of_val {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} (x : P.Cotangent) : Algebra.Generators.Cotangent.of x.val = x

@[simp]

theorem Algebra.Generators.Cotangent.val_of {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} (w : P.ker.Cotangent) : (Algebra.Generators.Cotangent.of w).val = w

@[simp]

theorem Algebra.Generators.Cotangent.val_sub {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} (x : P.Cotangent) (y : P.Cotangent) : (x - y).val = x.val - y.val

theorem Algebra.Generators.Cotangent.smul_eq_zero_of_mem {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} (p : P.Ring) (hp : p ∈ P.ker) (m : P.ker.Cotangent) : p • m = 0

noncomputable instance Algebra.Generators.Cotangent.module {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} : Module S P.Cotangent

Equations

• Algebra.Generators.Cotangent.module = Module.mk ⋯ ⋯

noncomputable instance Algebra.Generators.Cotangent.module' {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₀ S] : Module R₀ P.Cotangent

Equations

• Algebra.Generators.Cotangent.module' = Module.compHom P.Cotangent (algebraMap R₀ S)

instance Algebra.Generators.instIsScalarTowerCotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} {R₁ : Type u_1} {R₂ : Type u_2} [CommRing R₁] [CommRing R₂] [Algebra R₁ S] [Algebra R₂ S] [Algebra R₁ R₂] [IsScalarTower R₁ R₂ S] : IsScalarTower R₁ R₂ P.Cotangent

Equations

• ⋯ = ⋯

theorem Algebra.Generators.Cotangent.val_smul''' {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₀ S] (r : R₀) (x : P.Cotangent) : (r • x).val = P.σ ((algebraMap R₀ S) r) • x.val

@[simp]

theorem Algebra.Generators.Cotangent.val_smul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} (r : S) (x : P.Cotangent) : (r • x).val = P.σ r • x.val

@[simp]

theorem Algebra.Generators.Cotangent.val_smul' {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} (r : P.Ring) (x : P.Cotangent) : (r • x).val = r • x.val

@[simp]

theorem Algebra.Generators.Cotangent.val_smul'' {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} (r : R) (x : P.Cotangent) : (r • x).val = r • x.val

def Algebra.Generators.Cotangent.mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} : ↥P.ker →ₗ[P.Ring] P.Cotangent

The quotient map from the kernel of P = R[X] → S onto the cotangent space.

Equations

• Algebra.Generators.Cotangent.mk = { toFun := fun (x : ↥P.ker) => Algebra.Generators.Cotangent.of (P.ker.toCotangent x), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Algebra.Generators.Cotangent.val_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} (x : ↥P.ker) : (Algebra.Generators.Cotangent.mk x).val = P.ker.toCotangent x

theorem Algebra.Generators.Cotangent.mk_surjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} : Function.Surjective ⇑Algebra.Generators.Cotangent.mk

noncomputable def Algebra.Generators.Cotangent.map {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.Cotangent →ₗ[S] P'.Cotangent

A hom between families of generators induce a map between cotangent spaces.

Equations

• Algebra.Generators.Cotangent.map f = { toFun := fun (x : P.Cotangent) => Algebra.Generators.Cotangent.of ((P.ker.mapCotangent P'.ker f.toAlgHom ⋯) x.val), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Algebra.Generators.Cotangent.map_mk {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.ker) : (Algebra.Generators.Cotangent.map f) (Algebra.Generators.Cotangent.mk x) = Algebra.Generators.Cotangent.mk ⟨f.toAlgHom ↑x, ⋯⟩

@[simp]

theorem Algebra.Generators.Cotangent.map_id {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} : Algebra.Generators.Cotangent.map (Algebra.Generators.Hom.id P) = LinearMap.id

theorem Algebra.Generators.Cotangent.map_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' R''] [Algebra R' S''] [Algebra S S'] [Algebra S' S''] [Algebra S S''] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [Algebra R R''] [IsScalarTower R R' R''] [IsScalarTower R' R'' S''] [IsScalarTower R' S' S''] [IsScalarTower S S' S''] [Algebra R S''] [IsScalarTower R R'' S''] [IsScalarTower R S S''] (f : P.Hom P') (g : P'.Hom P'') : Algebra.Generators.Cotangent.map (g.comp f) = ↑S (Algebra.Generators.Cotangent.map g) ∘ₗ Algebra.Generators.Cotangent.map f