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 semiringR,M₁,M₁', ... are modules over the ringR₁,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)
[Semiring 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
- bilin_add_left : ∀ (x y z : M), BilinForm.bilin s (x + y) z = BilinForm.bilin s x z + BilinForm.bilin s y z
- bilin_smul_left : ∀ (a : R) (x y : M), BilinForm.bilin s (a • x) y = a * BilinForm.bilin s x y
- bilin_add_right : ∀ (x y z : M), BilinForm.bilin s x (y + z) = BilinForm.bilin s x y + BilinForm.bilin s x z
- bilin_smul_right : ∀ (a : R) (x y : M), BilinForm.bilin s x (a • y) = a * BilinForm.bilin s x y
Instances For
theorem
BilinForm.coeFn_mk
{R : Type u_1}
{M : Type u_2}
[Semiring 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}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
{x : M}
{x' : M}
{y : M}
{y' : M}
:
x = x' → y = y' → BilinForm.bilin B x y = BilinForm.bilin B x' y'
@[simp]
theorem
BilinForm.add_left
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
(x : M)
(y : M)
(z : M)
:
BilinForm.bilin B (x + y) z = BilinForm.bilin B x z + BilinForm.bilin B y z
@[simp]
theorem
BilinForm.smul_left
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
(a : R)
(x : M)
(y : M)
:
BilinForm.bilin B (a • x) y = a * BilinForm.bilin B x y
@[simp]
theorem
BilinForm.add_right
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
(x : M)
(y : M)
(z : M)
:
BilinForm.bilin B x (y + z) = BilinForm.bilin B x y + BilinForm.bilin B x z
@[simp]
theorem
BilinForm.smul_right
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
(a : R)
(x : M)
(y : M)
:
BilinForm.bilin B x (a • y) = a * BilinForm.bilin B x y
@[simp]
theorem
BilinForm.zero_left
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
(x : M)
:
BilinForm.bilin B 0 x = 0
@[simp]
theorem
BilinForm.zero_right
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
(x : M)
:
BilinForm.bilin B x 0 = 0
@[simp]
theorem
BilinForm.neg_left
{R₁ : Type u_4}
{M₁ : Type u_5}
[Ring R₁]
[AddCommGroup M₁]
[Module R₁ M₁]
{B₁ : BilinForm R₁ M₁}
(x : M₁)
(y : M₁)
:
BilinForm.bilin B₁ (-x) y = -BilinForm.bilin B₁ x y
@[simp]
theorem
BilinForm.neg_right
{R₁ : Type u_4}
{M₁ : Type u_5}
[Ring R₁]
[AddCommGroup M₁]
[Module R₁ M₁]
{B₁ : BilinForm R₁ M₁}
(x : M₁)
(y : M₁)
:
BilinForm.bilin B₁ x (-y) = -BilinForm.bilin B₁ x y
@[simp]
theorem
BilinForm.sub_left
{R₁ : Type u_4}
{M₁ : Type u_5}
[Ring R₁]
[AddCommGroup M₁]
[Module R₁ M₁]
{B₁ : BilinForm R₁ M₁}
(x : M₁)
(y : M₁)
(z : M₁)
:
BilinForm.bilin B₁ (x - y) z = BilinForm.bilin B₁ x z - BilinForm.bilin B₁ y z
@[simp]
theorem
BilinForm.sub_right
{R₁ : Type u_4}
{M₁ : Type u_5}
[Ring R₁]
[AddCommGroup M₁]
[Module R₁ M₁]
{B₁ : BilinForm R₁ M₁}
(x : M₁)
(y : M₁)
(z : M₁)
:
BilinForm.bilin B₁ x (y - z) = BilinForm.bilin B₁ x y - BilinForm.bilin B₁ x z
@[simp]
theorem
BilinForm.smul_left_of_tower
{R : Type u_1}
{M : Type u_2}
[Semiring 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)
:
BilinForm.bilin B (r • x) y = r • BilinForm.bilin B x y
@[simp]
theorem
BilinForm.smul_right_of_tower
{R : Type u_1}
{M : Type u_2}
[Semiring 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)
:
BilinForm.bilin B x (r • y) = r • BilinForm.bilin B x y
theorem
BilinForm.coe_injective
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Function.Injective BilinForm.bilin
theorem
BilinForm.ext
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
{D : BilinForm R M}
(H : ∀ (x y : M), BilinForm.bilin B x y = BilinForm.bilin D x y)
:
B = D
theorem
BilinForm.congr_fun
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
{D : BilinForm R M}
(h : B = D)
(x : M)
(y : M)
:
BilinForm.bilin B x y = BilinForm.bilin D x y
theorem
BilinForm.ext_iff
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{B : BilinForm R M}
{D : BilinForm R M}
:
B = D ↔ ∀ (x y : M), BilinForm.bilin B x y = BilinForm.bilin D x y
instance
BilinForm.instZeroBilinForm
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
BilinForm.coe_zero
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
0.bilin = 0
@[simp]
theorem
BilinForm.zero_apply
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(x : M)
(y : M)
:
BilinForm.bilin 0 x y = 0
instance
BilinForm.instAddBilinForm
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
BilinForm.add_apply
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(B : BilinForm R M)
(D : BilinForm R M)
(x : M)
(y : M)
:
BilinForm.bilin (B + D) x y = BilinForm.bilin B x y + BilinForm.bilin D x y
instance
BilinForm.instSMulBilinForm
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_12}
[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}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_12}
[Monoid α]
[DistribMulAction α R]
[SMulCommClass α R R]
(a : α)
(B : BilinForm R M)
:
@[simp]
theorem
BilinForm.smul_apply
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_12}
[Monoid α]
[DistribMulAction α R]
[SMulCommClass α R R]
(a : α)
(B : BilinForm R M)
(x : M)
(y : M)
:
BilinForm.bilin (a • B) x y = a • BilinForm.bilin B x y
instance
BilinForm.instSMulCommClassBilinFormInstSMulBilinFormInstSMulBilinForm
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_12}
{β : Type u_13}
[Monoid α]
[Monoid β]
[DistribMulAction α R]
[DistribMulAction β R]
[SMulCommClass α R R]
[SMulCommClass β R R]
[SMulCommClass α β R]
:
SMulCommClass α β (BilinForm R M)
Equations
- (_ : SMulCommClass α β (BilinForm R M)) = (_ : SMulCommClass α β (BilinForm R M))
instance
BilinForm.instIsScalarTowerBilinFormInstSMulBilinFormInstSMulBilinForm
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_12}
{β : Type u_13}
[Monoid α]
[Monoid β]
[SMul α β]
[DistribMulAction α R]
[DistribMulAction β R]
[SMulCommClass α R R]
[SMulCommClass β R R]
[IsScalarTower α β R]
:
IsScalarTower α β (BilinForm R M)
Equations
- (_ : IsScalarTower α β (BilinForm R M)) = (_ : IsScalarTower α β (BilinForm R M))
instance
BilinForm.instIsCentralScalarBilinFormInstSMulBilinFormMulOppositeMonoidOp_leftToSMulToZeroToMonoidWithZeroToSMulZeroClassToAddZeroClassToAddMonoidToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToDistribSMulToSMulToSMulZeroClassToSMulWithZeroToMulZeroClassToNonUnitalNonAssocSemiring
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_12}
[Monoid α]
[DistribMulAction α R]
[DistribMulAction αᵐᵒᵖ R]
[SMulCommClass α R R]
[IsCentralScalar α R]
:
IsCentralScalar α (BilinForm R M)
Equations
- (_ : IsCentralScalar α (BilinForm R M)) = (_ : IsCentralScalar α (BilinForm R M))
instance
BilinForm.instAddCommMonoidBilinForm
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
AddCommMonoid (BilinForm R M)
Equations
- One or more equations did not get rendered due to their size.
instance
BilinForm.instNegBilinFormToSemiringToAddCommMonoid
{R₁ : Type u_4}
{M₁ : Type u_5}
[Ring R₁]
[AddCommGroup M₁]
[Module R₁ M₁]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
BilinForm.neg_apply
{R₁ : Type u_4}
{M₁ : Type u_5}
[Ring R₁]
[AddCommGroup M₁]
[Module R₁ M₁]
(B₁ : BilinForm R₁ M₁)
(x : M₁)
(y : M₁)
:
BilinForm.bilin (-B₁) x y = -BilinForm.bilin B₁ x y
instance
BilinForm.instSubBilinFormToSemiringToAddCommMonoid
{R₁ : Type u_4}
{M₁ : Type u_5}
[Ring R₁]
[AddCommGroup M₁]
[Module R₁ M₁]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
BilinForm.sub_apply
{R₁ : Type u_4}
{M₁ : Type u_5}
[Ring R₁]
[AddCommGroup M₁]
[Module R₁ M₁]
(B₁ : BilinForm R₁ M₁)
(D₁ : BilinForm R₁ M₁)
(x : M₁)
(y : M₁)
:
BilinForm.bilin (B₁ - D₁) x y = BilinForm.bilin B₁ x y - BilinForm.bilin D₁ x y
instance
BilinForm.instAddCommGroupBilinFormToSemiringToAddCommMonoid
{R₁ : Type u_4}
{M₁ : Type u_5}
[Ring R₁]
[AddCommGroup M₁]
[Module R₁ M₁]
:
AddCommGroup (BilinForm R₁ M₁)
Equations
- One or more equations did not get rendered due to their size.
instance
BilinForm.instInhabitedBilinForm
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Equations
- BilinForm.instInhabitedBilinForm = { default := 0 }
def
BilinForm.coeFnAddMonoidHom
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
coeFn as an AddMonoidHom
Equations
Instances For
instance
BilinForm.instDistribMulActionBilinFormToAddMonoidInstAddCommMonoidBilinForm
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_12}
[Monoid α]
[DistribMulAction α R]
[SMulCommClass α R R]
:
DistribMulAction α (BilinForm R M)
Equations
- One or more equations did not get rendered due to their size.
instance
BilinForm.instModuleBilinFormInstAddCommMonoidBilinForm
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_12}
[Semiring α]
[Module α R]
[SMulCommClass α R R]
:
Equations
- One or more equations did not get rendered due to their size.
def
BilinForm.flipHomAux
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(R₂ : Type u_6)
[CommSemiring R₂]
[Algebra R₂ R]
:
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}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{R₂ : Type u_6}
[CommSemiring R₂]
[Algebra R₂ R]
(A : BilinForm R M)
:
(BilinForm.flipHomAux R₂) ((BilinForm.flipHomAux R₂) A) = A
def
BilinForm.flipHom
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(R₂ : Type u_6)
[CommSemiring R₂]
[Algebra R₂ R]
:
The flip of a bilinear form, obtained by exchanging the left and right arguments. This is a
less structured version of the equiv which applies to general (noncommutative) rings R with a
distinguished commutative subring R₂; over a commutative ring use flip.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
BilinForm.flip_apply
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{R₂ : Type u_6}
[CommSemiring R₂]
[Algebra R₂ R]
(A : BilinForm R M)
(x : M)
(y : M)
:
BilinForm.bilin ((BilinForm.flipHom R₂) A) x y = BilinForm.bilin A y x
theorem
BilinForm.flip_flip
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{R₂ : Type u_6}
[CommSemiring R₂]
[Algebra R₂ R]
:
BilinForm.flipHom R₂ ≪≫ₗ BilinForm.flipHom R₂ = LinearEquiv.refl R₂ (BilinForm R M)
@[inline, reducible]
The flip of a bilinear form over a ring, obtained by exchanging the left and right arguments,
here considered as an ℕ-linear equivalence, i.e. an additive equivalence.
Equations
- BilinForm.flip' = BilinForm.flipHom ℕ
Instances For
@[inline, reducible]
abbrev
BilinForm.flip
{R₂ : Type u_6}
{M₂ : Type u_7}
[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 R₂
Instances For
@[simp]
theorem
BilinForm.restrict_apply
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(B : BilinForm R M)
(W : Submodule R M)
(a : ↥W)
(b : ↥W)
:
BilinForm.bilin (BilinForm.restrict B W) a b = BilinForm.bilin B ↑a ↑b
def
BilinForm.restrict
{R : Type u_1}
{M : Type u_2}
[Semiring 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
- One or more equations did not get rendered due to their size.