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 semiring R,
• M₁, M₁', ... are modules over the ring R₁,
• 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

Tags

Bilinear form,

Reflexivity, symmetry, and alternativity

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

The proposition that a bilinear form is reflexive

Equations

• BilinForm.IsRefl B = ∀ (x y : M), B.bilin x y = 0 → B.bilin y x = 0

theorem BilinForm.IsRefl.eq_zero {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {B : BilinForm R M} (H : BilinForm.IsRefl B) {x : M} {y : M} : B.bilin x y = 0 → B.bilin y x = 0

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

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

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

@[simp]

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

@[simp]

theorem BilinForm.isRefl_neg {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁] {B : BilinForm R₁ M₁} : BilinForm.IsRefl (-B) ↔ BilinForm.IsRefl B

def BilinForm.IsSymm {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) : Prop

The proposition that a bilinear form is symmetric

Equations

• BilinForm.IsSymm B = ∀ (x y : M), B.bilin x y = B.bilin y x

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

theorem BilinForm.isSymm_neg {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁] {B : BilinForm R₁ M₁} : BilinForm.IsSymm (-B) ↔ BilinForm.IsSymm B

theorem BilinForm.isSymm_iff_flip {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (R₂ : Type u_5) [CommSemiring R₂] {B : BilinForm R M} [Algebra R₂ R] : BilinForm.IsSymm B ↔ (BilinForm.flipHom R₂) B = B

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

The proposition that a bilinear form is alternating

Equations

• BilinForm.IsAlt B = ∀ (x : M), B.bilin x x = 0

theorem BilinForm.IsAlt.self_eq_zero {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {B : BilinForm R M} (H : BilinForm.IsAlt B) (x : M) : B.bilin x x = 0

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

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

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

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

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

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

@[simp]

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

@[simp]

theorem BilinForm.isAlt_neg {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁] {B : BilinForm R₁ M₁} : BilinForm.IsAlt (-B) ↔ BilinForm.IsAlt B

Linear adjoints

def BilinForm.IsAdjointPair {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) {M' : Type u_13} [AddCommMonoid M'] [Module R M'] (B' : BilinForm R M') (f : M →ₗ[R] M') (g : M' →ₗ[R] M) : Prop

Given a pair of modules equipped with bilinear forms, this is the condition for a pair of maps between them to be mutually adjoint.

Equations

• BilinForm.IsAdjointPair B B' f g = ∀ ⦃x : M⦄ ⦃y : M'⦄, B'.bilin (f x) y = B.bilin x (g y)

theorem BilinForm.IsAdjointPair.eq {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {B : BilinForm R M} {M' : Type u_13} [AddCommMonoid M'] [Module R M'] {B' : BilinForm R M'} {f : M →ₗ[R] M'} {g : M' →ₗ[R] M} (h : BilinForm.IsAdjointPair B B' f g) {x : M} {y : M'} : B'.bilin (f x) y = B.bilin x (g y)

theorem BilinForm.isAdjointPair_iff_compLeft_eq_compRight {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {B : BilinForm R M} (F : BilinForm R M) (f : Module.End R M) (g : Module.End R M) : BilinForm.IsAdjointPair B F f g ↔ BilinForm.compLeft F f = BilinForm.compRight B g

theorem BilinForm.isAdjointPair_zero {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {B : BilinForm R M} {M' : Type u_13} [AddCommMonoid M'] [Module R M'] {B' : BilinForm R M'} : BilinForm.IsAdjointPair B B' 0 0

theorem BilinForm.isAdjointPair_id {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {B : BilinForm R M} : BilinForm.IsAdjointPair B B 1 1

theorem BilinForm.IsAdjointPair.add {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {B : BilinForm R M} {M' : Type u_13} [AddCommMonoid M'] [Module R M'] {B' : BilinForm R M'} {f : M →ₗ[R] M'} {f' : M →ₗ[R] M'} {g : M' →ₗ[R] M} {g' : M' →ₗ[R] M} (h : BilinForm.IsAdjointPair B B' f g) (h' : BilinForm.IsAdjointPair B B' f' g') : BilinForm.IsAdjointPair B B' (f + f') (g + g')

theorem BilinForm.IsAdjointPair.sub {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁] {B₁ : BilinForm R₁ M₁} {M₁' : Type u_14} [AddCommGroup M₁'] [Module R₁ M₁'] {B₁' : BilinForm R₁ M₁'} {f₁ : M₁ →ₗ[R₁] M₁'} {f₁' : M₁ →ₗ[R₁] M₁'} {g₁ : M₁' →ₗ[R₁] M₁} {g₁' : M₁' →ₗ[R₁] M₁} (h : BilinForm.IsAdjointPair B₁ B₁' f₁ g₁) (h' : BilinForm.IsAdjointPair B₁ B₁' f₁' g₁') : BilinForm.IsAdjointPair B₁ B₁' (f₁ - f₁') (g₁ - g₁')

theorem BilinForm.IsAdjointPair.smul {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {M₂' : Type u_11} [AddCommMonoid M₂'] [Module R₂ M₂'] {B₂ : BilinForm R₂ M₂} {B₂' : BilinForm R₂ M₂'} {f₂ : M₂ →ₗ[R₂] M₂'} {g₂ : M₂' →ₗ[R₂] M₂} (c : R₂) (h : BilinForm.IsAdjointPair B₂ B₂' f₂ g₂) : BilinForm.IsAdjointPair B₂ B₂' (c • f₂) (c • g₂)

theorem BilinForm.IsAdjointPair.comp {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {B : BilinForm R M} {M' : Type u_13} [AddCommMonoid M'] [Module R M'] {B' : BilinForm R M'} {f : M →ₗ[R] M'} {g : M' →ₗ[R] M} {M'' : Type u_15} [AddCommMonoid M''] [Module R M''] (B'' : BilinForm R M'') {f' : M' →ₗ[R] M''} {g' : M'' →ₗ[R] M'} (h : BilinForm.IsAdjointPair B B' f g) (h' : BilinForm.IsAdjointPair B' B'' f' g') : BilinForm.IsAdjointPair B B'' (f' ∘ₗ f) (g ∘ₗ g')

theorem BilinForm.IsAdjointPair.mul {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {B : BilinForm R M} {f : Module.End R M} {g : Module.End R M} {f' : Module.End R M} {g' : Module.End R M} (h : BilinForm.IsAdjointPair B B f g) (h' : BilinForm.IsAdjointPair B B f' g') : BilinForm.IsAdjointPair B B (f * f') (g' * g)

def BilinForm.IsPairSelfAdjoint {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) (F : BilinForm R M) (f : Module.End R M) : Prop

The condition for an endomorphism to be "self-adjoint" with respect to a pair of bilinear forms on the underlying module. In the case that these two forms are identical, this is the usual concept of self adjointness. In the case that one of the forms is the negation of the other, this is the usual concept of skew adjointness.

Equations

• BilinForm.IsPairSelfAdjoint B F f = BilinForm.IsAdjointPair B F f f

def BilinForm.isPairSelfAdjointSubmodule {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] (B₂ : BilinForm R₂ M₂) (F₂ : BilinForm R₂ M₂) : Submodule R₂ (Module.End R₂ M₂)

The set of pair-self-adjoint endomorphisms are a submodule of the type of all endomorphisms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BilinForm.mem_isPairSelfAdjointSubmodule {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] (B₂ : BilinForm R₂ M₂) (F₂ : BilinForm R₂ M₂) (f : Module.End R₂ M₂) : f ∈ BilinForm.isPairSelfAdjointSubmodule B₂ F₂ ↔ BilinForm.IsPairSelfAdjoint B₂ F₂ f

theorem BilinForm.isPairSelfAdjoint_equiv {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {M₂' : Type u_11} [AddCommMonoid M₂'] [Module R₂ M₂'] (B₂ : BilinForm R₂ M₂) (F₂ : BilinForm R₂ M₂) (e : M₂' ≃ₗ[R₂] M₂) (f : Module.End R₂ M₂) : BilinForm.IsPairSelfAdjoint B₂ F₂ f ↔ BilinForm.IsPairSelfAdjoint (BilinForm.comp B₂ ↑e ↑e) (BilinForm.comp F₂ ↑e ↑e) ((LinearEquiv.conj (LinearEquiv.symm e)) f)

def BilinForm.IsSelfAdjoint {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) (f : Module.End R M) : Prop

An endomorphism of a module is self-adjoint with respect to a bilinear form if it serves as an adjoint for itself.

Equations

• BilinForm.IsSelfAdjoint B f = BilinForm.IsAdjointPair B B f f

def BilinForm.IsSkewAdjoint {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁] (B₁ : BilinForm R₁ M₁) (f : Module.End R₁ M₁) : Prop

An endomorphism of a module is skew-adjoint with respect to a bilinear form if its negation serves as an adjoint.

Equations

• BilinForm.IsSkewAdjoint B₁ f = BilinForm.IsAdjointPair B₁ B₁ f (-f)

theorem BilinForm.isSkewAdjoint_iff_neg_self_adjoint {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁] (B₁ : BilinForm R₁ M₁) (f : Module.End R₁ M₁) : BilinForm.IsSkewAdjoint B₁ f ↔ BilinForm.IsAdjointPair (-B₁) B₁ f f

def BilinForm.selfAdjointSubmodule {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] (B₂ : BilinForm R₂ M₂) : Submodule R₂ (Module.End R₂ M₂)

The set of self-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact it is a Jordan subalgebra.)

Equations

• BilinForm.selfAdjointSubmodule B₂ = BilinForm.isPairSelfAdjointSubmodule B₂ B₂

@[simp]

theorem BilinForm.mem_selfAdjointSubmodule {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] (B₂ : BilinForm R₂ M₂) (f : Module.End R₂ M₂) : f ∈ BilinForm.selfAdjointSubmodule B₂ ↔ BilinForm.IsSelfAdjoint B₂ f

def BilinForm.skewAdjointSubmodule {R₃ : Type u_7} {M₃ : Type u_8} [CommRing R₃] [AddCommGroup M₃] [Module R₃ M₃] (B₃ : BilinForm R₃ M₃) : Submodule R₃ (Module.End R₃ M₃)

The set of skew-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact it is a Lie subalgebra.)

Equations

• BilinForm.skewAdjointSubmodule B₃ = BilinForm.isPairSelfAdjointSubmodule (-B₃) B₃

@[simp]

theorem BilinForm.mem_skewAdjointSubmodule {R₃ : Type u_7} {M₃ : Type u_8} [CommRing R₃] [AddCommGroup M₃] [Module R₃ M₃] (B₃ : BilinForm R₃ M₃) (f : Module.End R₃ M₃) : f ∈ BilinForm.skewAdjointSubmodule B₃ ↔ BilinForm.IsSkewAdjoint B₃ f

def BilinForm.Nondegenerate {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (B : 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

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

theorem BilinForm.not_nondegenerate_zero (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] : ¬BilinForm.Nondegenerate 0

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

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

theorem BilinForm.Nondegenerate.congr {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {M₂' : Type u_13} [AddCommMonoid M₂'] [Module R₂ M₂'] {B : BilinForm R₂ M₂} (e : M₂ ≃ₗ[R₂] M₂') (h : BilinForm.Nondegenerate B) : BilinForm.Nondegenerate ((BilinForm.congr e) B)

@[simp]

theorem BilinForm.nondegenerate_congr_iff {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {M₂' : Type u_13} [AddCommMonoid M₂'] [Module R₂ M₂'] {B : BilinForm R₂ M₂} (e : M₂ ≃ₗ[R₂] M₂') : BilinForm.Nondegenerate ((BilinForm.congr e) B) ↔ BilinForm.Nondegenerate B

theorem BilinForm.nondegenerate_iff_ker_eq_bot {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {B : BilinForm R₂ M₂} : BilinForm.Nondegenerate B ↔ LinearMap.ker (BilinForm.toLin B) = ⊥

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

theorem BilinForm.Nondegenerate.ker_eq_bot {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {B : BilinForm R₂ M₂} (h : BilinForm.Nondegenerate B) : LinearMap.ker (BilinForm.toLin B) = ⊥

theorem BilinForm.compLeft_injective {R₁ : Type u_3} {M₁ : Type u_4} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁] (B : BilinForm R₁ M₁) (b : BilinForm.Nondegenerate B) : Function.Injective (BilinForm.compLeft B)

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

noncomputable def BilinForm.toDual {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : BilinForm K V) (b : BilinForm.Nondegenerate B) : 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 with the underlying linear map B.toLin.

Equations

• One or more equations did not get rendered due to their size.

theorem BilinForm.toDual_def {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : BilinForm K V} (b : BilinForm.Nondegenerate B) {m : V} {n : V} : ((BilinForm.toDual B b) m) n = B.bilin m n

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

theorem BilinForm.nonDegenerateFlip_iff {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : BilinForm K V} : BilinForm.Nondegenerate (BilinForm.flip B) ↔ BilinForm.Nondegenerate B

noncomputable def BilinForm.dualBasis {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] {ι : Type u_14} [DecidableEq ι] [Finite ι] (B : BilinForm K V) (hB : BilinForm.Nondegenerate B) (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

• BilinForm.dualBasis B hB b = Basis.map (Basis.dualBasis b) (LinearEquiv.symm (BilinForm.toDual B hB))

@[simp]

theorem BilinForm.dualBasis_repr_apply {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] {ι : Type u_14} [DecidableEq ι] [Finite ι] (B : BilinForm K V) (hB : BilinForm.Nondegenerate B) (b : Basis ι K V) (x : V) (i : ι) : ((BilinForm.dualBasis B hB b).repr x) i = B.bilin x (b i)

theorem BilinForm.apply_dualBasis_left {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] {ι : Type u_14} [DecidableEq ι] [Finite ι] (B : BilinForm K V) (hB : BilinForm.Nondegenerate B) (b : Basis ι K V) (i : ι) (j : ι) : B.bilin ((BilinForm.dualBasis B hB b) i) (b j) = if j = i then 1 else 0

theorem BilinForm.apply_dualBasis_right {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] {ι : Type u_14} [DecidableEq ι] [Finite ι] (B : BilinForm K V) (hB : BilinForm.Nondegenerate B) (sym : BilinForm.IsSymm B) (b : Basis ι K V) (i : ι) (j : ι) : B.bilin (b i) ((BilinForm.dualBasis B hB b) j) = if i = j then 1 else 0

@[simp]

theorem BilinForm.dualBasis_dualBasis_flip {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : BilinForm K V) (hB : BilinForm.Nondegenerate B) {ι : Type u_15} [Finite ι] [DecidableEq ι] (b : Basis ι K V) : BilinForm.dualBasis B hB (BilinForm.dualBasis (BilinForm.flip B) (_ : BilinForm.Nondegenerate (BilinForm.flip B)) b) = b

@[simp]

theorem BilinForm.dualBasis_flip_dualBasis {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] (B : BilinForm K V) (hB : BilinForm.Nondegenerate B) {ι : Type u_15} [Finite ι] [DecidableEq ι] [FiniteDimensional K V] (b : Basis ι K V) : BilinForm.dualBasis (BilinForm.flip B) (_ : BilinForm.Nondegenerate (BilinForm.flip B)) (BilinForm.dualBasis B hB b) = b

@[simp]

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

noncomputable def BilinForm.symmCompOfNondegenerate {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B₁ : BilinForm K V) (B₂ : BilinForm K V) (b₂ : BilinForm.Nondegenerate B₂) : V →ₗ[K] V

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

Equations

• BilinForm.symmCompOfNondegenerate B₁ B₂ b₂ = LinearMap.comp (↑(LinearEquiv.symm (BilinForm.toDual B₂ b₂))) (BilinForm.toLin B₁)

theorem BilinForm.comp_symmCompOfNondegenerate_apply {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B₁ : BilinForm K V) {B₂ : BilinForm K V} (b₂ : BilinForm.Nondegenerate B₂) (v : V) : (BilinForm.toLin B₂) ((BilinForm.symmCompOfNondegenerate B₁ B₂ b₂) v) = (BilinForm.toLin B₁) v

@[simp]

theorem BilinForm.symmCompOfNondegenerate_left_apply {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B₁ : BilinForm K V) {B₂ : BilinForm K V} (b₂ : BilinForm.Nondegenerate B₂) (v : V) (w : V) : B₂.bilin ((BilinForm.symmCompOfNondegenerate B₁ B₂ b₂) w) v = B₁.bilin w v

noncomputable def BilinForm.leftAdjointOfNondegenerate {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : BilinForm K V) (b : BilinForm.Nondegenerate B) (φ : 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

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

theorem BilinForm.isAdjointPairLeftAdjointOfNondegenerate {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : BilinForm K V) (b : BilinForm.Nondegenerate B) (φ : V →ₗ[K] V) : BilinForm.IsAdjointPair B B (BilinForm.leftAdjointOfNondegenerate B b φ) φ

theorem BilinForm.isAdjointPair_iff_eq_of_nondegenerate {V : Type u_9} {K : Type u_10} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : BilinForm K V) (b : BilinForm.Nondegenerate B) (ψ : V →ₗ[K] V) (φ : V →ₗ[K] V) : BilinForm.IsAdjointPair B B ψ φ ↔ ψ = BilinForm.leftAdjointOfNondegenerate B b φ

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