Module

FiniteIndexTransfer.lean

Nyll.GaloisCohomology.ProP.FiniteIndexTransfer

2 declarations indexed from sourceView source ↗

Module documentation

Continuous transfer from an open finite-index subgroup

The algebraic transfer is continuous: its transversal formula is a finite product, and representatives are continuous functions of the discrete coset space. Normality of the subgroup and discreteness of the target are not needed.

Imports4

Mathlib.GroupTheory.Transfer
Mathlib.Topology.Algebra.OpenSubgroup
Mathlib.Topology.Algebra.Group.Quotient
Mathlib.Topology.Algebra.ContinuousMonoidHom

Imported by4

theorem

continuous_transfer_of_openSubgroup

L28 ↗

ClassFieldTower.Cohomology.continuous_transfer_of_openSubgroup

Documentation

Transfer from an open finite-index subgroup preserves continuity.

Source context 3 commands

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

open scoped Pointwise
namespace ClassFieldTower.Cohomology
variable {G A : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A]

Lean source · statement

theorem continuous_transfer_of_openSubgroup
    (H : OpenSubgroup G) [H.toSubgroup.FiniteIndex]
    (φ : H →* A) (hφ : Continuous φ) : Continuous (MonoidHom.transfer φ)

def

openSubgroupTransfer

L51 ↗

ClassFieldTower.Cohomology.openSubgroupTransfer