Documentation

TauCeti.LinearAlgebra.Matrix.Dual

The dot product on ι → R is a perfect pairing #

Mathlib's dotProductEquiv identifies ι → R, for ι finite, with its own dual under the dot product. This file records the symmetry and perfectness of this pairing, so that the dot product may be used directly as the pairing of a RootPairing or a RootDatum on ι → R.

Through the same identification, a linear equivalence f : (ι → R) ≃ₗ[R] (κ → R) has a contragredient f.dotProductContragredient, the equivalence g with g y ⬝ᵥ f x = y ⬝ᵥ x. In matrix terms it is the inverse transpose of f. It describes how a linear change of coordinates acts on orthogonal complements for the dot product, for instance on the dual of a linear code.

Main results #

source
instance TauCeti.dotProductBilin_isPerfPair (R : Type u_1) (ι : Type u_2) [CommSemiring R] [Fintype ι] :
(dotProductBilin R R).IsPerfPair

Over a commutative semiring, the dot product on ι → R is a perfect pairing of that module with itself: it is Mathlib's dotProductEquiv read as a bilinear map.

source
theorem TauCeti.isSymm_dotProductBilin {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] :
LinearMap.BilinForm.IsSymm (dotProductBilin R R)

The standard dot-product bilinear form is symmetric.

source
theorem TauCeti.linearIndependent_of_dotProduct_diagonal {κ : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype ι] [Ring R] {v w : κ → ι → R} {c : κ → R} (hc : ∀ (i : κ), IsRightRegular (c i)) (hdiag : ∀ (i : κ), v i ⬝ᵥ w i = c i) (hoff : ∀ (i j : κ), i ≠ j → v i ⬝ᵥ w j = 0) :
LinearIndependent R v

A family paired diagonally by a second family is linearly independent. If v i ⬝ᵥ w j vanishes whenever i ≠ j and right multiplication by v i ⬝ᵥ w i is injective, the v i are linearly independent. Over a ring without zero divisors, nonzero diagonal entries suffice; in particular, this applies over ℤ with diagonal 2. The ring may have zero divisors away from the chosen diagonal entries. The family index κ is arbitrary — neither finite nor decidable — and unrelated to the coordinate index ι; the scalars need not commute.

The contragredient of a linear equivalence for the dot product #

source
def LinearEquiv.dotProductContragredient {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (f : (ι → R) ≃ₗ[R] κ → R) :
(ι → R) ≃ₗ[R] κ → R

The contragredient of a linear equivalence f : (ι → R) ≃ₗ[R] (κ → R) for the dot product: the linear equivalence g with g y ⬝ᵥ f x = y ⬝ᵥ x for all x and y (LinearEquiv.eq_dotProductContragredient_iff). It is the dual map of f.symm, read through the identifications dotProductEquiv of ι → R and κ → R with their duals, and its matrix is the transpose of the matrix of f.symm (LinearEquiv.toMatrix'_dotProductContragredient).

Equations
Instances For
    source
    @[simp]
    theorem LinearEquiv.dotProductContragredient_apply_dotProduct {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (f : (ι → R) ≃ₗ[R] κ → R) (y : ι → R) (x : κ → R) :
    f.dotProductContragredient y ⬝ᵥ x = y ⬝ᵥ f.symm x

    The contragredient of f is adjoint, for the dot product, to the inverse of f.

    source
    theorem LinearEquiv.dotProductContragredient_apply_dotProduct_apply {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (f : (ι → R) ≃ₗ[R] κ → R) (y x : ι → R) :
    f.dotProductContragredient y ⬝ᵥ f x = y ⬝ᵥ x

    A linear equivalence and its contragredient preserve the dot product jointly.

    source
    @[simp]
    theorem LinearEquiv.apply_dotProduct_dotProductContragredient_apply {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (f : (ι → R) ≃ₗ[R] κ → R) (x y : ι → R) :
    f x ⬝ᵥ f.dotProductContragredient y = x ⬝ᵥ y

    A linear equivalence and its contragredient preserve the dot product jointly, with the contragredient applied on the right.

    source
    theorem LinearEquiv.eq_dotProductContragredient_iff {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] {f g : (ι → R) ≃ₗ[R] κ → R} :
    g = f.dotProductContragredient ↔ ∀ (y x : ι → R), g y ⬝ᵥ f x = y ⬝ᵥ x

    The contragredient of f is the unique linear equivalence g with g y ⬝ᵥ f x = y ⬝ᵥ x.

    source
    @[simp]
    theorem LinearEquiv.toMatrix'_dotProductContragredient {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (f : (ι → R) ≃ₗ[R] κ → R) :
    LinearMap.toMatrix' ↑f.dotProductContragredient = (LinearMap.toMatrix' ↑f.symm).transpose

    The matrix of the contragredient of f is the transpose of the matrix of f.symm.

    source
    @[simp]
    theorem LinearEquiv.dotProductContragredient_refl {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] [DecidableEq ι] :
    (refl R (ι → R)).dotProductContragredient = refl R (ι → R)

    The contragredient of the identity is the identity.

    source
    @[simp]
    theorem LinearEquiv.dotProductContragredient_trans {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {μ : Type u_4} [CommSemiring R] [Fintype ι] [Fintype κ] [Fintype μ] [DecidableEq ι] [DecidableEq κ] [DecidableEq μ] (f : (ι → R) ≃ₗ[R] κ → R) (g : (κ → R) ≃ₗ[R] μ → R) :
    (f ≪≫ₗ g).dotProductContragredient = f.dotProductContragredient ≪≫ₗ g.dotProductContragredient

    Taking the contragredient is compatible with composition: the contragredient of f.trans g is the composite of the contragredients of f and g.

    source
    @[simp]
    theorem LinearEquiv.dotProductContragredient_symm {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (f : (ι → R) ≃ₗ[R] κ → R) :
    f.symm.dotProductContragredient = f.dotProductContragredient.symm

    Taking the contragredient is compatible with inversion: the contragredient of f.symm is the inverse of the contragredient of f.

    source
    @[simp]
    theorem LinearEquiv.dotProductContragredient_dotProductContragredient {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (f : (ι → R) ≃ₗ[R] κ → R) :
    f.dotProductContragredient.dotProductContragredient = f

    Taking the contragredient is an involution.