Quadratic form structures related to Module.Dual
#
Main definitions #
LinearMap.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
LinearMap.dualProd_apply_apply
(R : Type u_1)
(M : Type u_2)
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(a : Module.Dual R M × M)
(a : Module.Dual R M × M)
:
((LinearMap.dualProd R M) a✝) a = a.1 a✝.2 + a✝.1 a.2
def
LinearMap.dualProd
(R : Type u_1)
(M : Type u_2)
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
LinearMap.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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LinearMap.isSymm_dualProd
(R : Type u_1)
(M : Type u_2)
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
theorem
LinearMap.separatingLeft_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.1 p.2
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
.
Equations
- QuadraticForm.dualProd R M = { toFun := fun (p : Module.Dual R M × M) => p.1 p.2, toFun_smul := ⋯, exists_companion' := ⋯ }
Instances For
@[simp]
theorem
LinearMap.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), (QuadraticForm.dualProdIsometry f).invFun a = ((↑f.symm.dualMap).prodCongr ↑f).symm 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 = ((↑f.symm.dualMap).prodCongr ↑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.
Equations
- QuadraticForm.dualProdIsometry f = { toLinearEquiv := f.dualMap.symm.prod f, map_app' := ⋯ }
Instances For
@[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),
QuadraticForm.dualProdProdIsometry.invFun a = ((Module.dualProdDualEquivDual R M N).symm.prod (LinearEquiv.refl R (M × N))).symm ((a.1.1, a.2.1), a.1.2, a.2.2)
@[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 = ((a.1 ∘ₗ LinearMap.inl R M N, a.2.1), a.1 ∘ₗ LinearMap.inr R M N, a.2.2)
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]
:
QuadraticMap.IsometryEquiv (QuadraticForm.dualProd R (M × N))
(QuadraticMap.prod (QuadraticForm.dualProd R M) (QuadraticForm.dualProd R N))
QuadraticForm.dualProd
commutes (isometrically) with QuadraticForm.prod
.
Equations
- One or more equations did not get rendered due to their size.
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)
:
def
QuadraticForm.toDualProd
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
[Invertible 2]
:
QuadraticMap.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; though we swap the order of the pairs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
TODO: show that QuadraticForm.toDualProd
is an QuadraticForm.IsometryEquiv