Documentation

Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Isometric equivalences with respect to quadratic forms #

Main definitions #

Main results #

structure QuadraticMap.IsometryEquiv {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] (Q₁ : QuadraticMap R M₁ N) (Q₂ : QuadraticMap R M₂ N) extends LinearEquiv :
Type (max u_5 u_6)

An isometric equivalence between two quadratic spaces M₁, Q₁ and M₂, Q₂ over a ring R, is a linear equivalence between M₁ and M₂ that commutes with the quadratic forms.

  • toFun : M₁M₂
  • map_add' : ∀ (x y : M₁), (self.toLinearEquiv).toFun (x + y) = (self.toLinearEquiv).toFun x + (self.toLinearEquiv).toFun y
  • map_smul' : ∀ (m : R) (x : M₁), (self.toLinearEquiv).toFun (m x) = (RingHom.id R) m (self.toLinearEquiv).toFun x
  • invFun : M₂M₁
  • left_inv : Function.LeftInverse self.invFun (self.toLinearEquiv).toFun
  • right_inv : Function.RightInverse self.invFun (self.toLinearEquiv).toFun
  • map_app' : ∀ (m : M₁), Q₂ ((self.toLinearEquiv).toFun m) = Q₁ m
Instances For
    theorem QuadraticMap.IsometryEquiv.map_app' {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (self : Q₁.IsometryEquiv Q₂) (m : M₁) :
    Q₂ ((self.toLinearEquiv).toFun m) = Q₁ m
    def QuadraticMap.Equivalent {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] (Q₁ : QuadraticMap R M₁ N) (Q₂ : QuadraticMap R M₂ N) :

    Two quadratic forms over a ring R are equivalent if there exists an isometric equivalence between them: a linear equivalence that transforms one quadratic form into the other.

    Equations
    • Q₁.Equivalent Q₂ = Nonempty (Q₁.IsometryEquiv Q₂)
    Instances For
      instance QuadraticMap.IsometryEquiv.instEquivLike {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} :
      EquivLike (Q₁.IsometryEquiv Q₂) M₁ M₂
      Equations
      • One or more equations did not get rendered due to their size.
      instance QuadraticMap.IsometryEquiv.instLinearEquivClass {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} :
      LinearEquivClass (Q₁.IsometryEquiv Q₂) R M₁ M₂
      Equations
      • =
      instance QuadraticMap.IsometryEquiv.instCoeOutLinearEquivId {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} :
      CoeOut (Q₁.IsometryEquiv Q₂) (M₁ ≃ₗ[R] M₂)
      Equations
      • QuadraticMap.IsometryEquiv.instCoeOutLinearEquivId = { coe := QuadraticMap.IsometryEquiv.toLinearEquiv }
      @[simp]
      theorem QuadraticMap.IsometryEquiv.coe_toLinearEquiv {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁.IsometryEquiv Q₂) :
      f.toLinearEquiv = f
      @[simp]
      theorem QuadraticMap.IsometryEquiv.map_app {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁.IsometryEquiv Q₂) (m : M₁) :
      Q₂ (f m) = Q₁ m
      def QuadraticMap.IsometryEquiv.refl {R : Type u_2} {M : Type u_4} {N : Type u_9} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (Q : QuadraticMap R M N) :
      Q.IsometryEquiv Q

      The identity isometric equivalence between a quadratic form and itself.

      Equations
      Instances For
        def QuadraticMap.IsometryEquiv.symm {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁.IsometryEquiv Q₂) :
        Q₂.IsometryEquiv Q₁

        The inverse isometric equivalence of an isometric equivalence between two quadratic forms.

        Equations
        • f.symm = let __src := f.symm; { toLinearEquiv := __src, map_app' := }
        Instances For
          def QuadraticMap.IsometryEquiv.trans {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R M₃] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} {Q₃ : QuadraticMap R M₃ N} (f : Q₁.IsometryEquiv Q₂) (g : Q₂.IsometryEquiv Q₃) :
          Q₁.IsometryEquiv Q₃

          The composition of two isometric equivalences between quadratic forms.

          Equations
          • f.trans g = let __src := f.trans g.toLinearEquiv; { toLinearEquiv := __src, map_app' := }
          Instances For
            @[simp]
            theorem QuadraticMap.IsometryEquiv.toIsometry_apply {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (g : Q₁.IsometryEquiv Q₂) (x : M₁) :
            g.toIsometry x = g x
            def QuadraticMap.IsometryEquiv.toIsometry {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (g : Q₁.IsometryEquiv Q₂) :
            Q₁ →qᵢ Q₂

            Isometric equivalences are isometric maps

            Equations
            • g.toIsometry = let __spread.0 := g; { toFun := fun (x : M₁) => g x, map_add' := , map_smul' := , map_app' := }
            Instances For
              theorem QuadraticMap.Equivalent.refl {R : Type u_2} {M : Type u_4} {N : Type u_9} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (Q : QuadraticMap R M N) :
              Q.Equivalent Q
              theorem QuadraticMap.Equivalent.symm {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (h : Q₁.Equivalent Q₂) :
              Q₂.Equivalent Q₁
              theorem QuadraticMap.Equivalent.trans {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N : Type u_9} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R M₃] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} {Q₃ : QuadraticMap R M₃ N} (h : Q₁.Equivalent Q₂) (h' : Q₂.Equivalent Q₃) :
              Q₁.Equivalent Q₃
              def QuadraticMap.isometryEquivOfCompLinearEquiv {R : Type u_2} {M : Type u_4} {M₁ : Type u_5} {N : Type u_9} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid N] [Module R M] [Module R M₁] [Module R N] (Q : QuadraticMap R M N) (f : M₁ ≃ₗ[R] M) :
              Q.IsometryEquiv (Q.comp f)

              A quadratic form composed with a LinearEquiv is isometric to itself.

              Equations
              • Q.isometryEquivOfCompLinearEquiv f = let __src := f.symm; { toLinearEquiv := __src, map_app' := }
              Instances For
                noncomputable def QuadraticMap.isometryEquivBasisRepr {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_9} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Finite ι] (Q : QuadraticMap R M N) (v : Basis ι R M) :
                Q.IsometryEquiv (Q.basisRepr v)

                A quadratic form is isometrically equivalent to its bases representations.

                Equations
                • Q.isometryEquivBasisRepr v = Q.isometryEquivOfCompLinearEquiv v.equivFun.symm
                Instances For
                  noncomputable def QuadraticForm.isometryEquivWeightedSumSquares {K : Type u_3} {V : Type u_8} [Field K] [Invertible 2] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (v : Basis (Fin (FiniteDimensional.finrank K V)) K V) (hv₁ : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) v) :

                  Given an orthogonal basis, a quadratic form is isometrically equivalent with a weighted sum of squares.

                  Equations
                  Instances For