Module

Theorem3Dot3FiniteOrderModP.lean

Nyll.Yamaguchi26AbfaithfulGalois.Theorem3Dot3FiniteOrderModP

4 declarations indexed from sourceView source ↗

Module documentation

Lemma 3.3: finite-order automorphisms trivial modulo an odd prime

Source: Yamaguchi, arXiv:2610.05634v1, Lemma 3.3. The separation hypothesis is stated elementwise; no finite generation is assumed.

Imports5

Nyll.ValuedFieldTheory.LocalField.Analytic.AugmentationDivisibility
Nyll.ValuedFieldTheory.LocalField.Analytic.PrimeOrderDivisibility
Mathlib.NumberTheory.Padics.PadicIntegers
Mathlib.Algebra.Module.Torsion.Free
Mathlib.GroupTheory.OrderOfElement

Imported by1

Nyll.Yamaguchi26AbfaithfulGalois.All

theorem

pow_action_sub_divisible

L25 ↗

Yamaguchi26AbfaithfulGalois.pow_action_sub_divisible

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open LocalFieldTheory.DiscreteValuationField
universe u

Lean source · statement

theorem pow_action_sub_divisible
    {p : ℕ} [Fact p.Prime] {M : Type u} [AddCommGroup M] [Module ℤ_[p] M]
    (T : M ≃ₗ[ℤ_[p]] M)
    (hT : ∀ x : M, ∃ y : M, T x - x = (p : ℤ_[p]) • y) :
    ∀ n : ℕ, ∀ x : M, ∃ y : M, (T ^ n) x - x = (p : ℤ_[p]) • y

theorem

divisible_subgroup_eq_bot

L44 ↗

Yamaguchi26AbfaithfulGalois.divisible_subgroup_eq_bot

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open LocalFieldTheory.DiscreteValuationField
universe u

Lean source · statement

theorem divisible_subgroup_eq_bot
    {p : ℕ} [Fact p.Prime] {M : Type u} [AddCommGroup M] [Module ℤ_[p] M]
    (hsep : ∀ x : M, (∀ n : ℕ, 0 < n → ∃ y : M, (p : ℤ_[p]) ^ n • y = x) → x = 0)
    (J : AddSubgroup M)
    (hJ : ∀ x : M, x ∈ J → ∃ y : M, y ∈ J ∧ (p : ℤ_[p]) • y = x) : J = ⊥

theorem

prime_order_mod_p_eq_one

L63 ↗

Yamaguchi26AbfaithfulGalois.prime_order_mod_p_eq_one

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open LocalFieldTheory.DiscreteValuationField
universe u

Lean source · statement

theorem prime_order_mod_p_eq_one
    {p : ℕ} [Fact p.Prime] (hp2 : p ≠ 2)
    {M : Type u} [AddCommGroup M] [Module ℤ_[p] M] [Module.IsTorsionFree ℤ_[p] M]
    (hsep : ∀ x : M, (∀ n : ℕ, 0 < n → ∃ y : M, (p : ℤ_[p]) ^ n • y = x) → x = 0)
    (T : M ≃ₗ[ℤ_[p]] M) (q : ℕ) (hq : q.Prime) (horder : orderOf T = q)
    (hdiv : ∀ x : M, ∃ y : M, T x - x = (p : ℤ_[p]) • y) : T = 1

theorem

finite_order_mod_p_3_3

L133 ↗

Yamaguchi26AbfaithfulGalois.finite_order_mod_p_3_3

Documentation

A finite-order automorphism of a separated torsion-free ℤ_p-module which acts trivially modulo the odd prime p is the identity.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open LocalFieldTheory.DiscreteValuationField
universe u

Lean source · statement

theorem finite_order_mod_p_3_3
    {p : ℕ} [Fact p.Prime] (hp2 : p ≠ 2)
    {M : Type u} [AddCommGroup M] [Module ℤ_[p] M] [Module.IsTorsionFree ℤ_[p] M]
    (hsep : ∀ x : M, (∀ n : ℕ, 0 < n → ∃ y : M, (p : ℤ_[p]) ^ n • y = x) → x = 0)
    (T : M ≃ₗ[ℤ_[p]] M) (hfinite : IsOfFinOrder T)
    (hdiv : ∀ x : M, ∃ y : M, T x - x = (p : ℤ_[p]) • y) : T = 1

Module documentation

Lemma 3.3: finite-order automorphisms trivial modulo an odd prime

Declarations

pow_action_sub_divisible

divisible_subgroup_eq_bot

prime_order_mod_p_eq_one

finite_order_mod_p_3_3