Documentation

Mathlib.LinearAlgebra.BilinearForm.DualLattice

Dual submodule with respect to a bilinear form. #

Main definitions and results #

TODO #

Properly develop the material in the context of lattices.

def LinearMap.BilinForm.dualSubmodule {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) (N : Submodule R M) :

The dual submodule of a submodule with respect to a bilinear form.

Equations
  • B.dualSubmodule N = { carrier := {x : M | yN, (B x) y 1}, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
    theorem LinearMap.BilinForm.mem_dualSubmodule {R : Type u_1} {S : Type u_3} {M : Type u_2} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) {N : Submodule R M} {x : M} :
    x B.dualSubmodule N yN, (B x) y 1
    theorem LinearMap.BilinForm.le_flip_dualSubmodule {R : Type u_1} {S : Type u_3} {M : Type u_2} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) {N₁ : Submodule R M} {N₂ : Submodule R M} :
    N₁ B.flip.dualSubmodule N₂ N₂ B.dualSubmodule N₁
    noncomputable def LinearMap.BilinForm.dualSubmoduleParing {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) {N : Submodule R M} (x : (B.dualSubmodule N)) (y : N) :
    R

    The natural paring of B.dualSubmodule N and N. This is bundled as a bilinear map in BilinForm.dualSubmoduleToDual.

    Equations
    Instances For
      @[simp]
      theorem LinearMap.BilinForm.dualSubmoduleParing_spec {R : Type u_1} {S : Type u_3} {M : Type u_2} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) {N : Submodule R M} (x : (B.dualSubmodule N)) (y : N) :
      (algebraMap R S) (B.dualSubmoduleParing x y) = (B x) y
      @[simp]
      theorem LinearMap.BilinForm.dualSubmoduleToDual_apply_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) [NoZeroSMulDivisors R S] (N : Submodule R M) (x : (B.dualSubmodule N)) (y : N) :
      ((B.dualSubmoduleToDual N) x) y = B.dualSubmoduleParing x y
      noncomputable def LinearMap.BilinForm.dualSubmoduleToDual {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) [NoZeroSMulDivisors R S] (N : Submodule R M) :
      (B.dualSubmodule N) →ₗ[R] Module.Dual R N

      The natural paring of B.dualSubmodule N and N.

      Equations
      • B.dualSubmoduleToDual N = { toFun := fun (x : (B.dualSubmodule N)) => { toFun := B.dualSubmoduleParing x, map_add' := , map_smul' := }, map_add' := , map_smul' := }
      Instances For
        theorem LinearMap.BilinForm.dualSubmoduleToDual_injective {R : Type u_3} {S : Type u_1} {M : Type u_2} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) (hB : B.Nondegenerate) [NoZeroSMulDivisors R S] (N : Submodule R M) (hN : Submodule.span S N = ) :
        Function.Injective (B.dualSubmoduleToDual N)
        theorem LinearMap.BilinForm.dualSubmodule_span_of_basis {R : Type u_4} {S : Type u_2} {M : Type u_3} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) {ι : Type u_1} [Finite ι] [DecidableEq ι] (hB : B.Nondegenerate) (b : Basis ι S M) :
        B.dualSubmodule (Submodule.span R (Set.range b)) = Submodule.span R (Set.range (B.dualBasis hB b))
        theorem LinearMap.BilinForm.dualSubmodule_dualSubmodule_flip_of_basis {R : Type u_4} {S : Type u_2} {M : Type u_3} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) {ι : Type u_1} [Finite ι] (hB : B.Nondegenerate) (b : Basis ι S M) :
        B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range b))) = Submodule.span R (Set.range b)
        theorem LinearMap.BilinForm.dualSubmodule_flip_dualSubmodule_of_basis {R : Type u_4} {S : Type u_2} {M : Type u_3} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) {ι : Type u_1} [Finite ι] (hB : B.Nondegenerate) (b : Basis ι S M) :
        B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range b))) = Submodule.span R (Set.range b)
        theorem LinearMap.BilinForm.dualSubmodule_dualSubmodule_of_basis {R : Type u_4} {S : Type u_2} {M : Type u_3} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) {ι : Type u_1} [Finite ι] (hB : B.Nondegenerate) (hB' : B.IsSymm) (b : Basis ι S M) :
        B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range b))) = Submodule.span R (Set.range b)