Module

FiniteCocycleOperations.lean

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.FiniteCocycleOperations

5 declarations indexed from sourceView source ↗

Module documentation

Arithmetic operations on finite oriented cocycles

Imports2

Imported by2

def

reduce

L21 ↗

Yamaguchi26AbfaithfulGalois.FiniteCocycle.reduce

Documentation

Reduce the coefficient values of a finite oriented cocycle to a smaller prime-power quotient.

Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois.FiniteCocycle
universe u
variable {ℓ : ℕ} [Fact ℓ.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {θ : Orientation ℓ G} {H : Subgroup G}

Lean source · full declaration

def reduce {m n : ℕ} (c : FiniteCocycle θ H n) (hmn : m ≤ n) :
    FiniteCocycle θ H m where
  toFun := fun x => ZMod.castHom (pow_dvd_pow ℓ hmn) (ZMod (ℓ ^ m)) (c.toFun x)
  continuous_toFun := continuous_of_discreteTopology.comp c.continuous_toFun
  cocycle := by
    intro x y
    rw [c.cocycle, map_add, map_mul]
    congr 1
    congr 1
    exact RingHom.congr_fun (PadicInt.zmod_cast_comp_toZModPow m n hmn)
      (θ (x : G) : PadicInt ℓ)

def

add

L34 ↗

Yamaguchi26AbfaithfulGalois.FiniteCocycle.add

Documentation

The pointwise sum of two finite oriented cocycles.

Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois.FiniteCocycle
universe u
variable {ℓ : ℕ} [Fact ℓ.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {θ : Orientation ℓ G} {H : Subgroup G}

Lean source · full declaration

def add {n : ℕ} (c d : FiniteCocycle θ H n) : FiniteCocycle θ H n where
  toFun := fun x => c.toFun x + d.toFun x
  continuous_toFun := c.continuous_toFun.add d.continuous_toFun
  cocycle := by
    intro x y
    rw [c.cocycle, d.cocycle, mul_add]
    abel

def

sub

L43 ↗

Yamaguchi26AbfaithfulGalois.FiniteCocycle.sub

Documentation

The pointwise difference of two finite oriented cocycles.

Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois.FiniteCocycle
universe u
variable {ℓ : ℕ} [Fact ℓ.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {θ : Orientation ℓ G} {H : Subgroup G}

Lean source · full declaration

def sub {n : ℕ} (c d : FiniteCocycle θ H n) : FiniteCocycle θ H n where
  toFun := fun x => c.toFun x - d.toFun x
  continuous_toFun := c.continuous_toFun.sub d.continuous_toFun
  cocycle := by
    intro x y
    rw [c.cocycle, d.cocycle, mul_sub]
    abel

def

mulPrime

L52 ↗

Yamaguchi26AbfaithfulGalois.FiniteCocycle.mulPrime

Documentation

The coefficient embedding induced by multiplication by ℓ.

Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois.FiniteCocycle
universe u
variable {ℓ : ℕ} [Fact ℓ.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {θ : Orientation ℓ G} {H : Subgroup G}

Lean source · full declaration

def mulPrime {n : ℕ} (c : FiniteCocycle θ H n) : FiniteCocycle θ H (n + 1) where
  toFun := fun x => ZMod.mulPow ℓ n (c.toFun x)
  continuous_toFun := continuous_of_discreteTopology.comp c.continuous_toFun
  cocycle := by
    intro x y
    rw [c.cocycle, map_add]
    congr 1
    have hc := RingHom.congr_fun (PadicInt.zmod_cast_comp_toZModPow n (n + 1)
      (Nat.le_succ n)) (θ (x : G) : PadicInt ℓ)
    change ZMod.castHom (pow_dvd_pow ℓ (Nat.le_succ n)) (ZMod (ℓ ^ n))
      (PadicInt.toZModPow (n + 1) (θ (x : G) : PadicInt ℓ)) = _ at hc
    rw [← hc, ZMod.mulPow_mul_castHom]

theorem

exists_divPrime

L66 ↗

Yamaguchi26AbfaithfulGalois.FiniteCocycle.exists_divPrime

Documentation

A cocycle that is zero modulo ℓ divides uniquely by ℓ.

Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois.FiniteCocycle
universe u
variable {ℓ : ℕ} [Fact ℓ.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {θ : Orientation ℓ G} {H : Subgroup G}

Lean source · statement

theorem exists_divPrime {n : ℕ} (c : FiniteCocycle θ H (n + 1))
    (hc : ∀ x : H, ZMod.castHom (pow_dvd_pow ℓ (Nat.succ_le_succ (Nat.zero_le n)))
      (ZMod (ℓ ^ 1)) (c.toFun x) = 0) :
    ∃ d : FiniteCocycle θ H n, ∀ x : H, ZMod.mulPow ℓ n (d.toFun x) = c.toFun x

Module documentation

Arithmetic operations on finite oriented cocycles

Declarations

reduce

add

sub

mulPrime

exists_divPrime