Documentation

Mathlib.Algebra.QuadraticAlgebra.AlgHom

Algebra homomorphisms between quadratic algebras #

An R-algebra homomorphism f : QuadraticAlgebra R a b →ₐ[R] QuadraticAlgebra R a' b' is determined by the image of ω, and its matrix in the bases 1, ω is [1, (f ω).re; 0, (f ω).im]. Furthermore f is injective exactly when (f ω).im is regular, bijective exactly when it is a unit. Finally, an injective f preserves the trace and the norm, and commutes with conjugation.

Main results #

source
theorem QuadraticAlgebra.toMatrix_algHom {R : Type u_1} [CommRing R] {a b a' b' : R} (f : QuadraticAlgebra R a b →ₐ[R] QuadraticAlgebra R a' b') :
(LinearMap.toMatrix (basis a b) (basis a' b')) f.toLinearMap = !![1, (f omega).re; 0, (f omega).im]

The matrix of an algebra homomorphism f between quadratic algebras in the bases 1, ω is [1, (f ω).re; 0, (f ω).im] since f 1 = 1. In particular, its determinant is (f ω).im, see det_toMatrix_algHom.

source
theorem QuadraticAlgebra.det_toMatrix_algHom {R : Type u_1} [CommRing R] {a b a' b' : R} (f : QuadraticAlgebra R a b →ₐ[R] QuadraticAlgebra R a' b') :
((LinearMap.toMatrix (basis a b) (basis a' b')) f.toLinearMap).det = (f omega).im

The determinant of an algebra homomorphism f between quadratic algebras, in the bases 1, ω, is (f ω).im.

source
theorem QuadraticAlgebra.isRegular_im_omega_iff_injective {R : Type u_1} [CommRing R] {a b a' b' : R} (f : QuadraticAlgebra R a b →ₐ[R] QuadraticAlgebra R a' b') :
IsRegular (f omega).im ↔ Function.Injective ⇑f

An algebra homomorphism f between quadratic algebras is injective exactly when (f ω).im is regular, which is the determinant of f in the bases 1, ω, see det_toMatrix_algHom.

source
theorem QuadraticAlgebra.isUnit_im_omega_iff_bijective {R : Type u_1} [CommRing R] {a b a' b' : R} (f : QuadraticAlgebra R a b →ₐ[R] QuadraticAlgebra R a' b') :
IsUnit (f omega).im ↔ Function.Bijective ⇑f

An algebra homomorphism f between quadratic algebras is bijective exactly when (f ω).im is a unit, the injective case being isRegular_im_omega_iff_injective.

source
theorem QuadraticAlgebra.isUnit_im_omega_of_algEquiv {R : Type u_1} [CommRing R] {a b a' b' : R} (e : QuadraticAlgebra R a b ≃ₐ[R] QuadraticAlgebra R a' b') :
IsUnit (e omega).im

Any R-algebra isomorphism between quadratic algebras sends ω to an element whose imaginary part is a unit.

source
theorem QuadraticAlgebra.trace_algHom_omega {R : Type u_1} [CommRing R] {a b a' b' : R} (f : QuadraticAlgebra R a b →ₐ[R] QuadraticAlgebra R a' b') (hf : Function.Injective ⇑f) :
trace (f omega) = b

An injective algebra homomorphism sends ω to an element of trace b.

source
theorem QuadraticAlgebra.norm_algHom_omega {R : Type u_1} [CommRing R] {a b a' b' : R} (f : QuadraticAlgebra R a b →ₐ[R] QuadraticAlgebra R a' b') (hf : Function.Injective ⇑f) :
norm (f omega) = -a

An injective algebra homomorphism sends ω to an element of norm -a.

source
theorem QuadraticAlgebra.trace_algHom {R : Type u_1} [CommRing R] {a b a' b' : R} (f : QuadraticAlgebra R a b →ₐ[R] QuadraticAlgebra R a' b') (hf : Function.Injective ⇑f) (x : QuadraticAlgebra R a b) :
trace (f x) = trace x

An injective algebra homomorphism preserves traces.

source
theorem QuadraticAlgebra.algHom_star {R : Type u_1} [CommRing R] {a b a' b' : R} (f : QuadraticAlgebra R a b →ₐ[R] QuadraticAlgebra R a' b') (hf : Function.Injective ⇑f) (x : QuadraticAlgebra R a b) :
f (star x) = star (f x)

An injective algebra homomorphism commutes with conjugation.

source
theorem QuadraticAlgebra.norm_algHom {R : Type u_1} [CommRing R] {a b a' b' : R} (f : QuadraticAlgebra R a b →ₐ[R] QuadraticAlgebra R a' b') (hf : Function.Injective ⇑f) (x : QuadraticAlgebra R a b) :
norm (f x) = norm x

An injective algebra homomorphism preserves norms.