Dual lattices

TheoremA spanning submodule localizes to the whole space#✓fully proved

Let \(A\) be a commutative ring with fraction field \(K\), let \(V\) be a \(K\)-vector space, viewed as an \(A\)-module through \(A \to K\), and let \(M\) be an \(A\)-submodule of \(V\) that spans \(V\) over \(K\). Then \(V\), together with the inclusion \(M \hookrightarrow V\), is the localization of the \(A\)-module \(M\) at the non-zero-divisors of \(A\).

Concretely, every non-zero-divisor \(s\) of \(A\) acts bijectively on \(V\), and every \(v \in V\) satisfies \(s v \in M\) for some non-zero-divisor \(s\) of \(A\).

theorem Submodule.isLocalizedModule_subtype_of_span_eq_top (M : Submodule A V)
    (hspan : Submodule.span K (M : Set V) = ⊤) :
    IsLocalizedModule (A⁰) M.subtype

Used by 1

Used bySurjectivity of the dual pairing

TheoremSurjectivity of the dual pairing#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\), let \(V\) be a finite-dimensional \(K\)-vector space, viewed as an \(A\)-module through \(A \subseteq K\), let \(B\) be a nondegenerate bilinear form on \(V\), and let \(M\) be an \(A\)-submodule of \(V\) that spans \(V\) over \(K\). Then the map from \(M^\vee = \{x \in V : B(x, y) \in A \text{ for all } y \in M\}\) to \(\operatorname{Hom}_A(M, A)\) sending \(x\) to the functional \(y \mapsto B(x, y)\) is surjective.

