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.

source
šŸ”ø coverage
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) :
Submodule R M

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

Instances For
    source
    šŸ“ coverage
    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 ā†” āˆ€ y āˆˆ N, (B x) y āˆˆ 1
    source
    šŸ“ coverage
    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ā‚ Nā‚‚ : Submodule R M} :
    Nā‚ ā‰¤ B.flip.dualSubmodule Nā‚‚ ā†” Nā‚‚ ā‰¤ B.dualSubmodule Nā‚
    source
    šŸ”ø coverage
    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.

    Instances For
      source
      šŸ“ coverage
      @[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
      source
      šŸ”ø coverage
      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) [IsDomain R] [Module.IsTorsionFree R S] (N : Submodule R M) :
      ā†„(B.dualSubmodule N) ā†’ā‚—[R] Module.Dual R ā†„N

      The natural paring of B.dualSubmodule N and N.

      Instances For
        source
        šŸ“ coverage
        @[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) [IsDomain R] [Module.IsTorsionFree R S] (N : Submodule R M) (x : ā†„(B.dualSubmodule N)) (y : ā†„N) :
        ((B.dualSubmoduleToDual N) x) y = B.dualSubmoduleParing x y
        source
        šŸ“ coverage
        theorem LinearMap.BilinForm.dualSubmoduleToDual_injective {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) [IsDomain R] (hB : B.Nondegenerate) [Module.IsTorsionFree R S] (N : Submodule R M) (hN : Submodule.span S ā†‘N = āŠ¤) :
        Function.Injective ā‡‘(B.dualSubmoduleToDual N)
        source
        šŸ“ coverage
        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 : Module.Basis Ī¹ S M) :
        B.dualSubmodule (Submodule.span R (Set.range ā‡‘b)) = Submodule.span R (Set.range ā‡‘(B.dualBasis hB b))
        source
        šŸ“ coverage
        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 : Module.Basis Ī¹ S M) :
        B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range ā‡‘b))) = Submodule.span R (Set.range ā‡‘b)
        source
        šŸ“ coverage
        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 : Module.Basis Ī¹ S M) :
        B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ā‡‘b))) = Submodule.span R (Set.range ā‡‘b)
        source
        šŸ“ coverage
        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 : Module.Basis Ī¹ S M) :
        B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ā‡‘b))) = Submodule.span R (Set.range ā‡‘b)