English
There is a canonical isometry sending the quadratic form Q.prod(-Q) to the dualProd; this is a standard construction (σ) from a well-known reference, albeit with the pair order swapped.
Русский
Существует каноническая изометрия, переводящая квадратичную форму Q.prod(-Q) в dualProd; это стандартная конструкция (σ) из известного источника, хотя порядок пар поменян местами.
LaTeX
$$toDualProd (Q) : (Q.prod <| -Q) ≃ Isometry QuadraticForm.dualProd R M$$
Lean4
/-- 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.
-/
@[simps!]
def toDualProd (Q : QuadraticForm R M) [Invertible (2 : R)] : (Q.prod <| -Q) →qᵢ QuadraticForm.dualProd R M
where
toLinearMap :=
LinearMap.prod (Q.associated.comp (LinearMap.fst _ _ _) + Q.associated.comp (LinearMap.snd _ _ _))
(LinearMap.fst _ _ _ - LinearMap.snd _ _ _)
map_app'
x := by
dsimp only [associated, associatedHom]
dsimp only [LinearMap.smul_apply, LinearMap.coe_mk, AddHom.coe_mk, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
LinearMap.prod_apply, Pi.prod, LinearMap.add_apply, LinearMap.coe_comp, Function.comp_apply, LinearMap.fst_apply,
LinearMap.snd_apply, LinearMap.sub_apply, dualProd_apply, polarBilin_apply_apply, prod_apply, neg_apply]
simp only [polar_sub_right, polar_self, nsmul_eq_mul, Nat.cast_ofNat, polar_comm _ x.1 x.2, smul_sub,
Module.End.smul_def, sub_add_sub_cancel, ← sub_eq_add_neg (Q x.1) (Q x.2)]
rw [← LinearMap.map_sub (⅟2 : Module.End R R), ← mul_sub, ← Module.End.smul_def]
simp only [Module.End.smul_def, half_moduleEnd_apply_eq_half_smul, smul_eq_mul, invOf_mul_cancel_left']
