Module

PadicCharacters.lean

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.PadicCharacters

7 declarations indexed from sourceView source ↗

Module documentation

Detecting primary abelianization by p-adic characters

Imports4

Imported by5

theorem

map_one

L27 ↗

Yamaguchi26AbfaithfulGalois.PadicCocycle.map_one

Source context 6 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
universe u
namespace PadicCocycle
variable {ℓ : ℕ} [Fact ℓ.Prime]
  {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  {θ : Orientation ℓ G} {U : Subgroup G}
omit [IsTopologicalGroup G] in

Lean source · statement

theorem map_one (c : PadicCocycle θ U) : c.toFun 1 = 0

theorem

map_conj

L33 ↗

Yamaguchi26AbfaithfulGalois.PadicCocycle.map_conj

Source context 6 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
universe u
namespace PadicCocycle
variable {ℓ : ℕ} [Fact ℓ.Prime]
  {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  {θ : Orientation ℓ G} {U : Subgroup G}
omit [IsTopologicalGroup G] in

Lean source · statement

theorem map_conj (c : PadicCocycle θ U) (u d : U) (hd : θ (d : G) = 1) :
    c.toFun (u * d * u⁻¹) = (θ (u : G) : PadicInt ℓ) * c.toFun d

def

restrictCharacter

L42 ↗

Yamaguchi26AbfaithfulGalois.PadicCocycle.restrictCharacter

Documentation

Restriction to an orientation-trivial subgroup is a continuous character.

Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
universe u
namespace PadicCocycle
variable {ℓ : ℕ} [Fact ℓ.Prime]
  {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  {θ : Orientation ℓ G} {U : Subgroup G}

Lean source · full declaration

def restrictCharacter (D : Subgroup G) (hDθ : D ≤ θ.toMonoidHom.ker)
    (hDU : D ≤ U) (c : PadicCocycle θ U) : D →ₜ* Multiplicative (PadicInt ℓ) where
  toFun d := Multiplicative.ofAdd (c.toFun (Subgroup.inclusion hDU d))
  map_one' := c.map_one
  map_mul' d e := by
    change c.toFun (Subgroup.inclusion hDU (d * e)) =
      c.toFun (Subgroup.inclusion hDU d) + c.toFun (Subgroup.inclusion hDU e)
    rw [_root_.map_mul, c.cocycle]
    rw [show θ ((Subgroup.inclusion hDU d : U) : G) = 1 from hDθ d.2,
      Units.val_one, one_mul]
  continuous_toFun := c.continuous_toFun.comp
    (continuous_subtype_val.subtype_mk fun d => hDU d.2)

def

primaryCharacter

L56 ↗

Yamaguchi26AbfaithfulGalois.PadicCocycle.primaryCharacter

Documentation

The p-adic character on the primary abelianization of the orientation kernel.

Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
universe u
namespace PadicCocycle
variable {ℓ : ℕ} [Fact ℓ.Prime]
  {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  {θ : Orientation ℓ G} {U : Subgroup G}

Lean source · statement

def primaryCharacter [CompactSpace G]
    (D : Subgroup G) (hDclosed : IsClosed (D : Set G))
    (hDθ : D ≤ θ.toMonoidHom.ker) (hDU : D ≤ U) (c : PadicCocycle θ U) :
    PrimaryAbelianization ℓ D →ₜ* Multiplicative (PadicInt ℓ)

theorem

primaryCharacter_mk

L64 ↗

Yamaguchi26AbfaithfulGalois.PadicCocycle.primaryCharacter_mk

Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
universe u
namespace PadicCocycle
variable {ℓ : ℕ} [Fact ℓ.Prime]
  {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  {θ : Orientation ℓ G} {U : Subgroup G}

Lean source · statement

theorem primaryCharacter_mk [CompactSpace G]
    (D : Subgroup G) (hDclosed : IsClosed (D : Set G))
    (hDθ : D ≤ θ.toMonoidHom.ker) (hDU : D ≤ U) (c : PadicCocycle θ U) (d : D) :
    (c.primaryCharacter D hDclosed hDθ hDU
      (QuotientGroup.mk' _ (TopologicalAbelianization.mk D d))).toAdd =
        c.toFun (Subgroup.inclusion hDU d)

theorem

primaryCharacter_conj

L71 ↗

Yamaguchi26AbfaithfulGalois.PadicCocycle.primaryCharacter_conj

Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
universe u
namespace PadicCocycle
variable {ℓ : ℕ} [Fact ℓ.Prime]
  {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  {θ : Orientation ℓ G} {U : Subgroup G}

Lean source · statement

theorem primaryCharacter_conj [CompactSpace G]
    (D : Subgroup G) [D.Normal] (hDclosed : IsClosed (D : Set G))
    (hDθ : D ≤ θ.toMonoidHom.ker) (hDU : D ≤ U) (c : PadicCocycle θ U)
    (u : U) (a : PrimaryAbelianization ℓ D) :
    (c.primaryCharacter D hDclosed hDθ hDU
      (primaryConjugationMap ℓ D hDclosed (u : G) a)).toAdd =
        (θ (u : G) : PadicInt ℓ) *
          (c.primaryCharacter D hDclosed hDθ hDU a).toAdd

theorem

exists_padicCocycle_detecting_primary

L89 ↗

Yamaguchi26AbfaithfulGalois.exists_padicCocycle_detecting_primary

Documentation

Every nonidentity primary class is detected by a p-adic cocycle on an open normal supergroup of the orientation kernel.

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_padicCocycle_detecting_primary
    {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (D : Subgroup G) [D.Normal] (hDclosed : IsClosed (D : Set G))
    (θ : Orientation ℓ G) (hDθ : D ≤ θ.toMonoidHom.ker)
    (hLift : RelativeFormalHilbert90 D θ)
    (a : PrimaryAbelianization ℓ D) (ha : a ≠ 1) :
    ∃ U : OpenNormalSubgroup G, ∃ hDU : D ≤ (U : Subgroup G),
      ∃ c : PadicCocycle θ (U : Subgroup G),
        (c.primaryCharacter D hDclosed hDθ hDU a).toAdd ≠ 0

Module documentation

Detecting primary abelianization by p-adic characters

Declarations

map_one

map_conj

restrictCharacter

primaryCharacter

primaryCharacter_mk

primaryCharacter_conj

exists_padicCocycle_detecting_primary