Module

TransferNaturality.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.TransferNaturality

11 declarations indexed from sourceView source ↗

Module documentation

Naturality of transfer under a quotient

This file supplies the group-theoretic source used in transfer--norm naturality. If a surjection has kernel contained in a finite-index subgroup, it identifies the two left-coset spaces and transfer commutes with the induced maps on abelianizations.

Imports2

Mathlib.GroupTheory.Transfer
Mathlib.GroupTheory.Abelianization.Defs

Imported by2

def

leftCosetEquivMapOfSurjective

L31 ↗

ClassFormation.leftCosetEquivMapOfSurjective

Documentation

A surjection identifies left cosets of H with left cosets of its image when its kernel is contained in H.

Source context 5 commands

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

namespace ClassFormation
noncomputable section
open Function
open scoped Pointwise
variable {P : Type*} {Q : Type*} [Group P] [Group Q]

Lean source · statement

def leftCosetEquivMapOfSurjective
    (f : P →* Q) (hf : Function.Surjective f)
    (H : Subgroup P) (hker : f.ker ≤ H) :
    P ⧸ H ≃ Q ⧸ H.map f

theorem

leftCosetEquivMapOfSurjective_mk

L62 ↗

ClassFormation.leftCosetEquivMapOfSurjective_mk

Documentation

Establishes the identity leftCosetEquivMapOfSurjective f hf H hker (QuotientGroup.mk p) = QuotientGroup.mk (f p).

Source context 5 commands

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

namespace ClassFormation
noncomputable section
open Function
open scoped Pointwise
variable {P : Type*} {Q : Type*} [Group P] [Group Q]

Lean source · statement

theorem leftCosetEquivMapOfSurjective_mk
    (f : P →* Q) (hf : Function.Surjective f)
    (H : Subgroup P) (hker : f.ker ≤ H) (p : P) :
    leftCosetEquivMapOfSurjective f hf H hker (QuotientGroup.mk p) =
      QuotientGroup.mk (f p)

theorem

leftCosetEquivMapOfSurjective_smul

L74 ↗

ClassFormation.leftCosetEquivMapOfSurjective_smul

Documentation

Establishes the identity leftCosetEquivMapOfSurjective f hf H hker (p • q) = f p • leftCosetEquivMapOfSurjective f hf H hker q.

Source context 5 commands

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

namespace ClassFormation
noncomputable section
open Function
open scoped Pointwise
variable {P : Type*} {Q : Type*} [Group P] [Group Q]

Lean source · statement

theorem leftCosetEquivMapOfSurjective_smul
    (f : P →* Q) (hf : Function.Surjective f)
    (H : Subgroup P) (hker : f.ker ≤ H)
    (p : P) (q : P ⧸ H) :
    leftCosetEquivMapOfSurjective f hf H hker (p • q) =
      f p • leftCosetEquivMapOfSurjective f hf H hker q

def

leftTransversalMapOfSurjective

L88 ↗

ClassFormation.leftTransversalMapOfSurjective

Documentation

A left transversal descends along the same quotient map. It is built from the induced equivalence of left-coset spaces, so its chosen representatives are literally the images of the original representatives.

Source context 5 commands

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

namespace ClassFormation
noncomputable section
open Function
open scoped Pointwise
variable {P : Type*} {Q : Type*} [Group P] [Group Q]

Lean source · statement

def leftTransversalMapOfSurjective
    (f : P →* Q) (hf : Function.Surjective f)
    (H : Subgroup P) (hker : f.ker ≤ H)
    (T : H.LeftTransversal) : (H.map f).LeftTransversal

theorem

leftTransversalMapOfSurjective_apply

L110 ↗

ClassFormation.leftTransversalMapOfSurjective_apply

Documentation

The defining evaluation formula for leftTransversalMapOfSurjective is ((leftTransversalMapOfSurjective f hf H hker T).2.leftQuotientEquiv q : Q) = f (T.2.leftQuotientEquiv ((leftCosetEquivMapOfSurjective f hf H hker).symm q) : P).

