p-adic Pontryagin duals

AbbreviationThe quotient \(\mathbb{Q}_p/\mathbb{Z}_p\)#✓fully proved

For a prime \(p\), \(\mathbb{Q}_p/\mathbb{Z}_p\) is the quotient of \(\mathbb{Q}_p\), viewed as a \(\mathbb{Z}_p\)-module, by the image of \(\mathbb{Z}_p\) under the canonical inclusion \(\mathbb{Z}_p \to \mathbb{Q}_p\).

noncomputable abbrev PadicQuotientInt (p : ℕ) [Fact p.Prime] :=
  ℚ_[p] ⧸ LinearMap.range (Algebra.linearMap ℤ_[p] ℚ_[p])

Used by 7

Used byContragredient action on the \(p\)-adic Pontryagin dual · Algebraic \(p\)-adic Pontryagin dual · Extensionality for the \(p\)-adic Pontryagin dual · The quotient map \(\mathbb{Q}_p \to \mathbb{Q}_p/\mathbb{Z}_p\) · The quotient map vanishes on \(\mathbb{Z}_p\) · The quotient map is the quotient projection · Evaluating the contragredient action

AbbreviationAlgebraic \(p\)-adic Pontryagin dual#✓fully proved

For a prime \(p\) and a \(\mathbb{Z}_p\)-module \(A\), the algebraic \(p\)-adic Pontryagin dual of \(A\) is the \(\mathbb{Z}_p\)-module \(\operatorname{Hom}_{\mathbb{Z}_p}(A, \mathbb{Q}_p/\mathbb{Z}_p)\) of all \(\mathbb{Z}_p\)-linear maps from \(A\) to \(\mathbb{Q}_p/\mathbb{Z}_p\); no topology or continuity condition is imposed.

noncomputable abbrev PadicPontryaginDual (p : ℕ) [Fact p.Prime]
    (A : Type*) [AddCommGroup A] [Module ℤ_[p] A] :=
  A →ₗ[ℤ_[p]] PadicQuotientInt p

Uses 1 · Used by 3

Statement usesThe quotient \(\mathbb{Q}_p/\mathbb{Z}_p\)

Used byContragredient action on the \(p\)-adic Pontryagin dual · Extensionality for the \(p\)-adic Pontryagin dual · Evaluating the contragredient action

TheoremExtensionality for the \(p\)-adic Pontryagin dual#✓fully proved

Let \(p\) be a prime and \(A\) a \(\mathbb{Z}_p\)-module. If two elements \(\varphi, \psi\) of the algebraic \(p\)-adic Pontryagin dual of \(A\) satisfy \(\varphi(a) = \psi(a)\) for every \(a \in A\), then \(\varphi = \psi\).

@[ext]
theorem PadicPontryaginDual_ext {p : ℕ} [Fact p.Prime]
    {A : Type*} [AddCommGroup A] [Module ℤ_[p] A]
    {φ ψ : PadicPontryaginDual p A} (h : ∀ a, φ a = ψ a) : φ = ψ

Uses 2 · Used by 1

Statement usesAlgebraic \(p\)-adic Pontryagin dual · The quotient \(\mathbb{Q}_p/\mathbb{Z}_p\)

Used byEvaluating the contragredient action

DefinitionThe quotient map \(\mathbb{Q}_p \to \mathbb{Q}_p/\mathbb{Z}_p\)#✓fully proved

For a prime \(p\), this is the canonical projection \(\mathbb{Q}_p \to \mathbb{Q}_p/\mathbb{Z}_p\), \(x \mapsto x + \mathbb{Z}_p\), as a \(\mathbb{Z}_p\)-linear map.

noncomputable def padicQuotientMap (p : ℕ) [Fact p.Prime] :
    ℚ_[p] →ₗ[ℤ_[p]] PadicQuotientInt p :=
  (LinearMap.range (Algebra.linearMap ℤ_[p] ℚ_[p])).mkQ

Uses 1 · Used by 2

Statement usesThe quotient \(\mathbb{Q}_p/\mathbb{Z}_p\)

Used byThe quotient map vanishes on \(\mathbb{Z}_p\) · The quotient map is the quotient projection

TheoremThe quotient map vanishes on \(\mathbb{Z}_p\)#✓fully proved

