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

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), self.bilin (x + y) z = self.bilin x z + self.bilin y z
• bilin_smul_left : ∀ (a : R) (x y : M), self.bilin (a • x) y = a * self.bilin x y
• bilin_add_right : ∀ (x y z : M), self.bilin x (y + z) = self.bilin x y + self.bilin x z
• bilin_smul_right : ∀ (a : R) (x y : M), self.bilin x (a • y) = a * self.bilin x y

instance BilinForm.instCoeFunBilinFormForAll {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] : CoeFun (BilinForm R M) fun (x : BilinForm R M) => M → M → R

Equations

• BilinForm.instCoeFunBilinFormForAll = { coe := BilinForm.bilin }

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' → B.bilin x y = B.bilin 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) : B.bilin (x + y) z = B.bilin x z + B.bilin 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) : B.bilin (a • x) y = a * B.bilin 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) : B.bilin x (y + z) = B.bilin x y + B.bilin 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) : B.bilin x (a • y) = a * B.bilin 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) : B.bilin 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) : B.bilin 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₁) : B₁.bilin (-x) y = -B₁.bilin 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₁) : B₁.bilin x (-y) = -B₁.bilin 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₁) : B₁.bilin (x - y) z = B₁.bilin x z - B₁.bilin 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₁) : B₁.bilin x (y - z) = B₁.bilin x y - B₁.bilin 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) : B.bilin (r • x) y = r • B.bilin 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) : B.bilin x (r • y) = r • B.bilin 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), B.bilin x y = D.bilin 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) : B.bilin x y = D.bilin 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), B.bilin x y = D.bilin x y

instance BilinForm.instZeroBilinForm {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] : Zero (BilinForm 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) : 0.bilin x y = 0

instance BilinForm.instAddBilinForm {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] : Add (BilinForm 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} [Semiring R] [AddCommMonoid M] [Module R M] (B : BilinForm R M) (D : BilinForm R M) : (B + D).bilin = B.bilin + D.bilin

@[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) : (B + D).bilin x y = B.bilin x y + D.bilin 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] : SMul α (BilinForm R M)

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) : (a • B).bilin = a • B.bilin

@[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) : (a • B).bilin x y = a • B.bilin 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₁] : Neg (BilinForm R₁ M₁)

Equations

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

@[simp]

theorem BilinForm.coe_neg {R₁ : Type u_4} {M₁ : Type u_5} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁] (B₁ : BilinForm R₁ M₁) : (-B₁).bilin = -B₁.bilin

@[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₁) : (-B₁).bilin x y = -B₁.bilin x y

instance BilinForm.instSubBilinFormToSemiringToAddCommMonoid {R₁ : Type u_4} {M₁ : Type u_5} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁] : Sub (BilinForm R₁ M₁)

Equations

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

@[simp]

theorem BilinForm.coe_sub {R₁ : Type u_4} {M₁ : Type u_5} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁] (B₁ : BilinForm R₁ M₁) (D₁ : BilinForm R₁ M₁) : (B₁ - D₁).bilin = B₁.bilin - D₁.bilin

@[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₁) : (B₁ - D₁).bilin x y = B₁.bilin x y - D₁.bilin 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] : Inhabited (BilinForm 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] : BilinForm R M →+ M → M → R

coeFn as an AddMonoidHom

Equations

• BilinForm.coeFnAddMonoidHom = { toZeroHom := { toFun := BilinForm.bilin, map_zero' := (_ : 0.bilin = 0) }, map_add' := (_ : ∀ (B D : BilinForm R M), (B + D).bilin = B.bilin + D.bilin) }

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] : Module α (BilinForm R M)

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] : BilinForm R M →ₗ[R₂] BilinForm 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.

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] : BilinForm R M ≃ₗ[R₂] BilinForm R M

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.

@[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.flipHom R₂) A).bilin x y = A.bilin 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]

abbrev BilinForm.flip' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] : BilinForm R M ≃ₗ[ℕ] BilinForm R M

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 ℕ

@[inline, reducible]

abbrev BilinForm.flip {R₂ : Type u_6} {M₂ : Type u_7} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] : BilinForm R₂ M₂ ≃ₗ[R₂] BilinForm 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₂

@[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.restrict B W).bilin a b = B.bilin ↑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.