Source context 5 commands

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

namespace ClassFormation
noncomputable section
open Function
open scoped Pointwise
variable {P : Type*} {Q : Type*} [Group P] [Group Q]

Lean source · statement

theorem leftTransversalMapOfSurjective_apply
    (f : P →* Q) (hf : Function.Surjective f)
    (H : Subgroup P) (hker : f.ker ≤ H)
    (T : H.LeftTransversal) (q : Q ⧸ H.map f) :
    ((leftTransversalMapOfSurjective f hf H hker T).2.leftQuotientEquiv q : Q) =
      f (T.2.leftQuotientEquiv
        ((leftCosetEquivMapOfSurjective f hf H hker).symm q) : P)

theorem

leftQuotientEquiv_mk_of_mem

L130 ↗

ClassFormation.leftQuotientEquiv_mk_of_mem

Source context 5 commands

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

namespace ClassFormation
noncomputable section
open Function
open scoped Pointwise
variable {P : Type*} {Q : Type*} [Group P] [Group Q]

Lean source · statement

theorem leftQuotientEquiv_mk_of_mem
    (H : Subgroup P) (T : H.LeftTransversal) (p : P)
    (hp : p ∈ (T : Set P)) :
    (T.2.leftQuotientEquiv (QuotientGroup.mk p) : P) = p

theorem

mem_leftTransversalMapOfSurjective_iff

L141 ↗

ClassFormation.mem_leftTransversalMapOfSurjective_iff

Source context 5 commands

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

namespace ClassFormation
noncomputable section
open Function
open scoped Pointwise
variable {P : Type*} {Q : Type*} [Group P] [Group Q]

Lean source · statement

theorem mem_leftTransversalMapOfSurjective_iff
    (f : P →* Q) (hf : Function.Surjective f)
    (H : Subgroup P) (hker : f.ker ≤ H)
    (T : H.LeftTransversal) (q : Q) :
    q ∈ (leftTransversalMapOfSurjective f hf H hker T : Set Q) ↔
      ∃ p ∈ (T : Set P), f p = q

theorem

leftTransversalMapOfSurjective_smul

L160 ↗

ClassFormation.leftTransversalMapOfSurjective_smul

Source context 5 commands

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

namespace ClassFormation
noncomputable section
open Function
open scoped Pointwise
variable {P : Type*} {Q : Type*} [Group P] [Group Q]

Lean source · statement

theorem leftTransversalMapOfSurjective_smul
    (f : P →* Q) (hf : Function.Surjective f)
    (H : Subgroup P) (hker : f.ker ≤ H)
    (T : H.LeftTransversal) (p : P) :
    leftTransversalMapOfSurjective f hf H hker (p • T) =
      f p • leftTransversalMapOfSurjective f hf H hker T

theorem

leftTransversals_diff_natural_of_surjective

L188 ↗

ClassFormation.leftTransversals_diff_natural_of_surjective

Source context 5 commands

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

namespace ClassFormation
noncomputable section
open Function
open scoped Pointwise
variable {P : Type*} {Q : Type*} [Group P] [Group Q]

Lean source · full declaration

theorem leftTransversals_diff_natural_of_surjective
    (f : P →* Q) (hf : Function.Surjective f)
    (H : Subgroup P) (hker : f.ker ≤ H) [H.FiniteIndex]
    (S T : H.LeftTransversal) :
    let J := H.map f
    letI : J.FiniteIndex := by
      rw [Subgroup.finiteIndex_iff, H.index_map_eq hf hker]
      exact Subgroup.FiniteIndex.index_ne_zero
    Abelianization.map (f.subgroupMap H)
        (Subgroup.leftTransversals.diff
          (Abelianization.of : H →* Abelianization H) S T) =
      Subgroup.leftTransversals.diff
        (Abelianization.of : J →* Abelianization J)
        (leftTransversalMapOfSurjective f hf H hker S)
        (leftTransversalMapOfSurjective f hf H hker T) := by
  dsimp only
  let : (H.map f).FiniteIndex := by
    rw [Subgroup.finiteIndex_iff, H.index_map_eq hf hker]
    exact Subgroup.FiniteIndex.index_ne_zero
  classical
  let : Fintype (P ⧸ H) := H.fintypeQuotientOfFiniteIndex
  let : Fintype (Q ⧸ H.map f) :=
    (H.map f).fintypeQuotientOfFiniteIndex
  let e := leftCosetEquivMapOfSurjective f hf H hker
  simp only [Subgroup.leftTransversals.diff, map_prod,
    Abelianization.map_of, leftTransversalMapOfSurjective_apply]
  rw [← e.prod_comp]
  apply Finset.prod_congr rfl
  intro q _
  apply congrArg Abelianization.of
  apply Subtype.ext
  simp [e]

