Quadratic form structures related to module.dual #
Main definitions #
bilin_form.dual_prod R M, the bilinear form on(f, x) : module.dual R M × Mdefined asf x.quadratic_form.dual_prod R M, the quadratic form on(f, x) : module.dual R M × Mdefined asf x.quadratic_form.to_dual_prod : M × M →ₗ[R] module.dual R M × Ma form-preserving map from(Q.prod $ -Q)toquadratic_form.dual_prod R M. Note that we do not have the morphism version ofquadratic_form.isometry, so for now this is stated without full bundling.
def
bilin_form.dual_prod
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
bilin_form 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
- bilin_form.dual_prod R M = ⇑linear_map.to_bilin ((linear_map.applyₗ.comp (linear_map.snd R (module.dual R M) M)).compl₂ (linear_map.fst R (module.dual R M) M) + ((linear_map.applyₗ.comp (linear_map.snd R (module.dual R M) M)).compl₂ (linear_map.fst R (module.dual R M) M)).flip)
@[simp]
theorem
bilin_form.dual_prod_apply
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M]
(x y : module.dual R M × M) :
theorem
bilin_form.is_symm_dual_prod
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
(bilin_form.dual_prod R M).is_symm
theorem
bilin_form.nondenerate_dual_prod
(R : Type u_1)
(M : Type u_2)
[comm_ring R]
[add_comm_group M]
[module R M] :
def
quadratic_form.dual_prod
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
quadratic_form R (module.dual R M × M)
The quadratic form on module.dual R M × M defined as Q (f, x) = f x.
Equations
- quadratic_form.dual_prod R M = {to_fun := λ (p : module.dual R M × M), ⇑(p.fst) p.snd, to_fun_smul := _, exists_companion' := _}
@[simp]
theorem
quadratic_form.dual_prod_apply
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M]
(p : module.dual R M × M) :
@[simp]
theorem
bilin_form.dual_prod.to_quadratic_form
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
(bilin_form.dual_prod R M).to_quadratic_form = 2 • quadratic_form.dual_prod R M
def
quadratic_form.dual_prod_isometry
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(f : M ≃ₗ[R] N) :
(quadratic_form.dual_prod R M).isometry (quadratic_form.dual_prod R N)
Any module isomorphism induces a quadratic isomorphism between the corresponding dual_prod.
Equations
- quadratic_form.dual_prod_isometry f = {to_linear_equiv := f.dual_map.symm.prod f, map_app' := _}
@[simp]
theorem
quadratic_form.dual_prod_isometry_to_linear_equiv
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(f : M ≃ₗ[R] N) :
@[simp]
theorem
quadratic_form.dual_prod_prod_isometry_to_linear_equiv
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
quadratic_form.dual_prod_prod_isometry.to_linear_equiv = ((module.dual_prod_dual_equiv_dual R M N).symm.prod (linear_equiv.refl R (M × N))).trans (linear_equiv.prod_prod_prod_comm R (module.dual R M) (module.dual R N) M N)
def
quadratic_form.dual_prod_prod_isometry
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
(quadratic_form.dual_prod R (M × N)).isometry ((quadratic_form.dual_prod R M).prod (quadratic_form.dual_prod R N))
quadratic_form.dual_prod commutes (isometrically) with quadratic_form.prod.
Equations
- quadratic_form.dual_prod_prod_isometry = {to_linear_equiv := ((module.dual_prod_dual_equiv_dual R M N).symm.prod (linear_equiv.refl R (M × N))).trans (linear_equiv.prod_prod_prod_comm R (module.dual R M) (module.dual R N) M N), map_app' := _}
@[simp]
theorem
quadratic_form.to_dual_prod_apply
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
[invertible 2]
(i : M × M) :
⇑(Q.to_dual_prod) i = (⇑(⇑bilin_form.to_lin (⇑quadratic_form.associated Q)) i.fst + ⇑(⇑bilin_form.to_lin (⇑quadratic_form.associated Q)) i.snd, i.fst - i.snd)
def
quadratic_form.to_dual_prod
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
[invertible 2] :
M × M →ₗ[R] module.dual R M × M
The isometry sending (Q.prod $ -Q) to (quadratic_form.dual_prod 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
- Q.to_dual_prod = ((⇑bilin_form.to_lin (⇑quadratic_form.associated Q)).comp (linear_map.fst R M M) + (⇑bilin_form.to_lin (⇑quadratic_form.associated Q)).comp (linear_map.snd R M M)).prod (linear_map.fst R M M - linear_map.snd R M M)
theorem
quadratic_form.to_dual_prod_isometry
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
[invertible 2]
(Q : quadratic_form R M)
(x : M × M) :
⇑(quadratic_form.dual_prod R M) (⇑(Q.to_dual_prod) x) = ⇑(Q.prod (-Q)) x