Bilinear form #

This file defines various properties of bilinear forms, including reflexivity, symmetry, alternativity, adjoint, and non-degeneracy. For orthogonality, see 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 #

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} [CommSemiring α] [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] :

LinearMap.BilinForm.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

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

Instances For

source

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

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] :

LinearMap.BilinForm.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 ↔ LinearMap.BilinForm.flipHom B = B

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] :

LinearMap.BilinForm.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] :

¬LinearMap.BilinForm.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) :

((LinearMap.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') :

((LinearMap.BilinForm.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 ↔ LinearMap.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) :

LinearMap.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ψ₁ : LinearMap.IsAdjointPair B B ⇑ψ₁ ⇑φ) (hψ₂ : LinearMap.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 : LinearMap.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 : Basis ι K V) :

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 : 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 : 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 : 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 : 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 : 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 : 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) :

LinearMap.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) :

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

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

Documentation

Mathlib.LinearAlgebra.BilinearForm.Properties

Bilinear form #

Notations #

References #

Tags #

Reflexivity, symmetry, and alternativity #