Module

RegularWreathQuotient.lean

Nyll.ProCGroups.GroupTheory.RegularWreathQuotient

4 declarations indexed from sourceView source ↗

Module documentation

Quotients of regular wreath modules

Restriction to a finite subgroup followed by multiplication along the fibers of a quotient is equivariant and surjective. This produces regular wreath quotients after restricting the right factor to the subgroup.

Imports3

Nyll.ProCGroups.WreathProducts
Mathlib.Algebra.BigOperators.Group.Finset.Basic
Mathlib.Algebra.Group.Pi.Lemmas

Imported by2

def

regularWreathFiberNorm

L27 ↗

ProCGroups.regularWreathFiberNorm

Documentation

Multiply the coordinates in each fiber of a homomorphism from a subgroup.

Source context 3 commands

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

namespace ProCGroups
universe u v w
variable {A : Type u} [CommGroup A] {Q : Type v} [Group Q] [Finite Q]
  {B : Type w} [Group B]

Lean source · statement

def regularWreathFiberNorm (J : Subgroup Q) (ρ : J →* B) :
    (Q → A) →* (B → A)

theorem

regularWreathFiberNorm_equivariant

L47 ↗

ProCGroups.regularWreathFiberNorm_equivariant

Documentation

Fiber multiplication intertwines the two regular translation actions.

Source context 3 commands

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

namespace ProCGroups
universe u v w
variable {A : Type u} [CommGroup A] {Q : Type v} [Group Q] [Finite Q]
  {B : Type w} [Group B]

Lean source · statement

theorem regularWreathFiberNorm_equivariant (J : Subgroup Q) (ρ : J →* B)
    (j : J) (f : Q → A) :
    regularWreathFiberNorm J ρ
        (mulAutArrow (G := Q) (A := Q) (M := A) (j : Q) f) =
      mulAutArrow (G := B) (A := B) (M := A) (ρ j)
        (regularWreathFiberNorm J ρ f)

theorem

regularWreathFiberNorm_mulSingle

L69 ↗

ProCGroups.regularWreathFiberNorm_mulSingle

Documentation

A coordinate supported in the subgroup maps to its image coordinate.

Source context 3 commands

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

namespace ProCGroups
universe u v w
variable {A : Type u} [CommGroup A] {Q : Type v} [Group Q] [Finite Q]
  {B : Type w} [Group B]

Lean source · statement

theorem regularWreathFiberNorm_mulSingle [DecidableEq Q] [DecidableEq B]
    (J : Subgroup Q) (ρ : J →* B)
    (j : J) (a : A) :
    regularWreathFiberNorm J ρ (Pi.mulSingle (j : Q) a) =
      (Pi.mulSingle (ρ j) a : B → A)

theorem

regularWreathFiberNorm_surjective

L90 ↗

ProCGroups.regularWreathFiberNorm_surjective

Documentation

A surjective homomorphism gives a surjective map on regular modules.

Source context 3 commands

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

namespace ProCGroups
universe u v w
variable {A : Type u} [CommGroup A] {Q : Type v} [Group Q] [Finite Q]
  {B : Type w} [Group B]

Lean source · statement

theorem regularWreathFiberNorm_surjective (J : Subgroup Q) (ρ : J →* B)
    (hρ : Function.Surjective ρ) :
    Function.Surjective (regularWreathFiberNorm (A := A) J ρ)

Module documentation

Quotients of regular wreath modules

Declarations

regularWreathFiberNorm

regularWreathFiberNorm_equivariant

regularWreathFiberNorm_mulSingle

regularWreathFiberNorm_surjective