Families of generators: extensionality and base change

Let P be a family of generators of an R-algebra S, that is, a surjection R[ι] → S.

Main results

• Algebra.Generators.algHom_ext: two R-algebra homomorphisms out of S agreeing on the generators of P are equal.
• Algebra.Generators.algebraMap_baseChange_map: the base change of P along R → T is compatible with P: on polynomials with coefficients in R, the map T[ι] → T ⊗[R] S is R[ι] → S followed by S → T ⊗[R] S.

theorem Algebra.Generators.algHom_ext {R : Type u_1} {S : Type u_2} {ι : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) {T : Type u_4} [Semiring T] [Algebra R T] {f g : S →ₐ[R] T} (h : ∀ (i : ι), f (P.val i) = g (P.val i)) : f = g

Two R-algebra homomorphisms out of S that agree on the generators of P are equal.

theorem Algebra.Generators.algebraMap_baseChange_map {R : Type u_1} {S : Type u_2} {ι : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (P : Generators R S ι) (T : Type u_4) [CommRing T] [Algebra R T] (x : P.Ring) : (algebraMap (baseChange T P).Ring (TensorProduct R T S)) ((MvPolynomial.map (algebraMap R T)) x) = TensorProduct.includeRight ((algebraMap P.Ring S) x)

The base change T[ι] → T ⊗[R] S of generators P of S extends R[ι] → S: on polynomials with coefficients in R, it is R[ι] → S followed by S → T ⊗[R] S.