Module

FixedInclusion.lean

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.FixedInclusion

2 declarations indexed from sourceView source ↗

Module documentation

Inclusion of fixed primary classes

Under relative formal Hilbert 90, globally fixed primary classes inject into the primary abelianization of the ambient group.

Imports2

Imported by2

theorem

primaryFixed_eq_one_of_inclusion_eq_one

L21 ↗

Yamaguchi26AbfaithfulGalois.primaryFixed_eq_one_of_inclusion_eq_one

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 primaryFixed_eq_one_of_inclusion_eq_one
    {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (D : Subgroup G) [D.Normal] (hD : IsClosed (D : Set G))
    (θ : Orientation ℓ G) (hDθ : D ≤ θ.toMonoidHom.ker)
    (hLift : RelativeFormalHilbert90 D θ)
    (a : PrimaryAbelianization ℓ D)
    (ha : a ∈ primaryFixedSubgroup ℓ D hD (⊤ : Subgroup G))
    (hzero : primaryInclusionMap ℓ D hD a = 1) : a = 1

theorem

primaryInclusionMap_injective_on_fixed

L64 ↗

Yamaguchi26AbfaithfulGalois.primaryInclusionMap_injective_on_fixed

Documentation

Global fixed primary classes inject into the primary abelianization of the ambient group under the relative formal Hilbert 90 hypothesis.