Documentation

Mathlib.LinearAlgebra.BilinearForm.Hom

Bilinear form and linear maps #

This file describes the relation between bilinear forms and linear maps.

TODO #

A lot of this file is now redundant following the replacement of the dedicated _root_.BilinForm structure with LinearMap.BilinForm, which is just an alias for M →ₗ[R] M →ₗ[R] R. For example LinearMap.BilinForm.toLinHom is now just the identity map. This redundant code should be removed.

Notations #

Given any term B of type BilinForm, due to a coercion, can use the notation B x y to refer to the function field, ie. B x y = B.bilin x y.

In this file we use the following type variables:

References #

Tags #

Bilinear form,

def LinearMap.BilinForm.toLinHomAux₁ {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (A : LinearMap.BilinForm R M) (x : M) :

Auxiliary definition to define toLinHom; see below.

Equations
  • A.toLinHomAux₁ x = A x
Instances For
    @[deprecated]

    Auxiliary definition to define toLinHom; see below.

    Equations
    • A.toLinHomAux₂ = A
    Instances For
      @[deprecated]

      The linear map obtained from a BilinForm by fixing the left co-ordinate and evaluating in the right.

      Equations
      • LinearMap.BilinForm.toLinHom = LinearMap.id
      Instances For
        @[deprecated]
        theorem LinearMap.BilinForm.toLin'_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (A : LinearMap.BilinForm R M) (x : M) :
        (LinearMap.BilinForm.toLinHom A) x = A x
        theorem LinearMap.BilinForm.sum_left {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) {α : Type u_7} (t : Finset α) (g : αM) (w : M) :
        (B (t.sum fun (i : α) => g i)) w = t.sum fun (i : α) => (B (g i)) w
        theorem LinearMap.BilinForm.sum_right {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) {α : Type u_7} (t : Finset α) (w : M) (g : αM) :
        (B w) (t.sum fun (i : α) => g i) = t.sum fun (i : α) => (B w) (g i)
        theorem LinearMap.BilinForm.sum_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {α : Type u_7} (t : Finset α) (B : αLinearMap.BilinForm R M) (v : M) (w : M) :
        ((t.sum fun (i : α) => B i) v) w = t.sum fun (i : α) => ((B i) v) w

        The linear map obtained from a BilinForm by fixing the right co-ordinate and evaluating in the left.

        Equations
        • LinearMap.BilinForm.toLinHomFlip = LinearMap.BilinForm.flipHom
        Instances For
          theorem LinearMap.BilinForm.toLin'Flip_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (A : LinearMap.BilinForm R M) (x : M) :
          ((LinearMap.BilinForm.toLinHomFlip A) x) = fun (y : M) => (A y) x
          def LinearMap.toBilinAux {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M →ₗ[R] R) :

          A map with two arguments that is linear in both is a bilinear form.

          This is an auxiliary definition for the full linear equivalence LinearMap.toBilin.

          Equations
          • f.toBilinAux = f
          Instances For
            @[deprecated]

            Bilinear forms are linearly equivalent to maps with two arguments that are linear in both.

            Equations
            • LinearMap.BilinForm.toLin = let __src := LinearMap.BilinForm.toLinHom; { toLinearMap := __src, invFun := LinearMap.toBilinAux, left_inv := , right_inv := }
            Instances For
              @[deprecated]

              A map with two arguments that is linear in both is linearly equivalent to bilinear form.

              Equations
              • LinearMap.toBilin = LinearMap.BilinForm.toLin.symm
              Instances For
                @[deprecated]
                theorem LinearMap.toBilinAux_eq {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M →ₗ[R] R) :
                f.toBilinAux = f
                @[deprecated]
                theorem LinearMap.toBilin_symm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
                LinearMap.toBilin.symm = LinearMap.BilinForm.toLin
                @[deprecated]
                theorem BilinForm.toLin_symm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
                LinearMap.BilinForm.toLin.symm = LinearMap.toBilin
                @[deprecated]
                theorem LinearMap.toBilin_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M →ₗ[R] R) (x : M) (y : M) :
                ((LinearMap.toBilin f) x) y = (f x) y
                @[deprecated]
                theorem BilinForm.toLin_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (x : M) :
                (LinearMap.BilinForm.toLin B) x = B x
                @[simp]
                theorem LinearMap.compBilinForm_apply_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {R' : Type u_7} [CommSemiring R'] [Algebra R' R] [Module R' M] [IsScalarTower R' R M] (f : R →ₗ[R'] R') (B : LinearMap.BilinForm R M) :
                ∀ (a m : M), ((f.compBilinForm B) a) m = f ((B a) m)
                def LinearMap.compBilinForm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {R' : Type u_7} [CommSemiring R'] [Algebra R' R] [Module R' M] [IsScalarTower R' R M] (f : R →ₗ[R'] R') (B : LinearMap.BilinForm R M) :

                Apply a linear map on the output of a bilinear form.

                Equations
                Instances For
                  def LinearMap.BilinForm.comp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type w} [AddCommMonoid M'] [Module R M'] (B : LinearMap.BilinForm R M') (l : M →ₗ[R] M') (r : M →ₗ[R] M') :

                  Apply a linear map on the left and right argument of a bilinear form.

                  Equations
                  Instances For

                    Apply a linear map to the left argument of a bilinear form.

                    Equations
                    • B.compLeft f = B.comp f LinearMap.id
                    Instances For

                      Apply a linear map to the right argument of a bilinear form.

                      Equations
                      • B.compRight f = B.comp LinearMap.id f
                      Instances For
                        theorem LinearMap.BilinForm.comp_comp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type w} [AddCommMonoid M'] [Module R M'] {M'' : Type u_7} [AddCommMonoid M''] [Module R M''] (B : LinearMap.BilinForm R M'') (l : M →ₗ[R] M') (r : M →ₗ[R] M') (l' : M' →ₗ[R] M'') (r' : M' →ₗ[R] M'') :
                        (B.comp l' r').comp l r = B.comp (l' ∘ₗ l) (r' ∘ₗ r)
                        @[simp]
                        theorem LinearMap.BilinForm.compLeft_compRight {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (l : M →ₗ[R] M) (r : M →ₗ[R] M) :
                        (B.compLeft l).compRight r = B.comp l r
                        @[simp]
                        theorem LinearMap.BilinForm.compRight_compLeft {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (l : M →ₗ[R] M) (r : M →ₗ[R] M) :
                        (B.compRight r).compLeft l = B.comp l r
                        @[simp]
                        theorem LinearMap.BilinForm.comp_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type w} [AddCommMonoid M'] [Module R M'] (B : LinearMap.BilinForm R M') (l : M →ₗ[R] M') (r : M →ₗ[R] M') (v : M) (w : M) :
                        ((B.comp l r) v) w = (B (l v)) (r w)
                        @[simp]
                        theorem LinearMap.BilinForm.compLeft_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (f : M →ₗ[R] M) (v : M) (w : M) :
                        ((B.compLeft f) v) w = (B (f v)) w
                        @[simp]
                        theorem LinearMap.BilinForm.compRight_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (f : M →ₗ[R] M) (v : M) (w : M) :
                        ((B.compRight f) v) w = (B v) (f w)
                        @[simp]
                        theorem LinearMap.BilinForm.comp_id_left {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (r : M →ₗ[R] M) :
                        B.comp LinearMap.id r = B.compRight r
                        @[simp]
                        theorem LinearMap.BilinForm.comp_id_right {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (l : M →ₗ[R] M) :
                        B.comp l LinearMap.id = B.compLeft l
                        @[simp]
                        theorem LinearMap.BilinForm.compLeft_id {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) :
                        B.compLeft LinearMap.id = B
                        @[simp]
                        theorem LinearMap.BilinForm.compRight_id {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) :
                        B.compRight LinearMap.id = B
                        @[simp]
                        theorem LinearMap.BilinForm.comp_id_id {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) :
                        B.comp LinearMap.id LinearMap.id = B
                        theorem LinearMap.BilinForm.comp_inj {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type w} [AddCommMonoid M'] [Module R M'] (B₁ : LinearMap.BilinForm R M') (B₂ : LinearMap.BilinForm R M') {l : M →ₗ[R] M'} {r : M →ₗ[R] M'} (hₗ : Function.Surjective l) (hᵣ : Function.Surjective r) :
                        B₁.comp l r = B₂.comp l r B₁ = B₂
                        def LinearMap.BilinForm.congr {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_7} [AddCommMonoid M'] [Module R M'] (e : M ≃ₗ[R] M') :

                        Apply a linear equivalence on the arguments of a bilinear form.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem LinearMap.BilinForm.congr_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_7} [AddCommMonoid M'] [Module R M'] (e : M ≃ₗ[R] M') (B : LinearMap.BilinForm R M) (x : M') (y : M') :
                          (((LinearMap.BilinForm.congr e) B) x) y = (B (e.symm x)) (e.symm y)
                          @[simp]
                          theorem LinearMap.BilinForm.congr_symm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_7} [AddCommMonoid M'] [Module R M'] (e : M ≃ₗ[R] M') :
                          theorem LinearMap.BilinForm.congr_trans {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_7} {M'' : Type u_8} [AddCommMonoid M'] [AddCommMonoid M''] [Module R M'] [Module R M''] (e : M ≃ₗ[R] M') (f : M' ≃ₗ[R] M'') :
                          theorem LinearMap.BilinForm.congr_congr {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_7} {M'' : Type u_8} [AddCommMonoid M'] [AddCommMonoid M''] [Module R M'] [Module R M''] (e : M' ≃ₗ[R] M'') (f : M ≃ₗ[R] M') (B : LinearMap.BilinForm R M) :
                          theorem LinearMap.BilinForm.congr_comp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_7} {M'' : Type u_8} [AddCommMonoid M'] [AddCommMonoid M''] [Module R M'] [Module R M''] (e : M ≃ₗ[R] M') (B : LinearMap.BilinForm R M) (l : M'' →ₗ[R] M') (r : M'' →ₗ[R] M') :
                          ((LinearMap.BilinForm.congr e) B).comp l r = B.comp (e.symm ∘ₗ l) (e.symm ∘ₗ r)
                          theorem LinearMap.BilinForm.comp_congr {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_7} {M'' : Type u_8} [AddCommMonoid M'] [AddCommMonoid M''] [Module R M'] [Module R M''] (e : M' ≃ₗ[R] M'') (B : LinearMap.BilinForm R M) (l : M' →ₗ[R] M) (r : M' →ₗ[R] M) :
                          (LinearMap.BilinForm.congr e) (B.comp l r) = B.comp (l ∘ₗ e.symm) (r ∘ₗ e.symm)
                          def LinearMap.BilinForm.linMulLin {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] R) (g : M →ₗ[R] R) :

                          linMulLin f g is the bilinear form mapping x and y to f x * g y

                          Equations
                          Instances For
                            @[simp]
                            theorem LinearMap.BilinForm.linMulLin_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {f : M →ₗ[R] R} {g : M →ₗ[R] R} (x : M) (y : M) :
                            ((LinearMap.BilinForm.linMulLin f g) x) y = f x * g y
                            @[simp]
                            theorem LinearMap.BilinForm.linMulLin_comp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_7} [AddCommMonoid M'] [Module R M'] {f : M →ₗ[R] R} {g : M →ₗ[R] R} (l : M' →ₗ[R] M) (r : M' →ₗ[R] M) :
                            (LinearMap.BilinForm.linMulLin f g).comp l r = LinearMap.BilinForm.linMulLin (f ∘ₗ l) (g ∘ₗ r)
                            @[simp]
                            theorem LinearMap.BilinForm.linMulLin_compLeft {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {f : M →ₗ[R] R} {g : M →ₗ[R] R} (l : M →ₗ[R] M) :
                            @[simp]
                            theorem LinearMap.BilinForm.linMulLin_compRight {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {f : M →ₗ[R] R} {g : M →ₗ[R] R} (r : M →ₗ[R] M) :
                            theorem LinearMap.BilinForm.ext_basis {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {F₂ : LinearMap.BilinForm R M} {ι : Type u_9} (b : Basis ι R M) (h : ∀ (i j : ι), (B (b i)) (b j) = (F₂ (b i)) (b j)) :
                            B = F₂

                            Two bilinear forms are equal when they are equal on all basis vectors.

                            theorem LinearMap.BilinForm.sum_repr_mul_repr_mul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {ι : Type u_9} (b : Basis ι R M) (x : M) (y : M) :
                            ((b.repr x).sum fun (i : ι) (xi : R) => (b.repr y).sum fun (j : ι) (yj : R) => xi yj (B (b i)) (b j)) = (B x) y

                            Write out B x y as a sum over B (b i) (b j) if b is a basis.