Documentation

Mathlib.LinearAlgebra.SesquilinearForm

Sesquilinear form #

This files provides properties about sesquilinear forms. The maps considered are of the form M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R, where I₁ : R₁ →+* R and I₂ : R₂ →+* R are ring homomorphisms and M₁ is a module over R₁ and M₂ is a module over R₂. Sesquilinear forms are the special case that M₁ = M₂, R₁ = R₂ = R, and I₁ = RingHom.id R. Taking additionally I₂ = RingHom.id R, then one obtains bilinear forms.

These forms are a special case of the bilinear maps defined in BilinearMap.lean and all basic lemmas about construction and elementary calculations are found there.

Main declarations #

References #

Tags #

Sesquilinear form,

Orthogonal vectors #

def LinearMap.IsOrtho {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R) (x : M₁) (y : M₂) :

The proposition that two elements of a sesquilinear form space are orthogonal

Equations
Instances For
    theorem LinearMap.isOrtho_def {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} {x : M₁} {y : M₂} :
    LinearMap.IsOrtho B x y ↑(B x) y = 0
    theorem LinearMap.isOrtho_zero_left {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R) (x : M₂) :
    theorem LinearMap.isOrtho_zero_right {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R) (x : M₁) :
    theorem LinearMap.isOrtho_flip {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₁' : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R} {x : M₁} {y : M₁} :
    def LinearMap.IsOrthoᵢ {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} {n : Type u_18} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₁' : R₁ →+* R} (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R) (v : nM₁) :

    A set of vectors v is orthogonal with respect to some bilinear form B if and only if for all i ≠ j, B (v i) (v j) = 0. For orthogonality between two elements, use BilinForm.isOrtho

    Equations
    Instances For
      theorem LinearMap.isOrthoᵢ_def {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} {n : Type u_18} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₁' : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R} {v : nM₁} :
      LinearMap.IsOrthoᵢ B v ∀ (i j : n), i j↑(B (v i)) (v j) = 0
      theorem LinearMap.isOrthoᵢ_flip {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} {n : Type u_18} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₁' : R₁ →+* R} (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R) {v : nM₁} :
      theorem LinearMap.ortho_smul_left {K : Type u_12} {K₁ : Type u_13} {K₂ : Type u_14} {V₁ : Type u_16} {V₂ : Type u_17} [Field K] [Field K₁] [AddCommGroup V₁] [Module K₁ V₁] [Field K₂] [AddCommGroup V₂] [Module K₂ V₂] {I₁ : K₁ →+* K} {I₂ : K₂ →+* K} {B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K} {x : V₁} {y : V₂} {a : K₁} (ha : a 0) :
      theorem LinearMap.ortho_smul_right {K : Type u_12} {K₁ : Type u_13} {K₂ : Type u_14} {V₁ : Type u_16} {V₂ : Type u_17} [Field K] [Field K₁] [AddCommGroup V₁] [Module K₁ V₁] [Field K₂] [AddCommGroup V₂] [Module K₂ V₂] {I₁ : K₁ →+* K} {I₂ : K₂ →+* K} {B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K} {x : V₁} {y : V₂} {a : K₂} {ha : a 0} :
      theorem LinearMap.linearIndependent_of_isOrthoᵢ {K : Type u_12} {K₁ : Type u_13} {V₁ : Type u_16} {n : Type u_18} [Field K] [Field K₁] [AddCommGroup V₁] [Module K₁ V₁] {I₁ : K₁ →+* K} {I₁' : K₁ →+* K} {B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] K} {v : nV₁} (hv₁ : LinearMap.IsOrthoᵢ B v) (hv₂ : ∀ (i : n), ¬LinearMap.IsOrtho B (v i) (v i)) :

      A set of orthogonal vectors v with respect to some sesquilinear form B is linearly independent if for all i, B (v i) (v i) ≠ 0.

      Reflexive bilinear forms #

      def LinearMap.IsRefl {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R) :

      The proposition that a sesquilinear form is reflexive

      Equations
      Instances For
        theorem LinearMap.IsRefl.eq_zero {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} (H : LinearMap.IsRefl B) {x : M₁} {y : M₁} :
        ↑(B x) y = 0↑(B y) x = 0
        theorem LinearMap.IsRefl.ortho_comm {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} (H : LinearMap.IsRefl B) {x : M₁} {y : M₁} :
        theorem LinearMap.IsRefl.domRestrict {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} (H : LinearMap.IsRefl B) (p : Submodule R₁ M₁) :
        @[simp]
        theorem LinearMap.IsRefl.flip_isRefl_iff {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} :
        theorem LinearMap.IsRefl.ker_flip_eq_bot {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} (H : LinearMap.IsRefl B) (h : LinearMap.ker B = ) :
        theorem LinearMap.IsRefl.ker_eq_bot_iff_ker_flip_eq_bot {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} (H : LinearMap.IsRefl B) :

        Symmetric bilinear forms #

        def LinearMap.IsSymm {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} (B : M →ₛₗ[I] M →ₗ[R] R) :

        The proposition that a sesquilinear form is symmetric

        Equations
        Instances For
          theorem LinearMap.IsSymm.eq {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} {B : M →ₛₗ[I] M →ₗ[R] R} (H : LinearMap.IsSymm B) (x : M) (y : M) :
          I (↑(B x) y) = ↑(B y) x
          theorem LinearMap.IsSymm.isRefl {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} {B : M →ₛₗ[I] M →ₗ[R] R} (H : LinearMap.IsSymm B) :
          theorem LinearMap.IsSymm.ortho_comm {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} {B : M →ₛₗ[I] M →ₗ[R] R} (H : LinearMap.IsSymm B) {x : M} {y : M} :

          Alternating bilinear forms #

          def LinearMap.IsAlt {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommRing R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R) :

          The proposition that a sesquilinear form is alternating

          Equations
          Instances For
            theorem LinearMap.IsAlt.self_eq_zero {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommRing R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} (H : LinearMap.IsAlt B) (x : M₁) :
            ↑(B x) x = 0
            theorem LinearMap.IsAlt.neg {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommRing R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} (H : LinearMap.IsAlt B) (x : M₁) (y : M₁) :
            -↑(B x) y = ↑(B y) x
            theorem LinearMap.IsAlt.isRefl {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommRing R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} (H : LinearMap.IsAlt B) :
            theorem LinearMap.IsAlt.ortho_comm {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommRing R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} (H : LinearMap.IsAlt B) {x : M₁} {y : M₁} :
            theorem LinearMap.isAlt_iff_eq_neg_flip {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommRing R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I : R₁ →+* R} [NoZeroDivisors R] [CharZero R] {B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R} :

            The orthogonal complement #

            def Submodule.orthogonalBilin {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommRing R] [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} (N : Submodule R₁ M₁) (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R) :
            Submodule R₁ M₁

            The orthogonal complement of a submodule N with respect to some bilinear form is the set of elements x which are orthogonal to all elements of N; i.e., for all y in N, B x y = 0.

            Note that for general (neither symmetric nor antisymmetric) bilinear forms this definition has a chirality; in addition to this "left" orthogonal complement one could define a "right" orthogonal complement for which, for all y in N, B y x = 0. This variant definition is not currently provided in mathlib.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem Submodule.mem_orthogonalBilin_iff {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommRing R] [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} {N : Submodule R₁ M₁} {m : M₁} :
              m Submodule.orthogonalBilin N B ∀ (n : M₁), n NLinearMap.IsOrtho B n m
              theorem Submodule.orthogonalBilin_le {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommRing R] [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} {N : Submodule R₁ M₁} {L : Submodule R₁ M₁} (h : N L) :
              theorem Submodule.le_orthogonalBilin_orthogonalBilin {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommRing R] [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} {N : Submodule R₁ M₁} (b : LinearMap.IsRefl B) :
              theorem LinearMap.span_singleton_inf_orthogonal_eq_bot {K : Type u_12} {K₁ : Type u_13} {V₁ : Type u_16} [Field K] [Field K₁] [AddCommGroup V₁] [Module K₁ V₁] {J₁ : K₁ →+* K} {J₁' : K₁ →+* K} (B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] K) (x : V₁) (hx : ¬LinearMap.IsOrtho B x x) :

              Given a bilinear form B and some x such that B x x ≠ 0, the span of the singleton of x is complement to its orthogonal complement.

              Adjoint pairs #

              def LinearMap.IsAdjointPair {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R M₁] {I : R →+* R} (B : M →ₗ[R] M →ₛₗ[I] R) (B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R) (f : M →ₗ[R] M₁) (g : M₁ →ₗ[R] M) :

              Given a pair of modules equipped with bilinear forms, this is the condition for a pair of maps between them to be mutually adjoint.

              Equations
              Instances For
                theorem LinearMap.isAdjointPair_iff_comp_eq_compl₂ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R M₁] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] R} {B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R} {f : M →ₗ[R] M₁} {g : M₁ →ₗ[R] M} :
                theorem LinearMap.isAdjointPair_zero {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R M₁] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] R} {B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R} :
                theorem LinearMap.isAdjointPair_id {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] R} :
                theorem LinearMap.IsAdjointPair.add {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R M₁] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] R} {B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R} {f : M →ₗ[R] M₁} {f' : M →ₗ[R] M₁} {g : M₁ →ₗ[R] M} {g' : M₁ →ₗ[R] M} (h : LinearMap.IsAdjointPair B B' f g) (h' : LinearMap.IsAdjointPair B B' f' g') :
                LinearMap.IsAdjointPair B B' (f + f') (g + g')
                theorem LinearMap.IsAdjointPair.comp {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] R} {B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R} {B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R} {f : M →ₗ[R] M₁} {g : M₁ →ₗ[R] M} {f' : M₁ →ₗ[R] M₂} {g' : M₂ →ₗ[R] M₁} (h : LinearMap.IsAdjointPair B B' f g) (h' : LinearMap.IsAdjointPair B' B'' f' g') :
                theorem LinearMap.IsAdjointPair.mul {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] R} {f : Module.End R M} {g : Module.End R M} {f' : Module.End R M} {g' : Module.End R M} (h : LinearMap.IsAdjointPair B B f g) (h' : LinearMap.IsAdjointPair B B f' g') :
                LinearMap.IsAdjointPair B B (f * f') (g' * g)
                theorem LinearMap.IsAdjointPair.sub {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] {B : M →ₗ[R] M →ₗ[R] R} {B' : M₁ →ₗ[R] M₁ →ₗ[R] R} {f : M →ₗ[R] M₁} {f' : M →ₗ[R] M₁} {g : M₁ →ₗ[R] M} {g' : M₁ →ₗ[R] M} (h : LinearMap.IsAdjointPair B B' f g) (h' : LinearMap.IsAdjointPair B B' f' g') :
                LinearMap.IsAdjointPair B B' (f - f') (g - g')
                theorem LinearMap.IsAdjointPair.smul {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] {B : M →ₗ[R] M →ₗ[R] R} {B' : M₁ →ₗ[R] M₁ →ₗ[R] R} {f : M →ₗ[R] M₁} {g : M₁ →ₗ[R] M} (c : R) (h : LinearMap.IsAdjointPair B B' f g) :

                Self-adjoint pairs #

                def LinearMap.IsPairSelfAdjoint {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} (B : M →ₗ[R] M →ₛₗ[I] R) (F : M →ₗ[R] M →ₛₗ[I] R) (f : Module.End R M) :

                The condition for an endomorphism to be "self-adjoint" with respect to a pair of bilinear forms on the underlying module. In the case that these two forms are identical, this is the usual concept of self adjointness. In the case that one of the forms is the negation of the other, this is the usual concept of skew adjointness.

                Equations
                Instances For
                  def LinearMap.IsSelfAdjoint {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} (B : M →ₗ[R] M →ₛₗ[I] R) (f : Module.End R M) :

                  An endomorphism of a module is self-adjoint with respect to a bilinear form if it serves as an adjoint for itself.

                  Equations
                  Instances For
                    def LinearMap.isPairSelfAdjointSubmodule {R : Type u_1} {M : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (F : M →ₗ[R] M →ₗ[R] R) :

                    The set of pair-self-adjoint endomorphisms are a submodule of the type of all endomorphisms.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def LinearMap.IsSkewAdjoint {R : Type u_1} {M : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (f : Module.End R M) :

                      An endomorphism of a module is skew-adjoint with respect to a bilinear form if its negation serves as an adjoint.

                      Equations
                      Instances For
                        def LinearMap.selfAdjointSubmodule {R : Type u_1} {M : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) :

                        The set of self-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact it is a Jordan subalgebra.)

                        Equations
                        Instances For
                          def LinearMap.skewAdjointSubmodule {R : Type u_1} {M : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) :

                          The set of skew-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact it is a Lie subalgebra.)

                          Equations
                          Instances For
                            theorem LinearMap.isPairSelfAdjoint_equiv {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] {B : M →ₗ[R] M →ₗ[R] R} {F : M →ₗ[R] M →ₗ[R] R} (e : M₁ ≃ₗ[R] M) (f : Module.End R M) :

                            Nondegenerate bilinear forms #

                            def LinearMap.SeparatingLeft {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R) :

                            A bilinear form is called left-separating if the only element that is left-orthogonal to every other element is 0; i.e., for every nonzero x in M₁, there exists y in M₂ with B x y ≠ 0.

                            Equations
                            Instances For
                              theorem LinearMap.not_separatingLeft_zero {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} (M₁ : Type u_6) (M₂ : Type u_7) [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] (I₁ : R₁ →+* R) (I₂ : R₂ →+* R) [Nontrivial M₁] :

                              In a non-trivial module, zero is not non-degenerate.

                              theorem LinearMap.SeparatingLeft.ne_zero {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} [Nontrivial M₁] {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} (h : LinearMap.SeparatingLeft B) :
                              B 0
                              theorem LinearMap.SeparatingLeft.congr {R : Type u_1} {Mₗ₁ : Type u_8} {Mₗ₁' : Type u_9} {Mₗ₂ : Type u_10} {Mₗ₂' : Type u_11} [CommSemiring R] [AddCommMonoid Mₗ₁] [AddCommMonoid Mₗ₂] [AddCommMonoid Mₗ₁'] [AddCommMonoid Mₗ₂'] [Module R Mₗ₁] [Module R Mₗ₂] [Module R Mₗ₁'] [Module R Mₗ₂'] {B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] R} (e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁') (e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂') (h : LinearMap.SeparatingLeft B) :
                              @[simp]
                              theorem LinearMap.separatingLeft_congr_iff {R : Type u_1} {Mₗ₁ : Type u_8} {Mₗ₁' : Type u_9} {Mₗ₂ : Type u_10} {Mₗ₂' : Type u_11} [CommSemiring R] [AddCommMonoid Mₗ₁] [AddCommMonoid Mₗ₂] [AddCommMonoid Mₗ₁'] [AddCommMonoid Mₗ₂'] [Module R Mₗ₁] [Module R Mₗ₂] [Module R Mₗ₁'] [Module R Mₗ₂'] {B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] R} (e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁') (e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂') :
                              def LinearMap.SeparatingRight {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R) :

                              A bilinear form is called right-separating if the only element that is right-orthogonal to every other element is 0; i.e., for every nonzero y in M₂, there exists x in M₁ with B x y ≠ 0.

                              Equations
                              Instances For
                                def LinearMap.Nondegenerate {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R) :

                                A bilinear form is called non-degenerate if it is left-separating and right-separating.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem LinearMap.flip_separatingRight {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} :
                                  @[simp]
                                  theorem LinearMap.flip_separatingLeft {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} :
                                  @[simp]
                                  theorem LinearMap.flip_nondegenerate {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} :
                                  theorem LinearMap.separatingLeft_iff_linear_nontrivial {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} :
                                  LinearMap.SeparatingLeft B ∀ (x : M₁), B x = 0x = 0
                                  theorem LinearMap.separatingRight_iff_linear_flip_nontrivial {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} :
                                  LinearMap.SeparatingRight B ∀ (y : M₂), ↑(LinearMap.flip B) y = 0y = 0
                                  theorem LinearMap.separatingLeft_iff_ker_eq_bot {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} :

                                  A bilinear form is left-separating if and only if it has a trivial kernel.

                                  theorem LinearMap.separatingRight_iff_flip_ker_eq_bot {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} :

                                  A bilinear form is right-separating if and only if its flip has a trivial kernel.

                                  The restriction of a reflexive bilinear form B onto a submodule W is nondegenerate if W has trivial intersection with its orthogonal complement, that is Disjoint W (W.orthogonalBilin B).

                                  theorem LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingLeft {R : Type u_1} {M : Type u_5} {n : Type u_18} [CommRing R] [AddCommGroup M] [Module R M] {I : R →+* R} {I' : R →+* R} [Nontrivial R] {B : M →ₛₗ[I] M →ₛₗ[I'] R} {v : Basis n R M} (h : LinearMap.IsOrthoᵢ B v) (hB : LinearMap.SeparatingLeft B) (i : n) :
                                  ¬LinearMap.IsOrtho B (v i) (v i)

                                  An orthogonal basis with respect to a left-separating bilinear form has no self-orthogonal elements.

                                  theorem LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingRight {R : Type u_1} {M : Type u_5} {n : Type u_18} [CommRing R] [AddCommGroup M] [Module R M] {I : R →+* R} {I' : R →+* R} [Nontrivial R] {B : M →ₛₗ[I] M →ₛₗ[I'] R} {v : Basis n R M} (h : LinearMap.IsOrthoᵢ B v) (hB : LinearMap.SeparatingRight B) (i : n) :
                                  ¬LinearMap.IsOrtho B (v i) (v i)

                                  An orthogonal basis with respect to a right-separating bilinear form has no self-orthogonal elements.

                                  theorem LinearMap.IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self {R : Type u_1} {M : Type u_5} {n : Type u_18} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroDivisors R] {B : M →ₗ[R] M →ₗ[R] R} (v : Basis n R M) (hO : LinearMap.IsOrthoᵢ B v) (h : ∀ (i : n), ¬LinearMap.IsOrtho B (v i) (v i)) :

                                  Given an orthogonal basis with respect to a bilinear form, the bilinear form is left-separating if the basis has no elements which are self-orthogonal.

                                  theorem LinearMap.IsOrthoᵢ.separatingRight_iff_not_isOrtho_basis_self {R : Type u_1} {M : Type u_5} {n : Type u_18} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroDivisors R] {B : M →ₗ[R] M →ₗ[R] R} (v : Basis n R M) (hO : LinearMap.IsOrthoᵢ B v) (h : ∀ (i : n), ¬LinearMap.IsOrtho B (v i) (v i)) :

                                  Given an orthogonal basis with respect to a bilinear form, the bilinear form is right-separating if the basis has no elements which are self-orthogonal.

                                  theorem LinearMap.IsOrthoᵢ.nondegenerate_of_not_isOrtho_basis_self {R : Type u_1} {M : Type u_5} {n : Type u_18} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroDivisors R] {B : M →ₗ[R] M →ₗ[R] R} (v : Basis n R M) (hO : LinearMap.IsOrthoᵢ B v) (h : ∀ (i : n), ¬LinearMap.IsOrtho B (v i) (v i)) :

                                  Given an orthogonal basis with respect to a bilinear form, the bilinear form is nondegenerate if the basis has no elements which are self-orthogonal.