Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FiniteAbelianFamilyRigidity

Module documentation

Rigidity from a cyclic quotient and subgroup data

A finite abelian quotient is determined by its action on all intermediate subgroups together with its action on a sufficiently large cyclic quotient. The group-theoretic statement below isolates the part of uniqueness of a coherent local Artin family that does not involve fields or valuations.

theorem

monoidHom_ext_of_cyclic_quotient_and_subgroups

L25 ↗

LocalClassFieldTheory.monoidHom_ext_of_cyclic_quotient_and_subgroups

Documentation

Two homomorphisms into an abelian group coincide if every subgroup containing a value of the first also contains the corresponding value of the second, and if they agree after passage to a cyclic quotient whose generator order annihilates the target. In the local Artin application the cyclic quotient is supplied by an unramified extension.

Source context 1 command

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

namespace LocalClassFieldTheory

Lean source · statement

theorem monoidHom_ext_of_cyclic_quotient_and_subgroups
    {A G C : Type*} [Group A] [Group G] [Group C]
    (f g : A →* G) (β : G →* C) (u : A)
    (hgenerator : Subgroup.zpowers (β (f u)) = ⊤)
    (hexponent : ∀ z : G, z ^ orderOf (β (f u)) = 1)
    (hsubgroups : ∀ (S : Subgroup G) (x : A), f x ∈ S → g x ∈ S)
    (hquotient : ∀ x : A, β (g x) = β (f x)) :
    f = g

Module documentation

Rigidity from a cyclic quotient and subgroup data

Declarations

monoidHom_ext_of_cyclic_quotient_and_subgroups