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.

Notation #

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

In this file we use the following type variables:

References #

Tags #

Bilinear form,

source
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) :
M →ₗ[R] R

Auxiliary definition to define toLinHom; see below.

Equations
Instances For
    source
    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 (∑ i ∈ t, g i)) w = ∑ i ∈ t, (B (g i)) w
    source
    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) (∑ i ∈ t, g i) = ∑ i ∈ t, (B w) (g i)
    source
    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 w : M) :
    ((∑ i ∈ t, B i) v) w = ∑ i ∈ t, ((B i) v) w
    source
    def LinearMap.BilinForm.toLinHomFlip {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
    LinearMap.BilinForm R M →ₗ[R] M →ₗ[R] M →ₗ[R] R

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

    Equations
    Instances For
      source
      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) :
      ⇑((toLinHomFlip A) x) = fun (y : M) => (A y) x
      source
      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) :
      LinearMap.BilinForm R' M

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

      Equations
      Instances For
        source
        @[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) (x a✝ : M) :
        ((f.compBilinForm B) x) a✝ = f ((B x) a✝)
        source
        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 r : M →ₗ[R] M') :
        LinearMap.BilinForm R M

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

        Equations
        Instances For
          source
          def LinearMap.BilinForm.compLeft {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (f : M →ₗ[R] M) :
          LinearMap.BilinForm R M

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

          Equations
          Instances For
            source
            def LinearMap.BilinForm.compRight {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (f : M →ₗ[R] M) :
            LinearMap.BilinForm R M

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

            Equations
            Instances For
              source
              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 r : M →ₗ[R] M') (l' r' : M' →ₗ[R] M'') :
              (B.comp l' r').comp l r = B.comp (l' ∘ₗ l) (r' ∘ₗ r)
              source
              @[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 r : M →ₗ[R] M) :
              (B.compLeft l).compRight r = B.comp l r
              source
              @[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 r : M →ₗ[R] M) :
              (B.compRight r).compLeft l = B.comp l r
              source
              @[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 r : M →ₗ[R] M') (v w : M) :
              ((B.comp l r) v) w = (B (l v)) (r w)
              source
              @[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 w : M) :
              ((B.compLeft f) v) w = (B (f v)) w
              source
              @[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 w : M) :
              ((B.compRight f) v) w = (B v) (f w)
              source
              @[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 id r = B.compRight r
              source
              @[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 id = B.compLeft l
              source
              @[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 id = B
              source
              @[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 id = B
              source
              @[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 id id = B
              source
              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₁ B₂ : LinearMap.BilinForm R M') {l r : M →ₗ[R] M'} (hₗ : Function.Surjective ⇑l) (hᵣ : Function.Surjective ⇑r) :
              B₁.comp l r = B₂.comp l r ↔ B₁ = B₂
              source
              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') :
              LinearMap.BilinForm R M ≃ₗ[R] LinearMap.BilinForm R M'

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

              Equations
              Instances For
                source
                @[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 y : M') :
                (((congr e) B) x) y = (B (e.symm x)) (e.symm y)
                source
                @[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') :
                (congr e).symm = congr e.symm
                source
                @[simp]
                theorem LinearMap.BilinForm.congr_refl {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
                congr (LinearEquiv.refl R M) = LinearEquiv.refl R (LinearMap.BilinForm R M)
                source
                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'') :
                congr e ≪≫ₗ congr f = congr (e ≪≫ₗ f)
                source
                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) :
                (congr e) ((congr f) B) = (congr (f ≪≫ₗ e)) B
                source
                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 r : M'' →ₗ[R] M') :
                ((congr e) B).comp l r = B.comp (↑e.symm ∘ₗ l) (↑e.symm ∘ₗ r)
                source
                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 r : M' →ₗ[R] M) :
                (congr e) (B.comp l r) = B.comp (l ∘ₗ ↑e.symm) (r ∘ₗ ↑e.symm)
                source
                def LinearEquiv.congrRight₂ {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N₁ : Type u_9} {N₂ : Type u_10} [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁] [Module R N₂] (e : N₁ ≃ₗ[R] N₂) :
                LinearMap.BilinMap R M N₁ ≃ₗ[R] LinearMap.BilinMap R M N₂

                When N₁ and N₂ are equivalent, bilinear maps on M into N₁ are equivalent to bilinear maps into N₂.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem LinearEquiv.congrRight₂_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N₁ : Type u_9} {N₂ : Type u_10} [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁] [Module R N₂] (e : N₁ ≃ₗ[R] N₂) (B : LinearMap.BilinMap R M N₁) :
                  e.congrRight₂ B = LinearMap.compr₂ B ↑e
                  source
                  @[simp]
                  theorem LinearEquiv.congrRight₂_refl {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N₁ : Type u_9} [AddCommMonoid N₁] [Module R N₁] :
                  (refl R N₁).congrRight₂ = refl R (LinearMap.BilinMap R M N₁)
                  source
                  @[simp]
                  theorem LinearEquiv.congrRight_symm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N₁ : Type u_9} {N₂ : Type u_10} [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁] [Module R N₂] (e : N₁ ≃ₗ[R] N₂) :
                  e.congrRight₂.symm = e.symm.congrRight₂
                  source
                  theorem LinearEquiv.congrRight₂_trans {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N₁ : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R N₁] [Module R N₂] [Module R N₃] (e₁₂ : N₁ ≃ₗ[R] N₂) (e₂₃ : N₂ ≃ₗ[R] N₃) :
                  (e₁₂ ≪≫ₗ e₂₃).congrRight₂ = e₁₂.congrRight₂ ≪≫ₗ e₂₃.congrRight₂
                  source
                  def LinearMap.BilinForm.linMulLin {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (f g : M →ₗ[R] R) :
                  LinearMap.BilinForm R M

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

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem LinearMap.BilinForm.linMulLin_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {f g : M →ₗ[R] R} (x y : M) :
                    ((linMulLin f g) x) y = f x * g y
                    source
                    @[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 g : M →ₗ[R] R} (l r : M' →ₗ[R] M) :
                    (linMulLin f g).comp l r = linMulLin (f ∘ₗ l) (g ∘ₗ r)
                    source
                    @[simp]
                    theorem LinearMap.BilinForm.linMulLin_compLeft {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {f g : M →ₗ[R] R} (l : M →ₗ[R] M) :
                    (linMulLin f g).compLeft l = linMulLin (f ∘ₗ l) g
                    source
                    @[simp]
                    theorem LinearMap.BilinForm.linMulLin_compRight {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {f g : M →ₗ[R] R} (r : M →ₗ[R] M) :
                    (linMulLin f g).compRight r = linMulLin f (g ∘ₗ r)
                    source
                    theorem LinearMap.BilinForm.ext_basis {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B F₂ : LinearMap.BilinForm R M} {ι : Type u_9} (b : Module.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.

                    source
                    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 : Module.Basis ι R M) (x 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.