Module

QuotientVariety.lean

Nyll.ProCGroups.Topologies.FullSubgroupTopology.QuotientVariety

2 declarations indexed from sourceView source ↗

Module documentation

Quotient varieties

A quotient variety is a quotient formation stable under pullback along group homomorphisms. This file shows that the corresponding notion of open subgroup is likewise preserved by comap.

Imports1

Nyll.ProCGroups.Topologies.FullSubgroupTopology.QuotientFormation

Imported by1

Nyll.ProCGroups.Topologies.FullSubgroupTopology.All

structure

QuotientVariety

L24 ↗

ProCGroups.Topologies.QuotientVariety

Documentation

A quotient variety is a quotient formation with the closure properties needed for varieties.

Source context 4 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u

Lean source · full declaration

structure QuotientVariety extends QuotientFormation where
  /-- Admissible quotient kernels are closed under pullback along group homomorphisms. -/
  comap_closed :
    ∀ {G H : Type u} [Group G] [Group H] (f : G →* H) {N : Subgroup H},
      toQuotientFormation.contains N → toQuotientFormation.contains (N.comap f)

theorem

isOpenSubgroup_comap

L36 ↗

ProCGroups.Topologies.QuotientVariety.isOpenSubgroup_comap

Documentation

Abstract form of the fact that full pro-\(C\) openness pulls back along a homomorphism.

Source context 7 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientVariety
variable (C : QuotientVariety)
variable {G H : Type u} [Group G] [Group H]

Lean source · statement

theorem isOpenSubgroup_comap (f : G →* H) {K : Subgroup H}
    (hK : C.toQuotientFormation.IsOpenSubgroup K) :
    C.toQuotientFormation.IsOpenSubgroup (K.comap f)

Module documentation

Quotient varieties

Declarations

QuotientVariety

isOpenSubgroup_comap