Module

CoprimeFixedLift.lean

Nyll.ProCGroups.ProP.CoprimeFixedLift

2 declarations indexed from sourceView source ↗

Module documentation

Fixed lifts under coprime group actions

A fixed element of an equivariant quotient has an invariant fiber. This fiber has the cardinality of the kernel. Orbit counting for an r-group therefore produces a fixed lift whenever r does not divide that cardinality. In particular, this holds for a quotient of a finite p-group when r ≠ p.

No finiteness assumption on the acting group is needed. The fiber uses the canonical action on a SubMulAction; no action instance is installed here.

Imports7

Mathlib.Data.Nat.Prime.Basic
Mathlib.GroupTheory.Coset.Basic
Mathlib.GroupTheory.GroupAction.Defs
Mathlib.GroupTheory.GroupAction.Hom
Mathlib.GroupTheory.GroupAction.SubMulAction
Mathlib.GroupTheory.PGroup
Mathlib.SetTheory.Cardinal.Finite

Imported by1

Nyll.ProCGroups.ProP.All

theorem

exists_fixed_lift_of_not_dvd_card_ker

L37 ↗

ClassFieldTower.ProP.exists_fixed_lift_of_not_dvd_card_ker

Documentation

Orbit counting on the actual fiber of an equivariant surjection produces a fixed lift if the acting prime does not divide the kernel's cardinality.

Source context 3 commands

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

namespace ClassFieldTower.ProP
universe u v w
variable {Γ : Type u} {P : Type v} {Q : Type w}
    [Group Γ] [Group P] [Group Q]
    [MulDistribMulAction Γ P] [MulDistribMulAction Γ Q]

Lean source · statement

theorem exists_fixed_lift_of_not_dvd_card_ker
    {r : ℕ} [Fact r.Prime] (hΓ : IsPGroup r Γ)
    (f : P →*[Γ] Q) (hf : Function.Surjective f)
    (hker : ¬ r ∣ Nat.card f.toMonoidHom.ker)
    (y : Q) (hy : ∀ γ : Γ, γ • y = y) :
    ∃ x : P, f x = y ∧ ∀ γ : Γ, γ • x = x

theorem

exists_fixed_lift_of_isPGroup

L63 ↗

ClassFieldTower.ProP.exists_fixed_lift_of_isPGroup