Module

InducedFunctions.lean

Nyll.ProCGroups.InducedFunctions

7 declarations indexed from sourceView source ↗

Module documentation

Induced groups of equivariant functions

For a subgroup H of G acting on a commutative group B, the induced group consists of functions satisfying f (h * x) = h • f x. Right translation gives its G-action. Evaluation at the identity is an H-equivariant epimorphism, without any finite-index assumption.

Imports3

Mathlib.Algebra.Group.Action.Basic
Mathlib.Algebra.Group.Pi.Basic
Mathlib.Algebra.Group.Subgroup.Defs

Imported by5

def

inducedSubgroup

L27 ↗

ProCGroups.InducedFunctions.inducedSubgroup

Documentation

The subgroup of equivariant functions defining the induced group.

Source context 3 commands

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

namespace ProCGroups.InducedFunctions
universe uG uB
variable {G : Type uG} {B : Type uB}

Lean source · full declaration

def inducedSubgroup [Group G] (H : Subgroup G) [CommGroup B]
    [MulDistribMulAction H B] : Subgroup (G → B) where
  carrier := {f | ∀ (h : H) (x : G), f (h.1 * x) = h • f x}
  one_mem' := by
    intro h x
    exact (smul_one h).symm
  mul_mem' := by
    intro f k hf hk h x
    simp only [Pi.mul_apply, hf h x, hk h x]
    exact (MulDistribMulAction.smul_mul h (f x) (k x)).symm
  inv_mem' := by
    intro f hf h x
    simp only [Pi.inv_apply, hf h x]
    exact (map_inv (MulDistribMulAction.toMonoidHom B h) (f x)).symm

abbrev

InducedModule

L43 ↗

ProCGroups.InducedFunctions.InducedModule

Documentation

The commutative group of equivariant functions.

Source context 3 commands

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

namespace ProCGroups.InducedFunctions
universe uG uB
variable {G : Type uG} {B : Type uB}

Lean source · statement

abbrev InducedModule [Group G] (H : Subgroup G) [CommGroup B]
    [MulDistribMulAction H B]

instance

inducedMulDistribMulAction

L48 ↗

ProCGroups.InducedFunctions.inducedMulDistribMulAction

Documentation

The canonical right-translation action on equivariant functions.

Source context 3 commands

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

namespace ProCGroups.InducedFunctions
universe uG uB
variable {G : Type uG} {B : Type uB}

Lean source · full declaration

instance inducedMulDistribMulAction [Group G] (H : Subgroup G) [CommGroup B]
    [MulDistribMulAction H B] :
    MulDistribMulAction G (InducedModule (B := B) H) where
  smul g f := ⟨fun x ↦ f.1 (x * g), by
    intro h x
    simpa only [mul_assoc] using f.2 h (x * g)⟩
  one_smul := by
    intro f
    apply Subtype.ext
    funext x
    change f.1 (x * 1) = f.1 x
    rw [mul_one]
  mul_smul := by
    intro g k f
    apply Subtype.ext
    funext x
    change f.1 (x * (g * k)) = f.1 ((x * g) * k)
    rw [mul_assoc]
  smul_mul := by
    intro g f k
    ext x
    rfl
  smul_one := by
    intro g
    ext x
    rfl

def

inducedEvaluation

L76 ↗

ProCGroups.InducedFunctions.inducedEvaluation

Documentation

Evaluation at the identity element of the ambient group.

Source context 3 commands

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

namespace ProCGroups.InducedFunctions
universe uG uB
variable {G : Type uG} {B : Type uB}

Lean source · full declaration

def inducedEvaluation [Group G] (H : Subgroup G) [CommGroup B]
    [MulDistribMulAction H B] :
    InducedModule (B := B) H →* B where
  toFun f := f.1 1
  map_one' := rfl
  map_mul' _ _ := rfl

theorem

inducedEvaluation_apply

L83 ↗

ProCGroups.InducedFunctions.inducedEvaluation_apply

Source context 3 commands

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

namespace ProCGroups.InducedFunctions
universe uG uB
variable {G : Type uG} {B : Type uB}

Lean source · statement

theorem inducedEvaluation_apply [Group G] (H : Subgroup G) [CommGroup B]
    [MulDistribMulAction H B] (f : InducedModule (B := B) H) :
    inducedEvaluation H f = f.1 1

theorem

inducedEvaluation_smul

L90 ↗

ProCGroups.InducedFunctions.inducedEvaluation_smul

Documentation

Evaluation intertwines the restricted translation action and the original subgroup action.

Source context 3 commands

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

namespace ProCGroups.InducedFunctions
universe uG uB
variable {G : Type uG} {B : Type uB}

Lean source · statement

theorem inducedEvaluation_smul [Group G] (H : Subgroup G) [CommGroup B]
    [MulDistribMulAction H B] (h : H) (f : InducedModule (B := B) H) :
    inducedEvaluation H ((h : G) • f) = h • inducedEvaluation H f

theorem

inducedEvaluation_surjective

L98 ↗

ProCGroups.InducedFunctions.inducedEvaluation_surjective

Documentation

An arbitrary value at the identity extends to an equivariant function: use the original action on H and the identity value outside H.

Source context 3 commands

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

namespace ProCGroups.InducedFunctions
universe uG uB
variable {G : Type uG} {B : Type uB}

Lean source · statement

theorem inducedEvaluation_surjective [Group G] (H : Subgroup G) [CommGroup B]
    [MulDistribMulAction H B] : Function.Surjective (inducedEvaluation (B := B) H)

Module documentation

Induced groups of equivariant functions

Declarations

inducedSubgroup

InducedModule

inducedMulDistribMulAction

inducedEvaluation

inducedEvaluation_apply

inducedEvaluation_smul

inducedEvaluation_surjective