Algebra homomorphisms out of a presented algebra

Let P be a presentation of an R-algebra S. Every family in an R-algebra T satisfying the relations of P is the family of values on the generators of an R-algebra homomorphism S →ₐ[R] T. This homomorphism is unique: an R-algebra homomorphism out of S is determined by its values on the generators (Algebra.Generators.algHom_ext, in TauCeti.RingTheory.Extension.Generators).

Main definitions

• Algebra.Presentation.lift P x hx: the R-algebra homomorphism out of S sending the generators of P to a family x satisfying the relations of P.

Main results

• Algebra.Presentation.lift_val: P.lift x hx sends the i-th generator to x i.
• MvPolynomial.map_ker_aeval_eq_ker_aeval_tmul: base change of the kernel of a surjection R[ι] → S is the kernel of the corresponding map B[ι] → B ⊗[R] S.
• Algebra.Presentation.ker_baseChange_eq_map: the kernel of the base change of a presentation is the extension of its kernel.

noncomputable def Algebra.Presentation.lift {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {ι : Type u_3} {σ : Type u_4} (P : Presentation R S ι σ) {T : Type u_5} [CommRing T] [Algebra R T] (x : ι → T) (hx : ∀ (r : σ), (MvPolynomial.aeval x) (P.relation r) = 0) : S →ₐ[R] T

The R-algebra homomorphism out of S sending the generators of the presentation P to a family x that satisfies the relations of P.

@[simp]

theorem Algebra.Presentation.lift_val {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {ι : Type u_3} {σ : Type u_4} (P : Presentation R S ι σ) {T : Type u_5} [CommRing T] [Algebra R T] (x : ι → T) (hx : ∀ (r : σ), (MvPolynomial.aeval x) (P.relation r) = 0) (i : ι) : (P.lift x hx) (P.val i) = x i

P.lift x hx sends the i-th generator of P to x i.

theorem Algebra.Presentation.ker_baseChange_eq_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {ι : Type u_3} {σ : Type u_4} (P : Presentation R S ι σ) (K : Type u_6) [CommRing K] [Algebra R K] : (baseChange K P).ker = Ideal.map (algebraMap P.Ring (baseChange K P).Ring) P.ker

The kernel of the base change of a presentation to K is the extension of its kernel.

theorem MvPolynomial.map_ker_aeval_eq_ker_aeval_tmul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {ι : Type u_3} {val : ι → S} (B : Type u_4) [CommRing B] [Algebra R B] (hϕ : Function.Surjective ⇑(aeval val)) : Ideal.map (map (algebraMap R B)) (RingHom.ker (aeval val)) = RingHom.ker (aeval fun (v : ι) => 1 ⊗ₜ[R] val v)

Base change of the kernel of a surjection from a polynomial ring onto S: if ϕ : R[ι] → S sends the variables to val, then for every commutative R-algebra B the kernel of the map B[ι] → B ⊗[R] S sending the variables to 1 ⊗ val i is the extension of ker ϕ to B[ι].