theorem

abelianization_transfer_natural_of_surjective

L225 ↗

ClassFormation.abelianization_transfer_natural_of_surjective

Documentation

Transfer is natural for a surjective homomorphism whose kernel is contained in the finite-index subgroup. Both transfer maps are Mathlib's actual MonoidHom.transfer; the proof descends an arbitrary left transversal and compares the defining products term by term.

Source context 5 commands

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

namespace ClassFormation
noncomputable section
open Function
open scoped Pointwise
variable {P : Type*} {Q : Type*} [Group P] [Group Q]

Lean source · full declaration

theorem abelianization_transfer_natural_of_surjective
    (f : P →* Q) (hf : Function.Surjective f)
    (H : Subgroup P) (hker : f.ker ≤ H) [H.FiniteIndex] :
    let J := H.map f
    letI : J.FiniteIndex := by
      rw [Subgroup.finiteIndex_iff, H.index_map_eq hf hker]
      exact Subgroup.FiniteIndex.index_ne_zero
    (Abelianization.map (f.subgroupMap H)).comp
        (Abelianization.lift
          (MonoidHom.transfer
            (Abelianization.of : H →* Abelianization H))) =
      (Abelianization.lift
          (MonoidHom.transfer
            (Abelianization.of : J →* Abelianization J))).comp
        (Abelianization.map f) := by
  dsimp only
  let : (H.map f).FiniteIndex := by
    rw [Subgroup.finiteIndex_iff, H.index_map_eq hf hker]
    exact Subgroup.FiniteIndex.index_ne_zero
  apply Abelianization.hom_ext
  apply MonoidHom.ext
  intro p
  simp only [MonoidHom.comp_apply, Abelianization.lift_apply_of,
    Abelianization.map_of]
  let T : H.LeftTransversal := default
  rw [MonoidHom.transfer_def
    (Abelianization.of : H →* Abelianization H) T p]
  rw [MonoidHom.transfer_def
    (Abelianization.of : H.map f →* Abelianization (H.map f))
    (leftTransversalMapOfSurjective f hf H hker T) (f p)]
  rw [← leftTransversalMapOfSurjective_smul f hf H hker T p]
  exact leftTransversals_diff_natural_of_surjective
    f hf H hker T (p • T)

theorem

abelianization_transfer_congr_subgroup

L261 ↗

ClassFormation.abelianization_transfer_congr_subgroup

Documentation

Replacing a finite-index subgroup by an equal subgroup only transports the codomain of transfer along the corresponding canonical equivalence.

Source context 5 commands

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

namespace ClassFormation
noncomputable section
open Function
open scoped Pointwise
variable {P : Type*} {Q : Type*} [Group P] [Group Q]

Lean source · statement

theorem abelianization_transfer_congr_subgroup
    (H J : Subgroup P) (h : H = J)
    [H.FiniteIndex] [J.FiniteIndex] :
    (MulEquiv.subgroupCongr h).abelianizationCongr.toMonoidHom.comp
        (Abelianization.lift
          (MonoidHom.transfer
            (Abelianization.of : H →* Abelianization H))) =
      Abelianization.lift
        (MonoidHom.transfer
          (Abelianization.of : J →* Abelianization J))

Module documentation

Naturality of transfer under a quotient

Declarations