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.

Equations
    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.

      Equations
        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.

          Equations
            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)