Quadratic algebras are stable under base change

Let R → S be a base change. We show that QuadraticAlgebra S (algebraMap R S a) (algebraMap R S b) is the base change of QuadraticAlgebra R a b along it, that is, that the square

          R             →               S
          ↓                             ↓
QuadraticAlgebra R a b  →  QuadraticAlgebra S (algebraMap R S a) (algebraMap R S b)

is a pushout.

Main results

• QuadraticAlgebra.isPushout: the base change square is a pushout.

• QuadraticAlgebra.baseChangeEquiv: the resulting isomorphism S ⊗[R] QuadraticAlgebra R a b ≃ₐ[S] QuadraticAlgebra S (algebraMap R S a) (algebraMap R S b)

Implementation notes

QuadraticAlgebra.algebra is activated as a local instance throughout this file.

@[simp]

theorem QuadraticAlgebra.algebraMap_eq_mapRingHom {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (a b : R) : algebraMap (QuadraticAlgebra R a b) (QuadraticAlgebra S ((algebraMap R S) a) ((algebraMap R S) b)) = mapRingHom (algebraMap R S) a b

instance QuadraticAlgebra.instIsScalarTowerCoeRingHomAlgebraMap {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (a b : R) : IsScalarTower R (QuadraticAlgebra R a b) (QuadraticAlgebra S ((algebraMap R S) a) ((algebraMap R S) b))

instance QuadraticAlgebra.isPushout {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (a b : R) : Algebra.IsPushout R S (QuadraticAlgebra R a b) (QuadraticAlgebra S ((algebraMap R S) a) ((algebraMap R S) b))

A quadratic algebra is stable under base change.

noncomputable def QuadraticAlgebra.baseChangeEquiv {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (a b : R) : TensorProduct R S (QuadraticAlgebra R a b) ≃ₐ[S] QuadraticAlgebra S ((algebraMap R S) a) ((algebraMap R S) b)

The base change of QuadraticAlgebra R a b along R → S, as an algebra isomorphism.

Equations

• QuadraticAlgebra.baseChangeEquiv S a b = Algebra.IsPushout.equiv R S (QuadraticAlgebra R a b) (QuadraticAlgebra S ((algebraMap R S) a) ((algebraMap R S) b))

@[simp]

theorem QuadraticAlgebra.baseChangeEquiv_tmul {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (a b : R) (s : S) (x : QuadraticAlgebra R a b) : (baseChangeEquiv S a b) (s ⊗ₜ[R] x) = s • (mapRingHom (algebraMap R S) a b) x