Module

TrivialOrientation.lean

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.TrivialOrientation

4 declarations indexed from sourceView source ↗

Module documentation

Fixed-group comparison for the trivial orientation

Imports4

Imported by2

theorem

h1Reduction_trivial_of_no_prime_torsion

L22 ↗

Yamaguchi26AbfaithfulGalois.h1Reduction_trivial_of_no_prime_torsion

Documentation

No prime torsion in the abelianization implies formal H¹ reduction surjectivity for the trivial orientation at the fixed subgroup.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
universe u

Lean source · statement

theorem h1Reduction_trivial_of_no_prime_torsion
    {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (H : Subgroup G) [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hH : ∀ a : TopologicalAbelianization H, a ^ ℓ = 1 → a = 1)
    (n : ℕ) (hn : 1 ≤ n) : HasH1ReductionSurjective (1 : Orientation ℓ G) H n hn

theorem

no_prime_torsion_of_h1Reduction_trivial

L88 ↗

Yamaguchi26AbfaithfulGalois.no_prime_torsion_of_h1Reduction_trivial

Documentation

Formal H¹ reduction surjectivity at a fixed subgroup excludes prime torsion in its actual topological abelianization.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
universe u

Lean source · statement

theorem no_prime_torsion_of_h1Reduction_trivial
    {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (H : Subgroup G) [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hH : ∀ n : ℕ, ∀ hn : 1 ≤ n, HasH1ReductionSurjective (1 : Orientation ℓ G) H n hn)
    (a : TopologicalAbelianization H) (ha : a ^ ℓ = 1) : a = 1

theorem

exists_padic_character_detecting_primary_of_h1_trivial

L144 ↗

Yamaguchi26AbfaithfulGalois.exists_padic_character_detecting_primary_of_h1_trivial

Documentation

Under trivial-orientation lifting, p-adic characters separate every primary class.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
universe u

Lean source · statement

theorem exists_padic_character_detecting_primary_of_h1_trivial
    {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (H : Subgroup G) [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hH : ∀ n : ℕ, ∀ hn : 1 ≤ n, HasH1ReductionSurjective (1 : Orientation ℓ G) H n hn)
    (a : PrimaryAbelianization ℓ H) (ha : a ≠ 1) :
    ∃ f : PrimaryAbelianization ℓ H →ₜ* Multiplicative (PadicInt ℓ), f a ≠ 1

theorem

primaryAbelianization_isMulTorsionFree_of_h1_trivial

L197 ↗

Yamaguchi26AbfaithfulGalois.primaryAbelianization_isMulTorsionFree_of_h1_trivial

Documentation

The primary abelianization is torsion-free under fixed-group trivial-orientation lifting.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
universe u

Lean source · statement

theorem primaryAbelianization_isMulTorsionFree_of_h1_trivial
    {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (H : Subgroup G) [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hH : ∀ n : ℕ, ∀ hn : 1 ≤ n, HasH1ReductionSurjective (1 : Orientation ℓ G) H n hn) :
    IsMulTorsionFree (PrimaryAbelianization ℓ H)

Module documentation

Fixed-group comparison for the trivial orientation

Declarations

h1Reduction_trivial_of_no_prime_torsion

no_prime_torsion_of_h1Reduction_trivial

exists_padic_character_detecting_primary_of_h1_trivial

primaryAbelianization_isMulTorsionFree_of_h1_trivial