Basic properties of quadratic maps #
This file records elementary consequences of the quadratic-map axioms.
Main results #
QuadraticMap.Anisotropic.comp: injective pullback preserves anisotropy.QuadraticMap.nontrivial_of_ne_zero: the source of a nonzero quadratic map is nontrivial.
theorem
QuadraticMap.nontrivial_of_ne_zero
{S : Type u_1}
{V : Type u_2}
{N : Type u_3}
[CommSemiring S]
[AddCommMonoid V]
[Module S V]
[AddCommMonoid N]
[Module S N]
{Q : QuadraticMap S V N}
(hQ : Q ≠ 0)
:
The source of a nonzero quadratic map is nontrivial.
theorem
QuadraticMap.Anisotropic.comp
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
[AddCommMonoid P]
[Module R P]
{Q : QuadraticMap R M N}
(hQ : Q.Anisotropic)
(f : P →ₗ[R] M)
(hf : Function.Injective ⇑f)
:
(Q.comp f).Anisotropic
An injective pullback of an anisotropic quadratic map is anisotropic.