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.

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:

• 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

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

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

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

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

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

@[simp]

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

@[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

def 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

Equations

• B.IsSymm = LinearMap.IsSymm B

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

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

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

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

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

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

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.

@[simp]

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

@[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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[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

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

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.

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

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

@[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

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.

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 = ⊥

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

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 ⇑ψ₂ ⇑φ) : ψ₁ = ψ₂

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 ⋯ ⋯

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

@[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

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

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

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

@[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)

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

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

@[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

@[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

@[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

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₁

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

@[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

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

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 φ) ⇑φ

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.