Bilinear form #

This file defines various properties of bilinear forms, including reflexivity, symmetry, alternativity, adjoint, and non-degeneracy. For orthogonality, see Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean.

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:

M, M', ... are modules over the commutative semiring R,
M₁, M₁', ... are modules over the commutative ring R₁,
V, ... is a vector space over the field K.

References #

https://en.wikipedia.org/wiki/Bilinear_form

Tags #

Bilinear form,

Reflexivity, symmetry, and alternativity #

source

def LinearMap.BilinForm.IsRefl {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) :

Prop

The proposition that a bilinear form is reflexive

Equations

B.IsRefl = LinearMap.IsRefl B

Instances For

source

theorem LinearMap.BilinForm.IsRefl.eq_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (H : B.IsRefl) {x y : M} :

(B x) y = 0 → (B y) x = 0

source

theorem LinearMap.BilinForm.IsRefl.neg {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B : LinearMap.BilinForm R₁ M₁} (hB : B.IsRefl) :

(-B).IsRefl

source

theorem LinearMap.BilinForm.IsRefl.smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {α : Type u_8} [Semiring α] [Module α R] [SMulCommClass R α R] [NoZeroSMulDivisors α R] (a : α) {B : LinearMap.BilinForm R M} (hB : B.IsRefl) :

(a • B).IsRefl

source

theorem LinearMap.BilinForm.IsRefl.groupSMul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {α : Type u_8} [Group α] [DistribMulAction α R] [SMulCommClass R α R] (a : α) {B : LinearMap.BilinForm R M} (hB : B.IsRefl) :

(a • B).IsRefl

source

@[simp]

theorem LinearMap.BilinForm.isRefl_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

IsRefl 0

source

@[simp]

theorem LinearMap.BilinForm.isRefl_neg {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B : LinearMap.BilinForm R₁ M₁} :

(-B).IsRefl ↔ B.IsRefl

source

structure LinearMap.BilinForm.IsSymm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) :

Prop

The proposition that a bilinear form is symmetric

eq (x y : M) : (B x) y = (B y) x

Instances For

source

theorem LinearMap.BilinForm.isSymm_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} :

B.IsSymm ↔ ∀ (x y : M), (B x) y = (B y) x

source

theorem LinearMap.BilinForm.isSymm_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} :

B.IsSymm ↔ LinearMap.IsSymm B

source

