Documentation

TauCeti.LinearAlgebra.BilinearForm.Prod

Products of bilinear forms #

The product of two bilinear forms is the block-diagonal form on the product module: each factor carries its own form and the two factors are orthogonal to each other. It is the bilinear counterpart of QuadraticMap.prod, and it is the form an orthogonal direct sum of bilinear modules carries.

Symmetry, separation and nondegeneracy are componentwise, flipping is componentwise, and a product of perfect pairings is a perfect pairing.

Main declarations #

source
def LinearMap.BilinForm.prod {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (B : LinearMap.BilinForm R M) (C : LinearMap.BilinForm R N) :
LinearMap.BilinForm R (M × N)

The block-diagonal bilinear form on a product module: the two factors keep their own forms and pair to zero with each other.

Instances For
    source
    @[simp]
    theorem LinearMap.BilinForm.prod_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (B : LinearMap.BilinForm R M) (C : LinearMap.BilinForm R N) (x y : M × N) :
    ((B.prod C) x) y = (B x.1) y.1 + (C x.2) y.2
    source
    @[simp]
    theorem LinearMap.BilinForm.toQuadraticMap_prod {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (B : LinearMap.BilinForm R M) (C : LinearMap.BilinForm R N) :
    BilinMap.toQuadraticMap (B.prod C) = (BilinMap.toQuadraticMap B).prod (BilinMap.toQuadraticMap C)

    The quadratic map of a product of bilinear forms is the product of the quadratic maps.

    source
    @[simp]
    theorem LinearMap.BilinForm.isSymm_prod_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {B : LinearMap.BilinForm R M} {C : LinearMap.BilinForm R N} :
    (B.prod C).IsSymm ↔ B.IsSymm ∧ C.IsSymm

    A product of bilinear forms is symmetric exactly when both factors are.

    source
    @[simp]
    theorem LinearMap.BilinForm.flip_prod {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (B : LinearMap.BilinForm R M) (C : LinearMap.BilinForm R N) :
    LinearMap.flip (B.prod C) = prod (LinearMap.flip B) (LinearMap.flip C)

    Flipping a product of bilinear forms flips each factor.

    source
    @[simp]
    theorem LinearMap.BilinForm.separatingLeft_prod_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {B : LinearMap.BilinForm R M} {C : LinearMap.BilinForm R N} :
    SeparatingLeft (B.prod C) ↔ SeparatingLeft B ∧ SeparatingLeft C

    A product of bilinear forms is left-separating exactly when both factors are.

    source
    @[simp]
    theorem LinearMap.BilinForm.separatingRight_prod_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {B : LinearMap.BilinForm R M} {C : LinearMap.BilinForm R N} :
    SeparatingRight (B.prod C) ↔ SeparatingRight B ∧ SeparatingRight C

    A product of bilinear forms is right-separating exactly when both factors are.

    source
    @[simp]
    theorem LinearMap.BilinForm.nondegenerate_prod_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {B : LinearMap.BilinForm R M} {C : LinearMap.BilinForm R N} :
    (B.prod C).Nondegenerate ↔ B.Nondegenerate ∧ C.Nondegenerate

    A product of bilinear forms is nondegenerate exactly when both factors are.

    source
    instance LinearMap.BilinForm.instIsPerfPairProd {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {B : LinearMap.BilinForm R M} {C : LinearMap.BilinForm R N} [IsPerfPair B] [IsPerfPair C] :
    IsPerfPair (B.prod C)

    A product of perfect pairings is a perfect pairing.