Module

TrivialOrientationCriterion.lean

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.TrivialOrientationCriterion

3 declarations indexed from sourceView source ↗

Module documentation

The trivial orientation and ab-torsion-freeness

The criterion retained from the earlier manuscript identifies formal Hilbert 90 for the trivial orientation with the absence of ℓ-torsion in every open-subgroup abelianization. Ab-torsion-freeness then supplies formal Hilbert 90 for the trivial orientation at each prime.

Imports3

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.TrivialOrientation
Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.AbTorsionFree
Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Imported by1

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.All

theorem

formalHilbert90_trivial_iff_no_primary_torsion

L26 ↗

Yamaguchi26AbfaithfulGalois.formalHilbert90_trivial_iff_no_primary_torsion

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem formalHilbert90_trivial_iff_no_primary_torsion
    {ℓ : ℕ} [Fact ℓ.Prime]
    (G : ProfiniteGrp.{u}) :
    FormalHilbert90 (1 : Orientation ℓ G) ↔
      ∀ H : OpenSubgroup G,
        ∀ a : TopologicalAbelianization (H : Subgroup G),
          a ^ ℓ = 1 → a = 1

theorem

formalHilbert90_trivial_iff_primary_torsionFree

L44 ↗

Yamaguchi26AbfaithfulGalois.formalHilbert90_trivial_iff_primary_torsionFree

Documentation

The earlier trivial-orientation criterion in its primary-component formulation.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem formalHilbert90_trivial_iff_primary_torsionFree
    {ℓ : ℕ} [Fact ℓ.Prime]
    (G : ProfiniteGrp.{u}) :
    FormalHilbert90 (1 : Orientation ℓ G) ↔
      ∀ H : OpenSubgroup G, IsMulTorsionFree (PrimaryAbelianization ℓ (H : Subgroup G))

theorem

formalHilbert90_trivial_of_isAbTorsionFree

L68 ↗

Yamaguchi26AbfaithfulGalois.formalHilbert90_trivial_of_isAbTorsionFree

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem formalHilbert90_trivial_of_isAbTorsionFree
    {ℓ : ℕ} [Fact ℓ.Prime]
    (G : ProfiniteGrp.{u})
    (hG : IsAbTorsionFree G) :
    FormalHilbert90 (1 : Orientation ℓ G)

Module documentation

The trivial orientation and ab-torsion-freeness

Declarations

formalHilbert90_trivial_iff_no_primary_torsion

formalHilbert90_trivial_iff_primary_torsionFree

formalHilbert90_trivial_of_isAbTorsionFree