Module

TransferRestriction.lean

Nyll.GaloisCohomology.ProP.TransferRestriction

1 declaration indexed from sourceView source ↗

Module documentation

Restricting transfer of a conjugation-invariant character

A normal subgroup acts trivially on its coset space. Each factor of the transfer of an element of the subgroup is therefore a conjugate of that element. Conjugation invariance of the character makes the product its value raised to the subgroup index.

Imports5

Mathlib.GroupTheory.Transfer
Mathlib.GroupTheory.GroupAction.ConjAct
Mathlib.GroupTheory.GroupAction.Quotient
Mathlib.GroupTheory.QuotientGroup.Defs
Mathlib.GroupTheory.Index

Imported by3

theorem

transfer_subtype_eq_pow_of_conjInvariant

L30 ↗

ClassFieldTower.Cohomology.transfer_subtype_eq_pow_of_conjInvariant

Documentation

Transfer restricts to the index power of a conjugation-invariant character on a normal finite-index subgroup.

Source context 3 commands

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

open scoped Pointwise
namespace ClassFieldTower.Cohomology
variable {G A : Type*} [Group G] [CommGroup A]

Lean source · statement

theorem transfer_subtype_eq_pow_of_conjInvariant
    (H : Subgroup G) [H.Normal] [H.FiniteIndex] (φ : H →* A)
    (hinv : ∀ (g : G) (h : H), φ (MulAut.conjNormal g h) = φ h) (h : H) :
    MonoidHom.transfer φ (h : G) = φ h ^ H.index

Module documentation

Restricting transfer of a conjugation-invariant character

Declarations

transfer_subtype_eq_pow_of_conjInvariant