Documentation

Mathlib.LinearAlgebra.QuadraticForm.Isometry

Isometric linear maps #

Main definitions #

Notation #

Q₁ →qᵢ Q₂ is notation for Q₁.Isometry Q₂.

structure QuadraticMap.Isometry {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {N : Type u_8} [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 LinearMap :
Type (max u_4 u_5)

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

  • toFun : M₁M₂
  • map_add' : ∀ (x y : M₁), self.toFun (x + y) = self.toFun x + self.toFun y
  • map_smul' : ∀ (m : R) (x : M₁), self.toFun (m x) = (RingHom.id R) m self.toFun x
  • map_app' : ∀ (m : M₁), Q₂ (self.toFun m) = Q₁ m

    The quadratic form agrees across the map.

Instances For
    theorem QuadraticMap.Isometry.map_app' {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {N : Type u_8} [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₁ →qᵢ Q₂) (m : M₁) :
    Q₂ (self.toFun m) = Q₁ m

    The quadratic form agrees across the map.

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      instance QuadraticMap.Isometry.instFunLike {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {N : Type u_8} [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} :
      FunLike (Q₁ →qᵢ Q₂) M₁ M₂
      Equations
      • QuadraticMap.Isometry.instFunLike = { coe := fun (f : Q₁ →qᵢ Q₂) => f.toLinearMap, coe_injective' := }
      instance QuadraticMap.Isometry.instLinearMapClass {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {N : Type u_8} [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} :
      LinearMapClass (Q₁ →qᵢ Q₂) R M₁ M₂
      Equations
      • =
      theorem QuadraticMap.Isometry.toLinearMap_injective {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {N : Type u_8} [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} :
      Function.Injective QuadraticMap.Isometry.toLinearMap
      theorem QuadraticMap.Isometry.ext {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {N : Type u_8} [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₁ →qᵢ Q₂ ⦃g : Q₁ →qᵢ Q₂ (h : ∀ (x : M₁), f x = g x) :
      f = g
      def QuadraticMap.Isometry.Simps.apply {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {N : Type u_8} [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₁ →qᵢ Q₂) :
      M₁M₂

      See Note [custom simps projection].

      Equations
      Instances For
        @[simp]
        theorem QuadraticMap.Isometry.map_app {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {N : Type u_8} [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₁ →qᵢ Q₂) (m : M₁) :
        Q₂ (f m) = Q₁ m
        @[simp]
        theorem QuadraticMap.Isometry.coe_toLinearMap {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {N : Type u_8} [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₁ →qᵢ Q₂) :
        f.toLinearMap = f
        @[simp]
        theorem QuadraticMap.Isometry.id_apply {R : Type u_2} {M : Type u_3} {N : Type u_8} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (a : M) :
        def QuadraticMap.Isometry.id {R : Type u_2} {M : Type u_3} {N : Type u_8} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (Q : QuadraticMap R M N) :

        The identity isometry from a quadratic form to itself.

        Equations
        Instances For
          @[simp]
          theorem QuadraticMap.Isometry.ofEq_apply {R : Type u_2} {M₁ : Type u_4} {N : Type u_8} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid N] [Module R M₁] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₁ N} (h : Q₁ = Q₂) (a : M₁) :
          def QuadraticMap.Isometry.ofEq {R : Type u_2} {M₁ : Type u_4} {N : Type u_8} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid N] [Module R M₁] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₁ N} (h : Q₁ = Q₂) :
          Q₁ →qᵢ Q₂

          The identity isometry between equal quadratic forms.

          Equations
          Instances For
            @[simp]
            theorem QuadraticMap.Isometry.ofEq_rfl {R : Type u_2} {M₁ : Type u_4} {N : Type u_8} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid N] [Module R M₁] [Module R N] {Q : QuadraticMap R M₁ N} :
            @[simp]
            theorem QuadraticMap.Isometry.comp_apply {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} {N : Type u_8} [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} (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) (x : M₁) :
            (g.comp f) x = g (f x)
            def QuadraticMap.Isometry.comp {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} {N : Type u_8} [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} (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) :
            Q₁ →qᵢ Q₃

            The composition of two isometries between quadratic forms.

            Equations
            • g.comp f = let __spread.0 := g.toLinearMap ∘ₗ f.toLinearMap; { toFun := fun (x : M₁) => g (f x), map_add' := , map_smul' := , map_app' := }
            Instances For
              @[simp]
              theorem QuadraticMap.Isometry.toLinearMap_comp {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} {N : Type u_8} [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} (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) :
              (g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap
              @[simp]
              theorem QuadraticMap.Isometry.id_comp {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {N : Type u_8} [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₁ →qᵢ Q₂) :
              (QuadraticMap.Isometry.id Q₂).comp f = f
              @[simp]
              theorem QuadraticMap.Isometry.comp_id {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {N : Type u_8} [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₁ →qᵢ Q₂) :
              f.comp (QuadraticMap.Isometry.id Q₁) = f
              theorem QuadraticMap.Isometry.comp_assoc {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} {M₄ : Type u_7} {N : Type u_8} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [AddCommMonoid N] [Module R M₁] [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} {Q₄ : QuadraticMap R M₄ N} (h : Q₃ →qᵢ Q₄) (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) :
              (h.comp g).comp f = h.comp (g.comp f)
              instance QuadraticMap.Isometry.instZeroOfNat {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {N : Type u_8} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₂ : QuadraticMap R M₂ N} :
              Zero (0 →qᵢ Q₂)

              There is a zero map from any module with the zero form.

              Equations
              • QuadraticMap.Isometry.instZeroOfNat = { zero := let __src := 0; { toLinearMap := __src, map_app' := } }
              instance QuadraticMap.Isometry.hasZeroOfSubsingleton {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {N : Type u_8} [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} [Subsingleton M₁] :
              Zero (Q₁ →qᵢ Q₂)

              There is a zero map from the trivial module.

              Equations
              • QuadraticMap.Isometry.hasZeroOfSubsingleton = { zero := let __src := 0; { toLinearMap := __src, map_app' := } }
              instance QuadraticMap.Isometry.instSubsingleton {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {N : Type u_8} [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} [Subsingleton M₂] :
              Subsingleton (Q₁ →qᵢ Q₂)

              Maps into the zero module are trivial

              Equations
              • =