For a prime \(p\) and every \(z \in \mathbb{Z}_p\), the quotient map \(\mathbb{Q}_p \to \mathbb{Q}_p/\mathbb{Z}_p\) sends the image of \(z\) in \(\mathbb{Q}_p\) to \(0\).

theorem padicQuotientMap_algebraMap_eq_zero (p : ℕ) [Fact p.Prime] (z : ℤ_[p]) :
    padicQuotientMap p (algebraMap ℤ_[p] ℚ_[p] z) = 0

Uses 2

Statement usesThe quotient \(\mathbb{Q}_p/\mathbb{Z}_p\) · The quotient map \(\mathbb{Q}_p \to \mathbb{Q}_p/\mathbb{Z}_p\)

TheoremThe quotient map is the quotient projection#✓fully proved

For a prime \(p\) and every \(x \in \mathbb{Q}_p\), the quotient map \(\mathbb{Q}_p \to \mathbb{Q}_p/\mathbb{Z}_p\) sends \(x\) to its class \(x + \mathbb{Z}_p\) in the quotient module.

theorem padicQuotientMap_mkQ_eq (p : ℕ) [Fact p.Prime] (x : ℚ_[p]) :
    padicQuotientMap p x = Submodule.Quotient.mk x

Uses 2

Statement usesThe quotient \(\mathbb{Q}_p/\mathbb{Z}_p\) · The quotient map \(\mathbb{Q}_p \to \mathbb{Q}_p/\mathbb{Z}_p\)

DefinitionContragredient action on the \(p\)-adic Pontryagin dual#✓fully proved

Let \(p\) be a prime, \(G\) a group and \(A\) a \(\mathbb{Z}_p\)-module on which \(G\) acts by additive maps commuting with the \(\mathbb{Z}_p\)-action. For \(g \in G\) and \(\varphi\) in the algebraic \(p\)-adic Pontryagin dual of \(A\), \(g \cdot \varphi\) is the element \(a \mapsto \varphi(g^{-1} a)\) of the dual.

noncomputable def contragredientSMul (p : ℕ) [Fact p.Prime] (G A : Type*) [Group G]
    [AddCommGroup A] [Module ℤ_[p] A] [DistribMulAction G A] [SMulCommClass G ℤ_[p] A]
    (g : G) (φ : PadicPontryaginDual p A) : PadicPontryaginDual p A where
  toFun a := φ (g⁻¹ • a)
  map_add' a b := by
    simp [smul_add, map_add]
  map_smul' r a := by
    change φ (g⁻¹ • (r • a)) = (RingHom.id ℤ_[p] r) • φ (g⁻¹ • a)
    rw [smul_comm g⁻¹ r a]
    simpa only [RingHom.id_apply] using φ.map_smul r (g⁻¹ • a)

Uses 2 · Used by 1

Statement usesAlgebraic \(p\)-adic Pontryagin dual · The quotient \(\mathbb{Q}_p/\mathbb{Z}_p\)

Used byEvaluating the contragredient action

TheoremEvaluating the contragredient action#✓fully proved

Let \(p\) be a prime, \(G\) a group and \(A\) a \(\mathbb{Z}_p\)-module on which \(G\) acts by additive maps commuting with the \(\mathbb{Z}_p\)-action. For \(g \in G\), \(\varphi\) in the algebraic \(p\)-adic Pontryagin dual of \(A\) and \(a \in A\), the contragredient action satisfies \((g \cdot \varphi)(a) = \varphi(g^{-1} a)\).

@[simp]
theorem smul_apply (p : ℕ) [Fact p.Prime] (G A : Type*) [Group G]
    [AddCommGroup A] [Module ℤ_[p] A] [DistribMulAction G A] [SMulCommClass G ℤ_[p] A]
    (g : G) (φ : PadicPontryaginDual p A) (a : A) :
    (g • φ) a = φ (g⁻¹ • a)

Uses 4

Statement usesAlgebraic \(p\)-adic Pontryagin dual · Extensionality for the \(p\)-adic Pontryagin dual · The quotient \(\mathbb{Q}_p/\mathbb{Z}_p\) · Contragredient action on the \(p\)-adic Pontryagin dual

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.