NYLL
Module

InducedSemidirect.lean

Nyll.ProCGroups.InducedSemidirect
3 declarations indexed from sourceView source ↗

Module documentation

Evaluation on induced semidirect products

The subgroup action on the induced group is the restriction of its ambient translation action. Evaluation at the identity therefore induces an actual surjective homomorphism of semidirect products.

Imports3
Imported by2

Declarations

def

inducedEvaluationSemidirectHom

L28 ↗
ProCGroups.InducedFunctions.inducedEvaluationSemidirectHom
Documentation

Evaluation on the function coordinate, with the subgroup coordinate unchanged, defines a homomorphism of the actual semidirect products.

Source context 4 commands

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

namespace ProCGroups.InducedFunctions
universe uQ uA
variable {Q : Type uQ} [Group Q] {A : Type uA} [CommGroup A]
variable (J : Subgroup Q) [MulDistribMulAction J A]
Lean source · statement
def inducedEvaluationSemidirectHom :
    (InducedModule (B := A) J) ⋊[
        (MulDistribMulAction.toMulAut Q (InducedModule (B := A) J)).comp J.subtype] J →*
      A ⋊[MulDistribMulAction.toMulAut J A] J
theorem

inducedEvaluationSemidirectHom_apply

L41 ↗
ProCGroups.InducedFunctions.inducedEvaluationSemidirectHom_apply
Documentation

The semidirect-product map evaluates exactly the induced-function coordinate and preserves the second coordinate.

Source context 4 commands

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

namespace ProCGroups.InducedFunctions
universe uQ uA
variable {Q : Type uQ} [Group Q] {A : Type uA} [CommGroup A]
variable (J : Subgroup Q) [MulDistribMulAction J A]
Lean source · statement
theorem inducedEvaluationSemidirectHom_apply
    (f : InducedModule (B := A) J) (j : J) :
    inducedEvaluationSemidirectHom J ⟨f, j⟩ = ⟨inducedEvaluation J f, j⟩
theorem

inducedEvaluationSemidirectHom_surjective

L47 ↗
ProCGroups.InducedFunctions.inducedEvaluationSemidirectHom_surjective
Documentation

Every pair has a preimage, supplied by the actual evaluation epimorphism.

Source context 4 commands

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

namespace ProCGroups.InducedFunctions
universe uQ uA
variable {Q : Type uQ} [Group Q] {A : Type uA} [CommGroup A]
variable (J : Subgroup Q) [MulDistribMulAction J A]
Lean source · statement
theorem inducedEvaluationSemidirectHom_surjective :
    Function.Surjective (inducedEvaluationSemidirectHom (A := A) J)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.