theorem LinearMap.BilinForm.dualSubmoduleToDual_surjective [IsDomain A]
    [FiniteDimensional K V]
    (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (M : Submodule A V)
    (hspan : Submodule.span K (M : Set V) = ⊤) :
    Function.Surjective (B.dualSubmoduleToDual M)

Uses 1 · Used by 1

Proof usesA spanning submodule localizes to the whole space

Used byBijectivity of the dual pairing

TheoremBijectivity of the dual pairing#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\), let \(V\) be a finite-dimensional \(K\)-vector space, viewed as an \(A\)-module through \(A \subseteq K\), let \(B\) be a nondegenerate bilinear form on \(V\), and let \(M\) be an \(A\)-submodule of \(V\) that spans \(V\) over \(K\). Then the map from \(M^\vee = \{x \in V : B(x, y) \in A \text{ for all } y \in M\}\) to \(\operatorname{Hom}_A(M, A)\) sending \(x\) to the functional \(y \mapsto B(x, y)\) is bijective.

theorem LinearMap.BilinForm.dualSubmoduleToDual_bijective [IsDomain A]
    [FiniteDimensional K V]
    (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (M : Submodule A V)
    (hspan : Submodule.span K (M : Set V) = ⊤) :
    Function.Bijective (B.dualSubmoduleToDual M)

Uses 1 · Used by 2

Proof usesSurjectivity of the dual pairing

Used byThe dual lattice and the dual module · The dual submodule is the dual module

TheoremThe dual of a lattice is finitely generated#✓fully proved

Let \(A\) be a Noetherian integral domain with fraction field \(K\), let \(V\) be a \(K\)-vector space, viewed as an \(A\)-module through \(A \subseteq K\), and let \(B\) be a nondegenerate bilinear form on \(V\). Let \(M\) be a finitely generated \(A\)-submodule of \(V\) that spans \(V\) over \(K\). Then the dual submodule \(M^\vee = \{x \in V : B(x, y) \in A \text{ for all } y \in M\}\) is a finitely generated \(A\)-submodule of \(V\).

theorem LinearMap.BilinForm.dualSubmodule_fg [IsDomain A] [IsNoetherianRing A]
    (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (M : Submodule A V)
    [Module.Finite A M]
    (hspan : Submodule.span K (M : Set V) = ⊤) :
    (B.dualSubmodule M).FG

Used by 1

Used byThe dual of a lattice is a lattice

TheoremThe dual of a finitely generated submodule spans#✓fully proved

Let \(A\) be a commutative ring with fraction field \(K\), let \(V\) be a \(K\)-vector space, viewed as an \(A\)-module through \(A \to K\), and let \(B\) be a bilinear form on \(V\). If \(M\) is a finitely generated \(A\)-submodule of \(V\), then its dual submodule \(M^\vee = \{x \in V : B(x, y) \in A \text{ for all } y \in M\}\) spans \(V\) over \(K\).

theorem LinearMap.BilinForm.dualSubmodule_span_eq_top
    (B : LinearMap.BilinForm K V) (M : Submodule A V) (hfg : M.FG) :
    Submodule.span K (B.dualSubmodule M : Set V) = ⊤

Used by 2

Used byDouble dual of a reflexive lattice · The dual of a lattice is a lattice

TheoremThe dual of a lattice is a lattice#✓fully proved

Let \(A\) be a Noetherian integral domain with fraction field \(K\), let \(V\) be a \(K\)-vector space, viewed as an \(A\)-module through \(A \subseteq K\), and let \(B\) be a nondegenerate bilinear form on \(V\). If \(M\) is an \(A\)-lattice in \(V\), that is, a finitely generated \(A\)-submodule that spans \(V\) over \(K\), then so is its dual submodule \(M^\vee = \{x \in V : B(x, y) \in A \text{ for all } y \in M\}\).

theorem LinearMap.BilinForm.dualSubmodule_isLattice [IsDomain A] [IsNoetherianRing A]
    (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (M : Submodule A V)
    [Submodule.IsLattice K M] : Submodule.IsLattice K (B.dualSubmodule M)

Uses 2 · Used by 1

Proof usesThe dual of a lattice is finitely generated · The dual of a finitely generated submodule spans

Used byThe dual lattice and the dual module

TheoremThe dual lattice and the dual module#✓fully proved

Let \(A\) be a Noetherian integral domain with fraction field \(K\), let \(V\) be a finite-dimensional \(K\)-vector space, viewed as an \(A\)-module through \(A \subseteq K\), and let \(B\) be a nondegenerate bilinear form on \(V\). Let \(M\) be an \(A\)-lattice in \(V\), that is, a finitely generated \(A\)-submodule that spans \(V\) over \(K\), and let \(M^\vee = \{x \in V : B(x, y) \in A \text{ for all } y \in M\}\). Then \(M^\vee\) is an \(A\)-lattice in \(V\), and the map \(M^\vee \to \operatorname{Hom}_A(M, A)\) sending \(x\) to the functional \(y \mapsto B(x, y)\) is bijective.

theorem LinearMap.BilinForm.dualSubmodule_isLattice_and_dualSubmoduleToDual_bijective
    [IsDomain A] [FiniteDimensional K V] [IsNoetherianRing A]
    (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (M : Submodule A V)
    [Submodule.IsLattice K M] :
    Submodule.IsLattice K (B.dualSubmodule M) ∧
      Function.Bijective (B.dualSubmoduleToDual M)

Uses 2

Proof usesBijectivity of the dual pairing · The dual of a lattice is a lattice

DefinitionThe dual submodule is the dual module#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\), let \(V\) be a finite-dimensional \(K\)-vector space, viewed as an \(A\)-module through \(A \subseteq K\), let \(B\) be a nondegenerate bilinear form on \(V\), and let \(M\) be an \(A\)-submodule of \(V\) that spans \(V\) over \(K\). Write \(M^\vee = \{x \in V : B(x, y) \in A \text{ for all } y \in M\}\). This is the isomorphism of \(A\)-modules \(M^\vee \cong \operatorname{Hom}_A(M, A)\) that sends \(x\) to the functional \(y \mapsto B(x, y)\).

noncomputable def LinearMap.BilinForm.dualSubmoduleLinearEquiv
    [IsDomain A] [FiniteDimensional K V]
    (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (M : Submodule A V)
    (hspan : Submodule.span K (M : Set V) = ⊤) :
    (B.dualSubmodule M) ≃ₗ[A] Module.Dual A M :=
  LinearEquiv.ofBijective (B.dualSubmoduleToDual M)
    (B.dualSubmoduleToDual_bijective hB M hspan)

Uses 1 · Used by 1

Statement usesBijectivity of the dual pairing

Used byDouble dual of a reflexive lattice

TheoremDouble dual of a reflexive lattice#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\), let \(V\) be a finite-dimensional \(K\)-vector space, viewed as an \(A\)-module through \(A \subseteq K\), and let \(B\) be a nondegenerate bilinear form on \(V\). Let \(M\) be an \(A\)-lattice in \(V\), that is, a finitely generated \(A\)-submodule that spans \(V\) over \(K\), and suppose that \(M\) is reflexive as an \(A\)-module. Let \(M^\vee = \{x \in V : B(x, y) \in A \text{ for all } y \in M\}\). Then \(\{x \in V : B(y, x) \in A \text{ for all } y \in M^\vee\} = M\).

This is the lattice analogue of the corresponding statement for the \(A\)-span of a \(K\)-basis of \(V\): no basis is needed when \(M\) is reflexive as an \(A\)-module.

theorem LinearMap.BilinForm.dualSubmodule_flip_dualSubmodule_of_isLattice
    [FiniteDimensional K V] [IsDomain A]
    (B : BilinForm K V) (hB : B.Nondegenerate) (M : Submodule A V)
    [Submodule.IsLattice K M] [Module.IsReflexive A M] :
    B.flip.dualSubmodule (B.dualSubmodule M) = M

Uses 2 · Used by 1

Proof usesThe dual submodule is the dual module · The dual of a finitely generated submodule spans

Used byDouble dual of a lattice over a Dedekind domain

TheoremDouble dual of a lattice over a Dedekind domain#✓fully proved

Let \(A\) be a Dedekind domain with fraction field \(K\), let \(V\) be a finite-dimensional \(K\)-vector space, viewed as an \(A\)-module through \(A \subseteq K\), and let \(B\) be a nondegenerate symmetric bilinear form on \(V\). For an \(A\)-submodule \(N\) of \(V\) write \(N^\vee = \{x \in V : B(x, y) \in A \text{ for all } y \in N\}\). If \(M\) is an \(A\)-lattice in \(V\), that is, a finitely generated \(A\)-submodule that spans \(V\) over \(K\), then \((M^\vee)^\vee = M\).

No reflexivity hypothesis on \(M\) is needed: over a Dedekind domain a finitely generated torsion-free module is flat, hence projective, hence reflexive.

theorem LinearMap.BilinForm.dualSubmodule_dualSubmodule_of_isLattice
    [FiniteDimensional K V] [IsDedekindDomain A]
    (B : BilinForm K V) (hB : B.Nondegenerate) (hBsymm : B.IsSymm)
    (M : Submodule A V) [Submodule.IsLattice K M] :
    B.dualSubmodule (B.dualSubmodule M) = M

Sources

• ATLAS NumberTheoryI, Proposition 5.16.

Uses 1

Proof usesDouble dual of a reflexive lattice

TheoremDual submodules commute with localization#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\), let \(V\) be a \(K\)-vector space that is also an \(A\)-module compatibly with \(A \to K\), and let \(B\) be a \(K\)-bilinear form on \(V\). For a subring \(R \subseteq K\) and an \(R\)-submodule \(N\) of \(V\), write \(N^\vee_R = \{x \in V : B(x, y) \in R \text{ for all } y \in N\}\) for the dual of \(N\) over \(R\). Let \(S\) be a submonoid of \(A\) consisting of non-zero-divisors, and let \(A_S = \{a/s : a \in A,\ s \in S\} \subseteq K\) be the localization of \(A\) at \(S\). Then for every finitely generated \(A\)-submodule \(M\) of \(V\), the dual over \(A_S\) of the \(A_S\)-span of \(M\) equals the \(A_S\)-span of the dual \(M^\vee_A\) of \(M\) over \(A\).

theorem dualSubmodule_span_localization (M : Submodule A V) (hM : M.FG) :
    let Aₛ := Localization.subalgebra.ofField K S hS
    B.dualSubmodule (Submodule.span Aₛ (M : Set V)) =
      Submodule.span Aₛ (B.dualSubmodule M : Set V)

Used by 1

Used byThe trace dual commutes with localization

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.