Bilinear form #
This file defines a bilinear form over a module. Basic ideas such as orthogonality are also introduced, as well as reflexive, symmetric, non-degenerate and alternating bilinear forms. Adjoints of linear maps with respect to a bilinear form are also introduced.
A bilinear form on an R-(semi)module M, is a function from M × M to R,
that is linear in both arguments. Comments will typically abbreviate
"(semi)module" as just "module", but the definitions should be as general as
possible.
The result that there exists an orthogonal basis with respect to a symmetric,
nondegenerate bilinear form can be found in QuadraticForm.lean with
exists_orthogonal_basis.
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 semiringR,M₁,M₁', ... are modules over the commutative ringR₁,V, ... is a vector space over the fieldK.
References #
Tags #
Bilinear form,
structure
BilinForm
(R : Type u_1)
(M : Type u_2)
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
Type (max u_1 u_2)
BilinForm R M is the type of R-bilinear functions M → M → R.
- bilin : M → M → R
Instances For
instance
BilinForm.instCoeFunBilinFormForAll
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
Equations
- BilinForm.instCoeFunBilinFormForAll = { coe := BilinForm.bilin }
theorem
BilinForm.coeFn_mk
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(f : M → M → R)
(h₁ : ∀ (x y z : M), f (x + y) z = f x z + f y z)
(h₂ : ∀ (a : R) (x y : M), f (a • x) y = a * f x y)
(h₃ : ∀ (x y z : M), f x (y + z) = f x y + f x z)
(h₄ : ∀ (a : R) (x y : M), f x (a • y) = a * f x y)
:
{ bilin := f, bilin_add_left := h₁, bilin_smul_left := h₂, bilin_add_right := h₃, bilin_smul_right := h₄ }.bilin = f
theorem
BilinForm.coeFn_congr
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
{x : M}
{x' : M}
{y : M}
{y' : M}
:
@[simp]
theorem
BilinForm.add_left
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
(x : M)
(y : M)
(z : M)
:
@[simp]
theorem
BilinForm.smul_left
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
(a : R)
(x : M)
(y : M)
:
@[simp]
theorem
BilinForm.add_right
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
(x : M)
(y : M)
(z : M)
:
@[simp]
theorem
BilinForm.smul_right
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
(a : R)
(x : M)
(y : M)
:
@[simp]
theorem
BilinForm.zero_left
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
(x : M)
:
B.bilin 0 x = 0
@[simp]
theorem
BilinForm.zero_right
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
(x : M)
:
B.bilin x 0 = 0
@[simp]
theorem
BilinForm.smul_left_of_tower
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_3}
[CommSemiring S]
[Algebra S R]
[Module S M]
[IsScalarTower S R M]
{B : BilinForm R M}
(r : S)
(x : M)
(y : M)
:
@[simp]
theorem
BilinForm.smul_right_of_tower
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_3}
[CommSemiring S]
[Algebra S R]
[Module S M]
[IsScalarTower S R M]
{B : BilinForm R M}
(r : S)
(x : M)
(y : M)
:
theorem
BilinForm.coe_injective
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
Function.Injective BilinForm.bilin
theorem
BilinForm.ext
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
{D : BilinForm R M}
(H : ∀ (x y : M), B.bilin x y = D.bilin x y)
:
B = D
theorem
BilinForm.congr_fun
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
{D : BilinForm R M}
(h : B = D)
(x : M)
(y : M)
:
B.bilin x y = D.bilin x y
theorem
BilinForm.ext_iff
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
{D : BilinForm R M}
:
instance
BilinForm.instZeroBilinForm
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
Equations
- BilinForm.instZeroBilinForm = { zero := { bilin := fun (x x : M) => 0, bilin_add_left := ⋯, bilin_smul_left := ⋯, bilin_add_right := ⋯, bilin_smul_right := ⋯ } }
@[simp]
theorem
BilinForm.coe_zero
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
0.bilin = 0
@[simp]
theorem
BilinForm.zero_apply
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(x : M)
(y : M)
:
0.bilin x y = 0
instance
BilinForm.instAddBilinForm
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
BilinForm.coe_add
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(B : BilinForm R M)
(D : BilinForm R M)
:
@[simp]
theorem
BilinForm.add_apply
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(B : BilinForm R M)
(D : BilinForm R M)
(x : M)
(y : M)
:
instance
BilinForm.instSMulBilinForm
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_8}
[Monoid α]
[DistribMulAction α R]
[SMulCommClass α R R]
:
BilinForm R M inherits the scalar action by α on R if this is compatible with
multiplication.
When R itself is commutative, this provides an R-action via Algebra.id.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
BilinForm.coe_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 : BilinForm R M)
:
@[simp]
theorem
BilinForm.smul_apply
{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 : BilinForm R M)
(x : M)
(y : M)
:
instance
BilinForm.instSMulCommClassBilinFormInstSMulBilinFormInstSMulBilinForm
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_8}
{β : Type u_9}
[Monoid α]
[Monoid β]
[DistribMulAction α R]
[DistribMulAction β R]
[SMulCommClass α R R]
[SMulCommClass β R R]
[SMulCommClass α β R]
:
SMulCommClass α β (BilinForm R M)
Equations
- ⋯ = ⋯
instance
BilinForm.instIsScalarTowerBilinFormInstSMulBilinFormInstSMulBilinForm
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_8}
{β : Type u_9}
[Monoid α]
[Monoid β]
[SMul α β]
[DistribMulAction α R]
[DistribMulAction β R]
[SMulCommClass α R R]
[SMulCommClass β R R]
[IsScalarTower α β R]
:
IsScalarTower α β (BilinForm R M)
Equations
- ⋯ = ⋯
instance
BilinForm.instIsCentralScalarBilinFormInstSMulBilinFormMulOppositeMonoidOp_leftToSMulToZeroToCommMonoidWithZeroToSMulZeroClassToAddZeroClassToAddMonoidToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToSemiringToDistribSMulToSMulId
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_8}
[Monoid α]
[DistribMulAction α R]
[DistribMulAction αᵐᵒᵖ R]
[SMulCommClass α R R]
[IsCentralScalar α R]
:
IsCentralScalar α (BilinForm R M)
Equations
- ⋯ = ⋯
instance
BilinForm.instAddCommMonoidBilinForm
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
AddCommMonoid (BilinForm R M)
Equations
- BilinForm.instAddCommMonoidBilinForm = Function.Injective.addCommMonoid BilinForm.bilin ⋯ ⋯ ⋯ ⋯
instance
BilinForm.instNegBilinFormToCommSemiringToAddCommMonoid
{R₁ : Type u_4}
{M₁ : Type u_5}
[CommRing R₁]
[AddCommGroup M₁]
[Module R₁ M₁]
:
Equations
- One or more equations did not get rendered due to their size.
instance
BilinForm.instSubBilinFormToCommSemiringToAddCommMonoid
{R₁ : Type u_4}
{M₁ : Type u_5}
[CommRing R₁]
[AddCommGroup M₁]
[Module R₁ M₁]
:
Equations
- One or more equations did not get rendered due to their size.
instance
BilinForm.instAddCommGroupBilinFormToCommSemiringToAddCommMonoid
{R₁ : Type u_4}
{M₁ : Type u_5}
[CommRing R₁]
[AddCommGroup M₁]
[Module R₁ M₁]
:
AddCommGroup (BilinForm R₁ M₁)
Equations
- BilinForm.instAddCommGroupBilinFormToCommSemiringToAddCommMonoid = Function.Injective.addCommGroup BilinForm.bilin ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
instance
BilinForm.instInhabitedBilinForm
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
Equations
- BilinForm.instInhabitedBilinForm = { default := 0 }
def
BilinForm.coeFnAddMonoidHom
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
coeFn as an AddMonoidHom
Equations
- BilinForm.coeFnAddMonoidHom = { toZeroHom := { toFun := BilinForm.bilin, map_zero' := ⋯ }, map_add' := ⋯ }
Instances For
instance
BilinForm.instDistribMulActionBilinFormToAddMonoidInstAddCommMonoidBilinForm
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_8}
[Monoid α]
[DistribMulAction α R]
[SMulCommClass α R R]
:
DistribMulAction α (BilinForm R M)
Equations
- BilinForm.instDistribMulActionBilinFormToAddMonoidInstAddCommMonoidBilinForm = Function.Injective.distribMulAction BilinForm.coeFnAddMonoidHom ⋯ ⋯
instance
BilinForm.instModuleBilinFormToSemiringInstAddCommMonoidBilinForm
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_8}
[CommSemiring α]
[Module α R]
[SMulCommClass α R R]
:
Equations
- BilinForm.instModuleBilinFormToSemiringInstAddCommMonoidBilinForm = Function.Injective.module α BilinForm.coeFnAddMonoidHom ⋯ ⋯
def
BilinForm.flipHomAux
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
Auxiliary construction for the flip of a bilinear form, obtained by exchanging the left and
right arguments. This version is a LinearMap; it is later upgraded to a LinearEquiv
in flipHom.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
BilinForm.flip_flip_aux
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(A : BilinForm R M)
:
BilinForm.flipHomAux (BilinForm.flipHomAux A) = A
def
BilinForm.flipHom
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
The flip of a bilinear form, obtained by exchanging the left and right arguments.
Equations
- BilinForm.flipHom = let __src := BilinForm.flipHomAux; { toLinearMap := __src, invFun := ⇑BilinForm.flipHomAux, left_inv := ⋯, right_inv := ⋯ }
Instances For
@[simp]
theorem
BilinForm.flip_apply
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(A : BilinForm R M)
(x : M)
(y : M)
:
(BilinForm.flipHom A).bilin x y = A.bilin y x
theorem
BilinForm.flip_flip
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
BilinForm.flipHom ≪≫ₗ BilinForm.flipHom = LinearEquiv.refl R (BilinForm R M)
@[inline, reducible]
abbrev
BilinForm.flip
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
The flip of a bilinear form over a commutative ring, obtained by exchanging the left and
right arguments.
Equations
- BilinForm.flip = BilinForm.flipHom
Instances For
@[simp]
theorem
BilinForm.restrict_apply
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(B : BilinForm R M)
(W : Submodule R M)
(a : ↥W)
(b : ↥W)
:
(BilinForm.restrict B W).bilin a b = B.bilin ↑a ↑b
def
BilinForm.restrict
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(B : BilinForm R M)
(W : Submodule R M)
:
BilinForm R ↥W
The restriction of a bilinear form on a submodule.
Equations
- BilinForm.restrict B W = { bilin := fun (a b : ↥W) => B.bilin ↑a ↑b, bilin_add_left := ⋯, bilin_smul_left := ⋯, bilin_add_right := ⋯, bilin_smul_right := ⋯ }