Module

AbsoluteGaloisAbelianModPower.lean

Nyll.GaloisCohomology.Topology.AbsoluteGaloisAbelianModPower

1 declaration indexed from sourceView source ↗

Module documentation

Functoriality of absolute Galois abelianizations modulo powers

The inner discrepancy in the choice of algebraic-closure embeddings disappears in every commutative quotient, including the quotient modulo q-th powers.

Imports2

Imported by2

theorem

abelianModPowerMap_map_comp

L25 ↗

Field.absoluteGaloisGroup.abelianModPowerMap_map_comp

Documentation

Absolute Galois restriction on abelianizations modulo powers respects composition of field embeddings.

Source context 3 commands

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

namespace Field.absoluteGaloisGroup
open ProCGroups.Abelian
variable {K L M : Type*} [Field K] [Field L] [Field M]

Lean source · statement

theorem abelianModPowerMap_map_comp (q : ℕ) (f : K →+* L) (g : L →+* M) :
    abelianModPowerMap q (map (g.comp f)) =
      (abelianModPowerMap q (map f)).comp (abelianModPowerMap q (map g))

Module documentation

Functoriality of absolute Galois abelianizations modulo powers

Declarations

abelianModPowerMap_map_comp