Module

Transfer.lean

Nyll.ProCGroups.Abelian.Transfer

6 declarations indexed from sourceView source ↗

Module documentation

Continuous transfer for open normal subgroups

Imports2

Imported by3

def

openNormalTransferTerm

L17 ↗

ProCGroups.FiniteStepSolvableQuotients.openNormalTransferTerm

Documentation

The individual transfer term landing in an open normal subgroup.

Source context 3 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian ProCGroups.ProC
universe u v

Lean source · statement

def openNormalTransferTerm
    {G : Type u} [TopologicalSpace G] [Group G]
    (N : OpenNormalSubgroup G)
    (q : G ⧸ (N : Subgroup G)) (g : G) :
    ↥(N : Subgroup G)

def

openNormalTransferTopologicalAbelianizationPre

L54 ↗

ProCGroups.FiniteStepSolvableQuotients.openNormalTransferTopologicalAbelianizationPre

Documentation

Transfer on topological abelianization, before passing to the quotient universal property.

Source context 3 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian ProCGroups.ProC
universe u v

Lean source · statement

def openNormalTransferTopologicalAbelianizationPre
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (N : OpenNormalSubgroup G) [Finite (G ⧸ (N : Subgroup G))] :
    G →ₜ* TopologicalAbelianization ↥(N : Subgroup G)

def

openNormalTransferTopologicalAbelianization

L154 ↗

ProCGroups.FiniteStepSolvableQuotients.openNormalTransferTopologicalAbelianization

Documentation

Open normal subgroups transfer through the topological abelianization by taking the appropriate preimage or image under the quotient map.

Source context 3 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian ProCGroups.ProC
universe u v

Lean source · statement

def openNormalTransferTopologicalAbelianization
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (N : OpenNormalSubgroup G) [Finite (G ⧸ (N : Subgroup G))] :
    TopologicalAbelianization G →ₜ* TopologicalAbelianization ↥(N : Subgroup G)

theorem

openNormalTransferTopologicalAbelianization_eq_pow_of_fixed

L162 ↗

ProCGroups.FiniteStepSolvableQuotients.openNormalTransferTopologicalAbelianization_eq_pow_of_fixed

Documentation

Transfer sends a fixed point to the \(|G/N|\)-th power of that point.

Source context 3 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian ProCGroups.ProC
universe u v

Lean source · statement

theorem openNormalTransferTopologicalAbelianization_eq_pow_of_fixed
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (N : OpenNormalSubgroup G) [Finite (G ⧸ (N : Subgroup G))]
    {a : TopologicalAbelianization ↥(N : Subgroup G)}
    (hfix :
      ∀ q : G ⧸ (N : Subgroup G),
        quotientConjugationTopologicalAbelianizationMap (G := G) (N := (N : Subgroup G)) q a = a) :
    openNormalTransferTopologicalAbelianization (G := G) N
      (TopologicalAbelianization.map
        { toMonoidHom := (N : Subgroup G).subtype
          continuous_toFun := continuous_subtype_val } a) =
      a ^ Nat.card (G ⧸ (N : Subgroup G))

def

openNormalCharacterTransfer

L281 ↗

ProCGroups.FiniteStepSolvableQuotients.openNormalCharacterTransfer

Documentation

Transfer of an arbitrary continuous character with commutative values.

Source context 3 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian ProCGroups.ProC
universe u v

Lean source · statement

def openNormalCharacterTransfer
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
    (N : OpenNormalSubgroup G) [Finite (G ⧸ (N : Subgroup G))]
    (χ : (N : Subgroup G) →ₜ* A) : G →ₜ* A

theorem

openNormalCharacterTransfer_apply_of_mem

L290 ↗

ProCGroups.FiniteStepSolvableQuotients.openNormalCharacterTransfer_apply_of_mem

Documentation

On the open normal subgroup, transfer is the product over conjugates.

Source context 3 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian ProCGroups.ProC
universe u v

Lean source · full declaration

theorem openNormalCharacterTransfer_apply_of_mem
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
    (N : OpenNormalSubgroup G) [Finite (G ⧸ (N : Subgroup G))]
    (χ : (N : Subgroup G) →ₜ* A) (n : (N : Subgroup G)) :
    letI : Fintype (G ⧸ (N : Subgroup G)) := Fintype.ofFinite _
    openNormalCharacterTransfer N χ n =
      ∏ q : G ⧸ (N : Subgroup G),
        χ (MulAut.conjNormal ((quotientOpenSubgroupSection (N : Subgroup G) q)⁻¹) n) := by
  classical
  let : Fintype (G ⧸ (N : Subgroup G)) := Fintype.ofFinite _
  change TopologicalAbelianization.lift χ
    (∏ q : G ⧸ (N : Subgroup G),
      TopologicalAbelianization.mk (N : Subgroup G) (openNormalTransferTerm N q n)) = _
  rw [map_prod]
  apply Fintype.prod_congr
  intro q
  rw [TopologicalAbelianization.lift_apply_mk]
  congr 1
  apply Subtype.ext
  have hn : QuotientGroup.mk' (N : Subgroup G) (n : G) = 1 :=
    (QuotientGroup.eq_one_iff (N := (N : Subgroup G)) _).mpr n.property
  change (quotientOpenSubgroupSection (N : Subgroup G)
    (QuotientGroup.mk' (N : Subgroup G) (n : G) * q))⁻¹ * (n : G) *
      quotientOpenSubgroupSection (N : Subgroup G) q = _
  rw [hn, one_mul]
  simp only [MulAut.conjNormal_apply, inv_inv]

Module documentation

Continuous transfer for open normal subgroups

Declarations

openNormalTransferTerm

openNormalTransferTopologicalAbelianizationPre

openNormalTransferTopologicalAbelianization

openNormalTransferTopologicalAbelianization_eq_pow_of_fixed

openNormalCharacterTransfer

openNormalCharacterTransfer_apply_of_mem