Documentation

Mathlib.LinearAlgebra.QuadraticForm.Isometry

Isometric linear maps #

Main definitions #

Notation #

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

structure QuadraticForm.Isometry {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) 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.

Instances For

    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.

    Instances For
      instance QuadraticForm.Isometry.instLinearMapClass {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} :
      LinearMapClass (Q₁ →qᵢ Q₂) R M₁ M₂
      theorem QuadraticForm.Isometry.toLinearMap_injective {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} :
      Function.Injective QuadraticForm.Isometry.toLinearMap
      theorem QuadraticForm.Isometry.ext {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} ⦃f : Q₁ →qᵢ Q₂ ⦃g : Q₁ →qᵢ Q₂ (h : ∀ (x : M₁), f x = g x) :
      f = g
      def QuadraticForm.Isometry.Simps.apply {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) :
      M₁M₂

      See Note [custom simps projection].

      Instances For
        @[simp]
        theorem QuadraticForm.Isometry.map_app {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) (m : M₁) :
        Q₂ (f m) = Q₁ m
        @[simp]
        theorem QuadraticForm.Isometry.coe_toLinearMap {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) :
        f.toLinearMap = f
        @[simp]
        theorem QuadraticForm.Isometry.id_apply {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) :
        ∀ (a : M), ↑(QuadraticForm.Isometry.id Q) a = a
        def QuadraticForm.Isometry.id {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) :

        The identity isometry from a quadratic form to itself.

        Instances For
          @[simp]
          theorem QuadraticForm.Isometry.comp_apply {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) (x : M₁) :
          ↑(QuadraticForm.Isometry.comp g f) x = g (f x)
          def QuadraticForm.Isometry.comp {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) :
          Q₁ →qᵢ Q₃

          The composition of two isometries between quadratic forms.

          Instances For
            @[simp]
            theorem QuadraticForm.Isometry.toLinearMap_comp {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) :
            (QuadraticForm.Isometry.comp g f).toLinearMap = LinearMap.comp g.toLinearMap f.toLinearMap
            @[simp]
            theorem QuadraticForm.Isometry.id_comp {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) :
            @[simp]
            theorem QuadraticForm.Isometry.comp_id {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) :
            theorem QuadraticForm.Isometry.comp_assoc {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} {M₄ : Type u_7} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} {Q₄ : QuadraticForm R M₄} (h : Q₃ →qᵢ Q₄) (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) :
            instance QuadraticForm.Isometry.instZeroIsometryOfNatQuadraticFormToOfNat0InstZeroQuadraticForm {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₂ : QuadraticForm R M₂} :
            Zero (0 →qᵢ Q₂)

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

            instance QuadraticForm.Isometry.hasZeroOfSubsingleton {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} [Subsingleton M₁] :
            Zero (Q₁ →qᵢ Q₂)

            There is a zero map from the trivial module.

            instance QuadraticForm.Isometry.instSubsingletonIsometry {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} [Subsingleton M₂] :
            Subsingleton (Q₁ →qᵢ Q₂)

            Maps into the zero module are trivial