theorem LinearMap.BilinForm.IsSymm.isRefl {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (H : B.IsSymm) :

B.IsRefl

source

theorem LinearMap.BilinForm.IsSymm.add {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B₁ B₂ : LinearMap.BilinForm R M} (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) :

(B₁ + B₂).IsSymm

source

theorem LinearMap.BilinForm.IsSymm.sub {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B₁ B₂ : LinearMap.BilinForm R₁ M₁} (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) :

(B₁ - B₂).IsSymm

source

theorem LinearMap.BilinForm.IsSymm.neg {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B : LinearMap.BilinForm R₁ M₁} (hB : B.IsSymm) :

(-B).IsSymm

source

theorem LinearMap.BilinForm.IsSymm.smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {α : Type u_8} [Monoid α] [DistribMulAction α R] [SMulCommClass R α R] (a : α) {B : LinearMap.BilinForm R M} (hB : B.IsSymm) :

(a • B).IsSymm

source

theorem LinearMap.BilinForm.IsSymm.restrict {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (b : B.IsSymm) (W : Submodule R M) :

(B.restrict W).IsSymm

The restriction of a symmetric bilinear form on a submodule is also symmetric.

source

@[simp]

theorem LinearMap.BilinForm.isSymm_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

IsSymm 0

source

@[simp]

theorem LinearMap.BilinForm.isSymm_neg {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B : LinearMap.BilinForm R₁ M₁} :

(-B).IsSymm ↔ B.IsSymm

source

theorem LinearMap.BilinForm.isSymm_iff_flip {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} :

B.IsSymm ↔ flipHom B = B

source

theorem LinearMap.BilinForm.IsSymm.polarization {M : Type u_2} [AddCommMonoid M] {R : Type u_8} [Field R] [NeZero 2] [Module R M] {B : LinearMap.BilinForm R M} (x y : M) (hB : B.IsSymm) :

(B x) y = ((B (x + y)) (x + y) - (B x) x - (B y) y) / 2

Polarization identity: a symmetric bilinear form can be expressed through the values it takes on the diagonal.

source

theorem LinearMap.BilinForm.ext_of_isSymm {M : Type u_2} [AddCommMonoid M] {R : Type u_8} [Field R] [NeZero 2] [Module R M] {B C : LinearMap.BilinForm R M} (hB : B.IsSymm) (hC : C.IsSymm) (h : ∀ (x : M), (B x) x = (C x) x) :

B = C

A symmetric bilinear form is characterized by the values it takes on the diagonal.

source

theorem LinearMap.BilinForm.ext_iff_of_isSymm {M : Type u_2} [AddCommMonoid M] {R : Type u_8} [Field R] [NeZero 2] [Module R M] {B C : LinearMap.BilinForm R M} (hB : B.IsSymm) (hC : C.IsSymm) :

B = C ↔ ∀ (x : M), (B x) x = (C x) x

A symmetric bilinear form is characterized by the values it takes on the diagonal.

source

theorem LinearMap.BilinForm.isSymm_iff_basis {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {ι : Type u_8} (b : Module.Basis ι R M) :

B.IsSymm ↔ ∀ (i j : ι), (B (b i)) (b j) = (B (b j)) (b i)

Positive semidefinite bilinear forms #

source

structure LinearMap.BilinForm.IsNonneg {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [LE R] (B : LinearMap.BilinForm R M) :

Prop

A bilinear form B is nonnegative if for any x we have 0 ≤ B x x.

nonneg (x : M) : 0 ≤ (B x) x

Instances For

source

theorem LinearMap.BilinForm.isNonneg_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [LE R] {B : LinearMap.BilinForm R M} :

B.IsNonneg ↔ ∀ (x : M), 0 ≤ (B x) x

source

theorem LinearMap.BilinForm.isNonneg_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [LE R] {B : LinearMap.BilinForm R M} :

B.IsNonneg ↔ LinearMap.IsNonneg B

A bilinear form is nonnegative if and only if it is nonnegative as a sesquilinear form.

source

@[simp]

theorem LinearMap.BilinForm.isNonneg_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [Preorder R] :

IsNonneg 0

source

theorem LinearMap.BilinForm.IsNonneg.add {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [Preorder R] [AddLeftMono R] {B C : LinearMap.BilinForm R M} (hB : B.IsNonneg) (hC : C.IsNonneg) :

(B + C).IsNonneg

source

theorem LinearMap.BilinForm.IsNonneg.smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [Preorder R] [PosMulMono R] {B : LinearMap.BilinForm R M} {c : R} (hB : B.IsNonneg) (hc : 0 ≤ c) :

(c • B).IsNonneg

source

structure LinearMap.BilinForm.IsPosSemidef {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [LE R] (B : LinearMap.BilinForm R M) extends B.IsSymm, B.IsNonneg :

Prop

A bilinear form B is positive semidefinite if it is symmetric and nonnegative.

eq (x y : M) : (B x) y = (B y) x
nonneg (x : M) : 0 ≤ (B x) x

Instances For

source

theorem LinearMap.BilinForm.isPosSemidef_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} [LE R] :

B.IsPosSemidef ↔ B.IsSymm ∧ B.IsNonneg

source

theorem LinearMap.BilinForm.isPosSemidef_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [LE R] {B : LinearMap.BilinForm R M} :

B.IsPosSemidef ↔ LinearMap.IsPosSemidef B

A bilinear form is positive semidefinite if and only if it is positive semidefinite as a sesquilinear form.

source

@[simp]

theorem LinearMap.BilinForm.isPosSemidef_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [Preorder R] :

IsPosSemidef 0

source

theorem LinearMap.BilinForm.IsPosSemidef.add {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [Preorder R] [AddLeftMono R] {B C : LinearMap.BilinForm R M} (hB : B.IsPosSemidef) (hC : C.IsPosSemidef) :

(B + C).IsPosSemidef

source

theorem LinearMap.BilinForm.IsPosSemidef.smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [Preorder R] [PosMulMono R] {B : LinearMap.BilinForm R M} {c : R} (hB : B.IsPosSemidef) (hc : 0 ≤ c) :

(c • B).IsPosSemidef

source

def LinearMap.BilinForm.IsAlt {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) :

Prop

The proposition that a bilinear form is alternating

Equations

B.IsAlt = LinearMap.IsAlt B

Instances For

source

theorem LinearMap.BilinForm.IsAlt.self_eq_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (H : B.IsAlt) (x : M) :

(B x) x = 0

source

theorem LinearMap.BilinForm.IsAlt.neg_eq {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B₁ : LinearMap.BilinForm R₁ M₁} (H : B₁.IsAlt) (x y : M₁) :

-(B₁ x) y = (B₁ y) x

source

theorem LinearMap.BilinForm.IsAlt.isRefl {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B₁ : LinearMap.BilinForm R₁ M₁} (H : B₁.IsAlt) :

B₁.IsRefl

source

theorem LinearMap.BilinForm.IsAlt.eq_of_add_add_eq_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} [IsCancelAdd R] {a b c : M} (H : B.IsAlt) (hAdd : a + b + c = 0) :

(B a) b = (B b) c

source

theorem LinearMap.BilinForm.IsAlt.add {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B₁ B₂ : LinearMap.BilinForm R M} (hB₁ : B₁.IsAlt) (hB₂ : B₂.IsAlt) :

(B₁ + B₂).IsAlt

source

theorem LinearMap.BilinForm.IsAlt.sub {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B₁ B₂ : LinearMap.BilinForm R₁ M₁} (hB₁ : B₁.IsAlt) (hB₂ : B₂.IsAlt) :

(B₁ - B₂).IsAlt

source

theorem LinearMap.BilinForm.IsAlt.neg {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B : LinearMap.BilinForm R₁ M₁} (hB : B.IsAlt) :

(-B).IsAlt

source

theorem LinearMap.BilinForm.IsAlt.smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {α : Type u_8} [Monoid α] [DistribMulAction α R] [SMulCommClass R α R] (a : α) {B : LinearMap.BilinForm R M} (hB : B.IsAlt) :

(a • B).IsAlt

source

@[simp]

theorem LinearMap.BilinForm.isAlt_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

IsAlt 0

source

@[simp]

theorem LinearMap.BilinForm.isAlt_neg {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B : LinearMap.BilinForm R₁ M₁} :

(-B).IsAlt ↔ B.IsAlt

source

def LinearMap.BilinForm.Nondegenerate {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) :

Prop

A nondegenerate bilinear form is a bilinear form such that the only element that is orthogonal to every other element is 0; i.e., for all nonzero m in M, there exists n in M with B m n ≠ 0.

Note that for general (neither symmetric nor antisymmetric) bilinear forms this definition has a chirality; in addition to this "left" nondegeneracy condition one could define a "right" nondegeneracy condition that in the situation described, B n m ≠ 0. This variant definition is not currently provided in mathlib. In finite dimension either definition implies the other.

Equations

B.Nondegenerate = ∀ (m : M), (∀ (n : M), (B m) n = 0) → m = 0

Instances For

source

theorem LinearMap.BilinForm.not_nondegenerate_zero (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] :

¬Nondegenerate 0

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

source

theorem LinearMap.BilinForm.Nondegenerate.ne_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] {B : LinearMap.BilinForm R M} (h : B.Nondegenerate) :

B ≠ 0

source

theorem LinearMap.BilinForm.Nondegenerate.congr {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {B : LinearMap.BilinForm R M} (e : M ≃ₗ[R] M') (h : B.Nondegenerate) :

((BilinForm.congr e) B).Nondegenerate

source

@[simp]

theorem LinearMap.BilinForm.nondegenerate_congr_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {B : LinearMap.BilinForm R M} (e : M ≃ₗ[R] M') :

((congr e) B).Nondegenerate ↔ B.Nondegenerate

source

theorem LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} :

B.Nondegenerate ↔ ker B = ⊥

A bilinear form is nondegenerate if and only if it has a trivial kernel.

source

theorem LinearMap.BilinForm.Nondegenerate.ker_eq_bot {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (h : B.Nondegenerate) :

ker B = ⊥

source

theorem LinearMap.BilinForm.compLeft_injective {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] (B : LinearMap.BilinForm R₁ M₁) (b : B.Nondegenerate) :

Function.Injective B.compLeft

source

theorem LinearMap.BilinForm.isAdjointPair_unique_of_nondegenerate {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] (B : LinearMap.BilinForm R₁ M₁) (b : B.Nondegenerate) (φ ψ₁ ψ₂ : M₁ →ₗ[R₁] M₁) (hψ₁ : IsAdjointPair B B ⇑ψ₁ ⇑φ) (hψ₂ : IsAdjointPair B B ⇑ψ₂ ⇑φ) :

ψ₁ = ψ₂

source

noncomputable def LinearMap.BilinForm.toDual {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (b : B.Nondegenerate) :

V ≃ₗ[K] Module.Dual K V

Given a nondegenerate bilinear form B on a finite-dimensional vector space, B.toDual is the linear equivalence between a vector space and its dual.

Equations

B.toDual b = LinearMap.linearEquivOfInjective B ⋯ ⋯

Instances For

source

theorem LinearMap.BilinForm.toDual_def {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} (b : SeparatingLeft B) {m n : V} :

((B.toDual b) m) n = (B m) n

source

@[simp]

theorem LinearMap.BilinForm.apply_toDual_symm_apply {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} {hB : B.Nondegenerate} (f : Module.Dual K V) (v : V) :

(B ((B.toDual hB).symm f)) v = f v

source

theorem LinearMap.BilinForm.Nondegenerate.flip {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} (hB : B.Nondegenerate) :

B.flip.Nondegenerate

source

theorem LinearMap.BilinForm.nonDegenerateFlip_iff {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} :

B.flip.Nondegenerate ↔ B.Nondegenerate

source

noncomputable def LinearMap.BilinForm.dualBasis {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] {ι : Type u_9} [DecidableEq ι] [Finite ι] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (b : Module.Basis ι K V) :

Module.Basis ι K V

The B-dual basis B.dualBasis hB b to a finite basis b satisfies B (B.dualBasis hB b i) (b j) = B (b i) (B.dualBasis hB b j) = if i = j then 1 else 0, where B is a nondegenerate (symmetric) bilinear form and b is a finite basis.

Equations

B.dualBasis hB b = b.dualBasis.map (B.toDual hB).symm

Instances For

source

@[simp]

theorem LinearMap.BilinForm.dualBasis_repr_apply {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] {ι : Type u_9} [DecidableEq ι] [Finite ι] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (b : Module.Basis ι K V) (x : V) (i : ι) :

((B.dualBasis hB b).repr x) i = (B x) (b i)

source

theorem LinearMap.BilinForm.apply_dualBasis_left {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] {ι : Type u_9} [DecidableEq ι] [Finite ι] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (b : Module.Basis ι K V) (i j : ι) :

(B ((B.dualBasis hB b) i)) (b j) = if j = i then 1 else 0

source

theorem LinearMap.BilinForm.apply_dualBasis_right {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] {ι : Type u_9} [DecidableEq ι] [Finite ι] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (sym : B.IsSymm) (b : Module.Basis ι K V) (i j : ι) :

(B (b i)) ((B.dualBasis hB b) j) = if i = j then 1 else 0

source

@[simp]

theorem LinearMap.BilinForm.dualBasis_dualBasis_flip {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) {ι : Type u_10} [Finite ι] [DecidableEq ι] (b : Module.Basis ι K V) :

B.dualBasis hB (B.flip.dualBasis ⋯ b) = b

source

@[simp]

theorem LinearMap.BilinForm.dualBasis_flip_dualBasis {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) {ι : Type u_10} [Finite ι] [DecidableEq ι] [FiniteDimensional K V] (b : Module.Basis ι K V) :

B.flip.dualBasis ⋯ (B.dualBasis hB b) = b

source

@[simp]

theorem LinearMap.BilinForm.dualBasis_dualBasis {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (hB' : B.IsSymm) {ι : Type u_10} [Finite ι] [DecidableEq ι] [FiniteDimensional K V] (b : Module.Basis ι K V) :

B.dualBasis hB (B.dualBasis hB b) = b

source

noncomputable def LinearMap.BilinForm.symmCompOfNondegenerate {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B₁ B₂ : LinearMap.BilinForm K V) (b₂ : B₂.Nondegenerate) :

V →ₗ[K] V

Given bilinear forms B₁, B₂ where B₂ is nondegenerate, symmCompOfNondegenerate is the linear map B₂ ∘ B₁.

Equations

B₁.symmCompOfNondegenerate B₂ b₂ = ↑(B₂.toDual b₂).symm ∘ₗ B₁

Instances For

source

theorem LinearMap.BilinForm.comp_symmCompOfNondegenerate_apply {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B₁ : LinearMap.BilinForm K V) {B₂ : LinearMap.BilinForm K V} (b₂ : B₂.Nondegenerate) (v : V) :

B₂ ((B₁.symmCompOfNondegenerate B₂ b₂) v) = B₁ v

source

@[simp]

theorem LinearMap.BilinForm.symmCompOfNondegenerate_left_apply {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B₁ : LinearMap.BilinForm K V) {B₂ : LinearMap.BilinForm K V} (b₂ : B₂.Nondegenerate) (v w : V) :

(B₂ ((B₁.symmCompOfNondegenerate B₂ b₂) w)) v = (B₁ w) v

source

noncomputable def LinearMap.BilinForm.leftAdjointOfNondegenerate {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (b : B.Nondegenerate) (φ : V →ₗ[K] V) :

V →ₗ[K] V

Given the nondegenerate bilinear form B and the linear map φ, leftAdjointOfNondegenerate provides the left adjoint of φ with respect to B. The lemma proving this property is BilinForm.isAdjointPairLeftAdjointOfNondegenerate.

Equations

B.leftAdjointOfNondegenerate b φ = (B.compRight φ).symmCompOfNondegenerate B b

Instances For

source

theorem LinearMap.BilinForm.isAdjointPairLeftAdjointOfNondegenerate {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (b : B.Nondegenerate) (φ : V →ₗ[K] V) :

IsAdjointPair B B ⇑(B.leftAdjointOfNondegenerate b φ) ⇑φ

source

theorem LinearMap.BilinForm.isAdjointPair_iff_eq_of_nondegenerate {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (b : B.Nondegenerate) (ψ φ : V →ₗ[K] V) :

IsAdjointPair B B ⇑ψ ⇑φ ↔ ψ = B.leftAdjointOfNondegenerate b φ

Given the nondegenerate bilinear form B, the linear map φ has a unique left adjoint given by BilinForm.leftAdjointOfNondegenerate.

PhysLean Documentation

Mathlib.LinearAlgebra.BilinearForm.Properties

Bilinear form #

Notation #

References #

Tags #

Reflexivity, symmetry, and alternativity #

Positive semidefinite bilinear forms #