Nyll.ClassFieldTheory.AbstractClassFieldTheory.Degree.PadicCyclicClosure

def

padicCyclicClosure_isOpen_of_degree_ne_one

ClassFormation.padicCyclicClosure_isOpen_of_degree_ne_one

Documentation

A continuous p-adic degree with finite kernel makes the cyclic closure of every element of nonzero degree open.

The degree image of the cyclic closure is compact, hence closed in ℤ_p; it contains a nonzero element, hence is open. Its relative index in the full degree image is therefore finite. The remaining relative-index factor lies in the finite degree kernel.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFormation
noncomputable section
universe u
variable
    {G : Type u} [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] [CompactSpace G]

Lean source · statement

theorem padicCyclicClosure_isOpen_of_degree_ne_one
    (p : ℕ) [Fact p.Prime]
    (degree : G →ₜ* Multiplicative ℤ_[p])
    [Finite degree.toMonoidHom.ker]
    (τ : G)
    (hτ : degree τ ≠ 1) :
    IsOpen ((padicCyclicClosure τ : Subgroup G) : Set G)

theorem

padicCyclicClosure_degree_injective_of_primePower_finiteCoordinate

L200 ↗

ClassFormation.padicCyclicClosure_degree_injective_of_primePower_finiteCoordinate

Documentation

On the cyclic closure of an element whose finite coordinate has p-power order and whose p-adic degree is a positive integer, the p-adic degree is injective.

The proof uses one carefully chosen open neighborhood. If a limit of integral powers has trivial p-adic degree, approximate it by a power whose degree lies in (n * p^m)ℤ_p. Cancellation of the nonzero integer n forces the exponent to be divisible by p^m, so its finite coordinate is trivial as well.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFormation
noncomputable section
universe u
variable
    {G : Type u} [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] [CompactSpace G]
omit [CompactSpace G] in

Lean source · full declaration

