Module

ContinuousQuotientEquiv.lean

Nyll.ValuedFieldTheory.LocalField.GroupTheory.ContinuousQuotientEquiv

2 declarations indexed from sourceView source ↗

Module documentation

Continuous equivalences of quotient groups

This module supplies the quotient equivalence induced by a continuous multiplicative equivalence. It belongs to the general local-field support layer and does not depend on the separate pro-\(C\) groups library.

Imports2

Mathlib.Topology.Algebra.Group.Quotient
Mathlib.Topology.Algebra.ContinuousMonoidHom

Imported by3

def

continuousCongr

L34 ↗

LocalFieldTheory.QuotientGroup.continuousCongr

Documentation

A continuous multiplicative equivalence descends to continuously equivalent quotients when it maps one normal subgroup onto the other.

Source context 7 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory.QuotientGroup
universe u v
variable {G : Type u} {H : Type v}
variable [Group G] [TopologicalSpace G]
variable [Group H] [TopologicalSpace H]

Lean source · statement

def continuousCongr
    (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
    (e : G ≃ₜ* H) (h : N.map e.toMulEquiv.toMonoidHom = M) :
    G ⧸ N ≃ₜ* H ⧸ M

theorem

continuousCongr_mk

L56 ↗

LocalFieldTheory.QuotientGroup.continuousCongr_mk