NYLL
Module

QuotientTransport.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ClosedFiniteIndexClassFieldReciprocity.Topological.QuotientTransport
2 declarations indexed from sourceView source ↗

Module documentation

Continuous transport between equal quotient groups

Equality of normal subgroups identifies their quotient groups with the same native quotient topology. Eliminating the equality therefore gives the continuous multiplicative equivalence directly; no discrete-topology instances or domain-specific class-field tower are required.

Imports1
Imported by7

Declarations

def

quotientContinuousMulEquivOfEq

L28 ↗
QuotientGroup.quotientContinuousMulEquivOfEq
Documentation

Equal normal subgroups induce a continuous multiplicative equivalence between their quotient groups with their native quotient topologies.

Source context 3 commands

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

noncomputable section
namespace QuotientGroup
variable {G : Type*} [Group G] [TopologicalSpace G]
Lean source · statement
def quotientContinuousMulEquivOfEq
    {N H : Subgroup G} [N.Normal] [H.Normal]
    (h : N = H) :
    G ⧸ N ≃ₜ* G ⧸ H
theorem

quotientContinuousMulEquivOfEq_apply

L38 ↗
QuotientGroup.quotientContinuousMulEquivOfEq_apply
Documentation

Forgetting topology from quotientContinuousMulEquivOfEq recovers the canonical multiplicative equivalence induced by the same equality.

Source context 3 commands

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

noncomputable section
namespace QuotientGroup
variable {G : Type*} [Group G] [TopologicalSpace G]
Lean source · statement
theorem quotientContinuousMulEquivOfEq_apply
    {N H : Subgroup G} [N.Normal] [H.Normal]
    (h : N = H) (x : G ⧸ N) :
    quotientContinuousMulEquivOfEq h x =
      QuotientGroup.quotientMulEquivOfEq h x

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