theorem padicCyclicClosure_degree_injective_of_primePower_finiteCoordinate
    {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
    (p : ℕ) [Fact p.Prime]
    (finiteCoordinate : G →ₜ* Q)
    (degree : G →ₜ* Multiplicative ℤ_[p])
    (hjoint :
      Function.Injective
        (fun g : G => (finiteCoordinate g, degree g)))
    (γ : G)
    (m n : ℕ)
    (hn : 0 < n)
    (hfinite : (finiteCoordinate γ) ^ (p ^ m) = 1)
    (hdegree :
      degree γ =
        (Multiplicative.ofAdd (1 : ℤ_[p])) ^ n) :
    Function.Injective
      ((degree.toMonoidHom.comp
        (padicCyclicClosure γ).toSubgroup.subtype) :
        padicCyclicClosure γ →
          Multiplicative ℤ_[p]) := by
  let Γ : ClosedSubgroup G :=
    padicCyclicClosure γ
  let inclusion : Γ.toSubgroup →ₜ* G :=
    { toMonoidHom := Γ.toSubgroup.subtype
      continuous_toFun := continuous_subtype_val }
  let restrictedDegree :
      Γ.toSubgroup →ₜ* Multiplicative ℤ_[p] :=
    degree.comp inclusion
  have hkernel :
      ∀ z : Γ.toSubgroup,
        restrictedDegree z = 1 →
          z = 1 := by
    intro z hzdegree
    let c : ℕ :=
      n * p ^ m
    let J : AddSubgroup ℤ_[p] :=
      (Ideal.span ({(c : ℤ_[p])} : Set ℤ_[p])).toAddSubgroup
    have hcne : c ≠ 0 := by
      exact
        Nat.mul_ne_zero (Nat.ne_of_gt hn)
          (pow_ne_zero m (Fact.out : p.Prime).ne_zero)
    have hJrange :
        (J : Set ℤ_[p]) =
          Set.range (fun a : ℤ_[p] => a * (c : ℤ_[p])) := by
      ext x
      constructor
      · intro hx
        change
          x ∈ Ideal.span
            ({(c : ℤ_[p])} : Set ℤ_[p]) at hx
        rw [Ideal.mem_span_singleton] at hx
        obtain ⟨a, rfl⟩ := hx
        exact ⟨a, mul_comm _ _⟩
      · rintro ⟨a, rfl⟩
        change
          a * (c : ℤ_[p]) ∈
            Ideal.span ({(c : ℤ_[p])} : Set ℤ_[p])
        rw [Ideal.mem_span_singleton]
        exact ⟨a, mul_comm _ _⟩
    have hJclosed : IsClosed (J : Set ℤ_[p]) := by
      rw [hJrange]
      exact
        (isCompact_range
          (continuous_id.mul continuous_const)).isClosed
    have hJne : J ≠ ⊥ := by
      intro hbot
      have hcMem : (c : ℤ_[p]) ∈ J := by
        change
          (c : ℤ_[p]) ∈
            Ideal.span ({(c : ℤ_[p])} : Set ℤ_[p])
        exact Ideal.subset_span (by simp)
      rw [hbot] at hcMem
      have hc0 : (c : ℤ_[p]) = 0 := by
        simpa only [AddSubgroup.mem_bot] using hcMem
      have hc0' : c = 0 := by
        exact_mod_cast hc0
      exact hcne hc0'
    have hJopen : IsOpen (J : Set ℤ_[p]) :=
      PadicInt.addSubgroup_isOpen_of_isClosed_of_ne_bot
        p J hJclosed hJne
    let O : Set G :=
      finiteCoordinate ⁻¹' {finiteCoordinate z.1} ∩
        (fun g : G =>
          Multiplicative.toAdd (degree g)) ⁻¹'
            (J : Set ℤ_[p])
    have hOopen : IsOpen O := by
      exact
        ((isOpen_discrete
          ({finiteCoordinate z.1} : Set Q)).preimage
            finiteCoordinate.continuous_toFun).inter
          (hJopen.preimage
            (continuous_toAdd.comp
              degree.continuous_toFun))
    have hzO : z.1 ∈ O := by
      refine ⟨rfl, ?_⟩
      change
        Multiplicative.toAdd (restrictedDegree z) ∈ J
      rw [hzdegree]
      exact J.zero_mem
    have hzclosure :
        z.1 ∈
          closure
            (((Subgroup.closure
              (Set.range (fun _ : Unit => γ))) :
                Subgroup G) :
              Set G) := by
      exact z.2
    obtain ⟨y, hyO, hyGenerated⟩ :=
      mem_closure_iff.mp hzclosure O hOopen hzO
    have hrange :
        Set.range (fun _ : Unit => γ) =
          ({γ} : Set G) := by
      ext x
      constructor
      · rintro ⟨u, rfl⟩
        simp
      · intro hx
        rw [Set.mem_singleton_iff] at hx
        exact ⟨(), hx.symm⟩
    have hyZPowers :
        y ∈ Subgroup.zpowers γ := by
      rw [Subgroup.zpowers_eq_closure, ← hrange]
      exact hyGenerated
    obtain ⟨k, hk⟩ :=
      Subgroup.mem_zpowers_iff.mp hyZPowers
    have hyJ :
        Multiplicative.toAdd (degree y) ∈ J :=
      hyO.2
    have hyJ' :
        (k : ℤ_[p]) * (n : ℤ_[p]) ∈ J := by
      rw [← hk, map_zpow, hdegree] at hyJ
      simpa using hyJ
    change
      (k : ℤ_[p]) * (n : ℤ_[p]) ∈
        Ideal.span ({(c : ℤ_[p])} : Set ℤ_[p]) at hyJ'
    rw [Ideal.mem_span_singleton] at hyJ'
    obtain ⟨a, ha⟩ := hyJ'
    have hnZ : (n : ℤ_[p]) ≠ 0 := by
      exact_mod_cast Nat.ne_of_gt hn
    have hcancel :
        a * (p : ℤ_[p]) ^ m =
          (k : ℤ_[p]) := by
      apply mul_left_cancel₀ hnZ
      calc
        (n : ℤ_[p]) *
            (a * (p : ℤ_[p]) ^ m) =
            a * (c : ℤ_[p]) := by
              simp only [c, Nat.cast_mul, Nat.cast_pow]
              ring
        _ = (k : ℤ_[p]) * (n : ℤ_[p]) := by
          simpa [mul_comm] using ha.symm
        _ = (n : ℤ_[p]) * (k : ℤ_[p]) := mul_comm _ _
    have hkSpan :
        (k : ℤ_[p]) ∈
          Ideal.span
            ({(p : ℤ_[p]) ^ m} : Set ℤ_[p]) := by
      rw [Ideal.mem_span_singleton]
      exact ⟨a, by simpa [mul_comm] using hcancel.symm⟩
    have hkMod :
        PadicInt.toZModPow m (k : ℤ_[p]) = 0 := by
      rw [← PadicInt.ker_toZModPow m,
        RingHom.mem_ker] at hkSpan
      exact hkSpan
    have hkMod' :
        (k : ZMod (p ^ m)) = 0 := by
      simpa only [map_intCast] using hkMod
    have hkdiv :
        ((p ^ m : ℕ) : ℤ) ∣ k :=
      (CharP.intCast_eq_zero_iff
        (ZMod (p ^ m)) (p ^ m) k).1 hkMod'
    obtain ⟨l, hl⟩ := hkdiv
    have hfinitePower :
        finiteCoordinate y = 1 := by
      rw [← hk, map_zpow, hl]
      calc
        finiteCoordinate γ ^
              (((p ^ m : ℕ) : ℤ) * l) =
            (finiteCoordinate γ ^
              ((p ^ m : ℕ) : ℤ)) ^ l := by
                rw [zpow_mul]
        _ = 1 := by
          rw [zpow_natCast, hfinite, one_zpow]
    have hzfinite :
        finiteCoordinate z.1 = 1 := by
      exact hyO.1.symm.trans hfinitePower
    have hzG : z.1 = (1 : G) := by
      apply hjoint
      apply Prod.ext
      · simpa only [map_one] using hzfinite
      · have hzdegree' : degree z.1 = 1 := by
          dsimp [restrictedDegree, inclusion] at hzdegree
          exact hzdegree
        simpa only [map_one] using hzdegree'
    exact Subtype.ext hzG
  intro x y hxy
  have hxy' : restrictedDegree x = restrictedDegree y := by
    change degree (x : G) = degree (y : G)
    change degree (x : G) = degree (y : G) at hxy
    exact hxy
  have hquotient :
      restrictedDegree (x * y⁻¹) = 1 := by
    rw [map_mul, map_inv, hxy', mul_inv_cancel]
  have hunit :
      x * y⁻¹ = 1 :=
    hkernel (x * y⁻¹) hquotient
  exact mul_inv_eq_one.mp hunit

PadicCyclicClosure.lean

Module documentation

Cyclic closures detected by a p-adic degree

padicCyclicClosure

padicCyclicClosureGenerator

padicCyclicClosure_isOpen_of_degree_ne_one

padicCyclicClosure_degree_injective_of_primePower_finiteCoordinate

Module documentation

Cyclic closures detected by a p-adic degree

Declarations

padicCyclicClosure

padicCyclicClosureGenerator

padicCyclicClosure_isOpen_of_degree_ne_one

padicCyclicClosure_degree_injective_of_primePower_finiteCoordinate