Quadratic form structures related to Module.Dual
#
Main definitions #
BilinForm.dualProd R M
, the bilinear form on(f, x) : Module.Dual R M × M
defined asf x
.QuadraticForm.dualProd R M
, the quadratic form on(f, x) : Module.Dual R M × M
defined asf x
.QuadraticForm.toDualProd : (Q.prod <| -Q) →qᵢ QuadraticForm.dualProd R M
a form-preserving map from(Q.prod <| -Q)
toQuadraticForm.dualProd R M
.
@[simp]
theorem
BilinForm.dualProd_apply
(R : Type u_1)
(M : Type u_2)
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(x : Module.Dual R M × M)
(y : Module.Dual R M × M)
:
BilinForm.bilin (BilinForm.dualProd R M) x y = ↑y.fst x.snd + ↑x.fst y.snd
def
BilinForm.dualProd
(R : Type u_1)
(M : Type u_2)
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
BilinForm R (Module.Dual R M × M)
The symmetric bilinear form on Module.Dual R M × M
defined as
B (f, x) (g, y) = f y + g x
.
Instances For
theorem
BilinForm.isSymm_dualProd
(R : Type u_1)
(M : Type u_2)
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
theorem
BilinForm.nondenerate_dualProd
(R : Type u_1)
(M : Type u_2)
[CommRing R]
[AddCommGroup M]
[Module R M]
:
@[simp]
theorem
QuadraticForm.dualProd_apply
(R : Type u_1)
(M : Type u_2)
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(p : Module.Dual R M × M)
:
↑(QuadraticForm.dualProd R M) p = ↑p.fst p.snd
def
QuadraticForm.dualProd
(R : Type u_1)
(M : Type u_2)
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
QuadraticForm R (Module.Dual R M × M)
The quadratic form on Module.Dual R M × M
defined as Q (f, x) = f x
.
Instances For
@[simp]
theorem
BilinForm.dualProd.toQuadraticForm
(R : Type u_1)
(M : Type u_2)
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
@[simp]
theorem
QuadraticForm.dualProdIsometry_invFun
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
(f : M ≃ₗ[R] N)
:
∀ (a : Module.Dual R N × N),
LinearEquiv.invFun (QuadraticForm.dualProdIsometry f).toLinearEquiv a = ↑(AddEquiv.symm (AddEquiv.prodCongr ↑(LinearEquiv.dualMap (LinearEquiv.symm f)) ↑f)) a
@[simp]
theorem
QuadraticForm.dualProdIsometry_toFun
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
(f : M ≃ₗ[R] N)
:
∀ (a : Module.Dual R M × M),
↑(QuadraticForm.dualProdIsometry f) a = ↑(AddEquiv.prodCongr ↑(LinearEquiv.dualMap (LinearEquiv.symm f)) ↑f) a
def
QuadraticForm.dualProdIsometry
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
(f : M ≃ₗ[R] N)
:
Any module isomorphism induces a quadratic isomorphism between the corresponding dual_prod.
Instances For
@[simp]
theorem
QuadraticForm.dualProdProdIsometry_toFun
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
:
∀ (a : Module.Dual R (M × N) × M × N),
↑QuadraticForm.dualProdProdIsometry a = ((LinearMap.comp a.fst (LinearMap.inl R M N), a.snd.fst), LinearMap.comp a.fst (LinearMap.inr R M N), a.snd.snd)
@[simp]
theorem
QuadraticForm.dualProdProdIsometry_invFun
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
:
∀ (a : (Module.Dual R M × M) × Module.Dual R N × N),
LinearEquiv.invFun QuadraticForm.dualProdProdIsometry.toLinearEquiv a = ↑↑(LinearEquiv.symm
(LinearEquiv.prod (LinearEquiv.symm (Module.dualProdDualEquivDual R M N)) (LinearEquiv.refl R (M × N))))
(↑↑(LinearEquiv.prodProdProdComm R (Module.Dual R M) M (Module.Dual R N) N) a)
def
QuadraticForm.dualProdProdIsometry
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
:
QuadraticForm.IsometryEquiv (QuadraticForm.dualProd R (M × N))
(QuadraticForm.prod (QuadraticForm.dualProd R M) (QuadraticForm.dualProd R N))
QuadraticForm.dualProd
commutes (isometrically) with QuadraticForm.prod
.
Instances For
@[simp]
theorem
QuadraticForm.toDualProd_apply
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
[Invertible 2]
(i : M × M)
:
↑(QuadraticForm.toDualProd Q) i = (↑(↑BilinForm.toLin (↑QuadraticForm.associated Q)) i.fst + ↑(↑BilinForm.toLin (↑QuadraticForm.associated Q)) i.snd,
i.fst - i.snd)
def
QuadraticForm.toDualProd
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
[Invertible 2]
:
QuadraticForm.prod Q (-Q) →qᵢ QuadraticForm.dualProd R M
The isometry sending (Q.prod $ -Q)
to (QuadraticForm.dualProd R M)
.
This is σ
from Proposition 4.8, page 84 of
[Hermitian K-Theory and Geometric Applications][hyman1973]; though we swap the order of the pairs.
Instances For
TODO: show that QuadraticForm.toDualProd
is an QuadraticForm.IsometryEquiv