Documentation

Mathlib.LinearAlgebra.QuadraticForm.Dual

Quadratic form structures related to Module.Dual #

Main definitions #

@[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

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
    @[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

    The quadratic form on Module.Dual R M × M defined as Q (f, x) = f x.

    Equations
    Instances For
      @[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

      Any module isomorphism induces a quadratic isomorphism between the corresponding dual_prod.

      Equations
      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)

        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) :
          Q.toDualProd i = ((QuadraticMap.associated Q) i.1 + (QuadraticMap.associated Q) i.2, i.1 - i.2)

          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