Module

QuotientPullbackEquivalences.lean

Nyll.ProCGroups.Categorical.QuotientPullbackEquivalences

55 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / Categorical / Quotient Pullback Equivalences

This module identifies the quotient by an intersection with the concrete fiber product of the two quotient maps to the quotient by their supremum, in both the algebraic and continuous settings.

Imports3

Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Nyll.ProCGroups.Categorical.ProfinitePullbacks
Nyll.ProCGroups.ProC.Quotients.ClosedNormal

Imported by2

instance

normal_iInf

L24 ↗

ProCGroups.Subgroup.normal_iInf

Documentation

An infimum of normal subgroups is normal.

Source context 2 commands

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

namespace ProCGroups
namespace Subgroup

Lean source · full declaration

instance normal_iInf
    {ι : Type*} {G : Type*} [Group G] (W : ι → Subgroup G)
    [∀ i, (W i).Normal] :
    (⨅ i, W i).Normal where
  conj_mem := by
    intro n hn g
    rw [Subgroup.mem_iInf] at hn ⊢
    intro i
    exact (show (W i).Normal by infer_instance).conj_mem n (hn i) g

theorem

isClosed_sup_of_isCompact_of_normal_right

L38 ↗

ProCGroups.Subgroup.isClosed_sup_of_isCompact_of_normal_right

Documentation

In a Hausdorff topological group, the join of a compact subgroup with a compact normal subgroup is closed.

Source context 2 commands

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

namespace ProCGroups
namespace Subgroup

Lean source · statement

theorem isClosed_sup_of_isCompact_of_normal_right
    {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [T2Space G]
    (U V : Subgroup G) [V.Normal]
    (hU : IsCompact (U : Set G)) (hV : IsCompact (V : Set G)) :
    IsClosed ((U ⊔ V : Subgroup G) : Set G)

theorem

isClosed_sup_of_normal

L67 ↗

ProCGroups.Subgroup.isClosed_sup_of_normal

Documentation

In a compact Hausdorff topological group, the join of a closed subgroup with a closed normal subgroup is closed.

Source context 2 commands

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

namespace ProCGroups
namespace Subgroup

Lean source · statement

theorem isClosed_sup_of_normal
    {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [CompactSpace G]
    [T2Space G]
    (U V : Subgroup G) [V.Normal]
    (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
    IsClosed ((U ⊔ V : Subgroup G) : Set G)

def

quotientMapOfLE

L87 ↗

ProCGroups.Categorical.quotientMapOfLE

Documentation

The quotient map induced by an inclusion of normal subgroups.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

def quotientMapOfLE (M N : Subgroup G) [M.Normal] [N.Normal] (hMN : M ≤ N) :
    G ⧸ M →* G ⧸ N

theorem

quotientMapOfLE_mk

L94 ↗

ProCGroups.Categorical.quotientMapOfLE_mk

Documentation

The quotient map induced by an inclusion sends a coset to its image coset.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem quotientMapOfLE_mk (M N : Subgroup G) [M.Normal] [N.Normal]
    (hMN : M ≤ N) (g : G) :
    quotientMapOfLE (G := G) M N hMN (QuotientGroup.mk g) = QuotientGroup.mk g

def

quotientIInfToCoordinate

L104 ↗

ProCGroups.Categorical.quotientIInfToCoordinate

Documentation

Coordinate map from the quotient by an indexed intersection of normal subgroups.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

def quotientIInfToCoordinate {ι : Type v} (W : ι → Subgroup G) [∀ i, (W i).Normal]
    (i : ι) :
    G ⧸ (⨅ j, W j) →* G ⧸ W i

theorem

quotientIInfToCoordinate_mk

L113 ↗

ProCGroups.Categorical.quotientIInfToCoordinate_mk

Documentation

The map from the quotient by the infimum to a coordinate quotient sends a representative to its coordinate coset.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem quotientIInfToCoordinate_mk {ι : Type v}
    (W : ι → Subgroup G) [∀ i, (W i).Normal] (i : ι) (g : G) :
    quotientIInfToCoordinate (G := G) W i (QuotientGroup.mk' (⨅ j, W j) g) =
      QuotientGroup.mk' (W i) g

theorem

quotient_iInf_isLimit

L123 ↗

ProCGroups.Categorical.quotient_iInf_isLimit

Documentation

Quotient classes modulo an indexed intersection are equal when all coordinate quotients are equal.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem quotient_iInf_isLimit {ι : Type v}
    (W : ι → Subgroup G) [∀ i, (W i).Normal]
    {x y : G ⧸ (⨅ i, W i)}
    (hxy : ∀ i, quotientIInfToCoordinate (G := G) W i x =
      quotientIInfToCoordinate (G := G) W i y) :
    x = y

theorem

ker_quotientMapOfLE_comp_mk

L142 ↗

ProCGroups.Categorical.ker_quotientMapOfLE_comp_mk

Documentation

Kernel of the quotient map induced by M \(\le\) N, after precomposition with the quotient map from \(G\).

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem ker_quotientMapOfLE_comp_mk (M N : Subgroup G) [M.Normal] [N.Normal]
    (hMN : M ≤ N) :
    ((quotientMapOfLE (G := G) M N hMN).comp (QuotientGroup.mk' M)).ker = N

def

quotientInfToLeft

L151 ↗

ProCGroups.Categorical.quotientInfToLeft

Documentation

The left-hand map in the quotient pullback square.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

def quotientInfToLeft : G ⧸ (U ⊓ V) →* G ⧸ U

def

quotientInfToRight

L155 ↗

ProCGroups.Categorical.quotientInfToRight

Documentation

The right-hand map in the quotient pullback square.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

def quotientInfToRight : G ⧸ (U ⊓ V) →* G ⧸ V

def

quotientToSupLeft

L159 ↗

ProCGroups.Categorical.quotientToSupLeft

Documentation

The bottom-left map in the quotient pullback square.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

def quotientToSupLeft : G ⧸ U →* G ⧸ (U ⊔ V)

def

quotientToSupRight

L163 ↗

ProCGroups.Categorical.quotientToSupRight

Documentation

The bottom-right map in the quotient pullback square.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

def quotientToSupRight : G ⧸ V →* G ⧸ (U ⊔ V)

theorem

ker_quotientToSupLeft_comp_mk

L167 ↗

ProCGroups.Categorical.ker_quotientToSupLeft_comp_mk

Documentation

Kernel of the left quotient-to-sup map after precomposition with the quotient map from \(G\).

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem ker_quotientToSupLeft_comp_mk :
    ((quotientToSupLeft (G := G) U V).comp (QuotientGroup.mk' U)).ker = U ⊔ V

theorem

ker_quotientToSupRight_comp_mk

L175 ↗

ProCGroups.Categorical.ker_quotientToSupRight_comp_mk

Documentation

This lemma identifies the kernel of the right quotient-to-sup map after precomposition with the quotient map from \(G\).

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem ker_quotientToSupRight_comp_mk :
    ((quotientToSupRight (G := G) U V).comp (QuotientGroup.mk' V)).ker = U ⊔ V

def

quotientMapOfLECont

L180 ↗

ProCGroups.Categorical.quotientMapOfLECont

Documentation

The quotient map induced by an inclusion of normal subgroups is viewed as continuous.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

def quotientMapOfLECont
    {G : Type u} [Group G] [TopologicalSpace G]
    (M N : Subgroup G) [M.Normal] [N.Normal] (hMN : M ≤ N) :
    G ⧸ M →ₜ* G ⧸ N

theorem

quotientMapOfLECont_toMonoidHom

L192 ↗

ProCGroups.Categorical.quotientMapOfLECont_toMonoidHom

Documentation

The quotient map sends the class of an element to the class of its image under the underlying group homomorphism.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem quotientMapOfLECont_toMonoidHom
    {G : Type u} [Group G] [TopologicalSpace G]
    (M N : Subgroup G) [M.Normal] [N.Normal] (hMN : M ≤ N) :
    (quotientMapOfLECont (G := G) M N hMN).toMonoidHom =
      quotientMapOfLE (G := G) M N hMN

theorem

quotientMapOfLECont_mk

L203 ↗

ProCGroups.Categorical.quotientMapOfLECont_mk

Documentation

Evaluation of the continuous quotient map induced by inclusion on a quotient class.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem quotientMapOfLECont_mk
    {G : Type u} [Group G] [TopologicalSpace G]
    (M N : Subgroup G) [M.Normal] [N.Normal] (hMN : M ≤ N) (g : G) :
    quotientMapOfLECont (G := G) M N hMN (QuotientGroup.mk g) = QuotientGroup.mk g

def

quotientInfToPullback

L220 ↗

ProCGroups.Categorical.quotientInfToPullback

Documentation

The canonical map from \(G/(U \cap V)\) to the concrete pullback of \(G/U\) and \(G/V\) over \(G/(UV)\).

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

def quotientInfToPullback :
    G ⧸ (U ⊓ V) →*
      FiberProduct.carrier (quotientToSupLeft (G := G) U V) (quotientToSupRight (G := G) U V)

theorem

quotientInfToPullback_mk

L234 ↗

ProCGroups.Categorical.quotientInfToPullback_mk

Documentation

The quotient-to-pullback map sends a coset to the corresponding pair of quotient cosets.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem quotientInfToPullback_mk (g : G) :
    quotientInfToPullback (G := G) U V (QuotientGroup.mk g) =
      ⟨(QuotientGroup.mk g, QuotientGroup.mk g), rfl⟩

theorem

pullbackFst_quotientInfToPullback

L240 ↗

ProCGroups.Categorical.pullbackFst_quotientInfToPullback

Documentation

The first projection of the quotient-to-pullback map is the natural quotient map to \(G/U\).

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem pullbackFst_quotientInfToPullback :
    (FiberProduct.fst _ _).comp
        (quotientInfToPullback (G := G) U V) =
      quotientInfToLeft (G := G) U V

theorem

pullbackSnd_quotientInfToPullback

L251 ↗

ProCGroups.Categorical.pullbackSnd_quotientInfToPullback

Documentation

The second projection of the quotient-to-pullback map is the natural quotient map to \(G/V\).

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem pullbackSnd_quotientInfToPullback :
    (FiberProduct.snd _ _).comp
        (quotientInfToPullback (G := G) U V) =
      quotientInfToRight (G := G) U V

theorem

quotientInfToPullback_injective

L265 ↗

ProCGroups.Categorical.quotientInfToPullback_injective

Documentation

The canonical map from \(G/(U \cap V)\) to the pullback of \(G/U\) and \(G/V\) over \(G/(UV)\) is injective.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem quotientInfToPullback_injective :
    Function.Injective (quotientInfToPullback (G := G) U V)

theorem

quotientInfToPullback_surjective

L284 ↗

ProCGroups.Categorical.quotientInfToPullback_surjective

Documentation

The canonical map from the quotient by \(U \cap V\) to the pullback of the quotients by \(U\) and \(V\) is surjective.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem quotientInfToPullback_surjective :
    Function.Surjective (quotientInfToPullback (G := G) U V)

theorem

quotientInfToPullback_bijective

L338 ↗

ProCGroups.Categorical.quotientInfToPullback_bijective

Documentation

The canonical quotient-to-pullback map is bijective.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem quotientInfToPullback_bijective :
    Function.Bijective (quotientInfToPullback (G := G) U V)

def

quotientInfPullbackEquiv

L344 ↗

ProCGroups.Categorical.quotientInfPullbackEquiv

Documentation

The quotient square is canonically isomorphic to the pullback.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

def quotientInfPullbackEquiv :
    G ⧸ (U ⊓ V) ≃*
      FiberProduct.carrier (quotientToSupLeft (G := G) U V) (quotientToSupRight (G := G) U V)

theorem

quotientInfPullbackEquiv_fst

L351 ↗

ProCGroups.Categorical.quotientInfPullbackEquiv_fst

Documentation

The first coordinate of the quotient pullback equivalence is the natural map to \(G/U\).

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem quotientInfPullbackEquiv_fst :
    (FiberProduct.fst _ _).comp (quotientInfPullbackEquiv (G := G) U V).toMonoidHom =
      quotientInfToLeft (G := G) U V

theorem

quotientInfPullbackEquiv_snd

L359 ↗

ProCGroups.Categorical.quotientInfPullbackEquiv_snd

Documentation

The second coordinate of the quotient pullback equivalence is the natural map to \(G/V\).

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem quotientInfPullbackEquiv_snd :
    (FiberProduct.snd _ _).comp (quotientInfPullbackEquiv (G := G) U V).toMonoidHom =
      quotientInfToRight (G := G) U V

theorem

quotientInf_isPullback

L367 ↗

ProCGroups.Categorical.quotientInf_isPullback

Documentation

The quotient square is a pullback square.

Source context 4 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]

Lean source · statement

theorem quotientInf_isPullback :
    CategoryTheory.IsPullback
      (GrpCat.ofHom (quotientInfToLeft (G := G) U V))
      (GrpCat.ofHom (quotientInfToRight (G := G) U V))
      (GrpCat.ofHom (quotientToSupLeft (G := G) U V))
      (GrpCat.ofHom (quotientToSupRight (G := G) U V))

def

quotientInfToLeftCont

L392 ↗

ProCGroups.Categorical.quotientInfToLeftCont

Documentation

The left map in the continuous quotient square.

Source context 6 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]

Lean source · statement

def quotientInfToLeftCont : G ⧸ (U ⊓ V) →ₜ* G ⧸ U

def

quotientInfToRightCont

L396 ↗

ProCGroups.Categorical.quotientInfToRightCont

Documentation

The right map in the continuous quotient square.

Source context 6 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]

Lean source · statement

def quotientInfToRightCont : G ⧸ (U ⊓ V) →ₜ* G ⧸ V

def

quotientToSupLeftCont

L400 ↗

ProCGroups.Categorical.quotientToSupLeftCont

Documentation

The bottom-left map in the continuous quotient square.

Source context 6 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]

Lean source · statement

def quotientToSupLeftCont : G ⧸ U →ₜ* G ⧸ (U ⊔ V)

def

quotientToSupRightCont

L404 ↗

ProCGroups.Categorical.quotientToSupRightCont

Documentation

The bottom-right map in the continuous quotient square.

Source context 6 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]

Lean source · statement

def quotientToSupRightCont : G ⧸ V →ₜ* G ⧸ (U ⊔ V)

theorem

quotientInfToLeftCont_toMonoidHom

L410 ↗

ProCGroups.Categorical.quotientInfToLeftCont_toMonoidHom

Documentation

Forgetting continuity from the left continuous quotient-square map recovers the algebraic map.

Source context 6 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]

Lean source · statement

theorem quotientInfToLeftCont_toMonoidHom :
    (quotientInfToLeftCont (G := G) U V).toMonoidHom = quotientInfToLeft (G := G) U V

theorem

quotientInfToRightCont_toMonoidHom

L416 ↗

ProCGroups.Categorical.quotientInfToRightCont_toMonoidHom

Documentation

Forgetting continuity from the right continuous quotient-square map recovers the algebraic map.

Source context 6 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]

Lean source · statement

theorem quotientInfToRightCont_toMonoidHom :
    (quotientInfToRightCont (G := G) U V).toMonoidHom = quotientInfToRight (G := G) U V

theorem

quotientToSupLeftCont_toMonoidHom

L424 ↗

ProCGroups.Categorical.quotientToSupLeftCont_toMonoidHom

Documentation

Forgetting continuity from the lower-left continuous quotient-square map recovers the algebraic map.

Source context 6 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]

Lean source · statement

theorem quotientToSupLeftCont_toMonoidHom :
    (quotientToSupLeftCont (G := G) U V).toMonoidHom = quotientToSupLeft (G := G) U V

theorem

quotientToSupRightCont_toMonoidHom

L432 ↗

ProCGroups.Categorical.quotientToSupRightCont_toMonoidHom

Documentation

Forgetting continuity from the lower-right continuous quotient-square map recovers the algebraic map.

Source context 6 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]

Lean source · statement

theorem quotientToSupRightCont_toMonoidHom :
    (quotientToSupRightCont (G := G) U V).toMonoidHom = quotientToSupRight (G := G) U V

theorem

quotientInfToLeftCont_mk

L437 ↗

ProCGroups.Categorical.quotientInfToLeftCont_mk

Documentation

Evaluation of the left continuous quotient-square map on a quotient class.

Source context 6 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]

Lean source · statement

theorem quotientInfToLeftCont_mk (g : G) :
    quotientInfToLeftCont (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk g

theorem

quotientInfToRightCont_mk

L442 ↗

ProCGroups.Categorical.quotientInfToRightCont_mk

Documentation

Evaluation of the right continuous quotient-square map on a quotient class.

Source context 6 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]

Lean source · statement

theorem quotientInfToRightCont_mk (g : G) :
    quotientInfToRightCont (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk g

theorem

quotientToSupLeftCont_mk

L447 ↗

ProCGroups.Categorical.quotientToSupLeftCont_mk

Documentation

Evaluation of the lower-left continuous quotient-square map on a quotient class.

Source context 6 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]

Lean source · statement

theorem quotientToSupLeftCont_mk (g : G) :
    quotientToSupLeftCont (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk g

theorem

quotientToSupRightCont_mk

L452 ↗

ProCGroups.Categorical.quotientToSupRightCont_mk

Documentation

Evaluation of the lower-right continuous quotient-square map on a quotient class.

Source context 6 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]

Lean source · statement

theorem quotientToSupRightCont_mk (g : G) :
    quotientToSupRightCont (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk g

def

quotientInfToContinuousPullback

L462 ↗

ProCGroups.Categorical.quotientInfToContinuousPullback

Documentation

The canonical continuous map from \(G/(U \cap V)\) to the concrete continuous pullback of \(G/U\) and \(G/V\) over \(G/(UV)\).

Source context 7 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]
variable [IsTopologicalGroup G]

Lean source · statement

def quotientInfToContinuousPullback :
    G ⧸ (U ⊓ V) →ₜ*
      TopologicalFiberProduct.carrier (quotientToSupLeftCont (G := G) U V)
          (quotientToSupRightCont (G := G) U V)

theorem

quotientInfToContinuousPullback_toMonoidHom

L480 ↗

ProCGroups.Categorical.quotientInfToContinuousPullback_toMonoidHom

Documentation

Forgetting continuity from the continuous quotient-to-pullback map recovers the algebraic one.

Source context 8 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]
variable [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem quotientInfToContinuousPullback_toMonoidHom :
    (quotientInfToContinuousPullback (G := G) U V).toMonoidHom =
      quotientInfToPullback (G := G) U V

theorem

quotientInfToContinuousPullback_mk

L491 ↗

ProCGroups.Categorical.quotientInfToContinuousPullback_mk

Documentation

Evaluation formula for the continuous quotient-to-pullback map.

Source context 8 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]
variable [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem quotientInfToContinuousPullback_mk (g : G) :
    quotientInfToContinuousPullback (G := G) U V (QuotientGroup.mk g) =
      ⟨(QuotientGroup.mk g, QuotientGroup.mk g), rfl⟩

theorem

pullbackFstCont_quotientInfToContinuousPullback

L499 ↗

ProCGroups.Categorical.pullbackFstCont_quotientInfToContinuousPullback

Documentation

The first projection of the continuous quotient-to-pullback map is the natural quotient map to G/U.

Source context 8 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]
variable [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem pullbackFstCont_quotientInfToContinuousPullback :
    (TopologicalFiberProduct.fst _ _).comp (quotientInfToContinuousPullback (G := G) U V) =
      quotientInfToLeftCont (G := G) U V

theorem

pullbackSndCont_quotientInfToContinuousPullback

L511 ↗

ProCGroups.Categorical.pullbackSndCont_quotientInfToContinuousPullback

Documentation

The second projection of the continuous quotient-to-pullback map is the natural quotient map to G/V.

Source context 8 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]
variable [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem pullbackSndCont_quotientInfToContinuousPullback :
    (TopologicalFiberProduct.snd _ _).comp (quotientInfToContinuousPullback (G := G) U V) =
      quotientInfToRightCont (G := G) U V

theorem

quotientInfToContinuousPullback_injective

L522 ↗

ProCGroups.Categorical.quotientInfToContinuousPullback_injective

Documentation

Injectivity of the continuous quotient-to-pullback map on the underlying groups.

Source context 8 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]
variable [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem quotientInfToContinuousPullback_injective :
    Function.Injective (quotientInfToContinuousPullback (G := G) U V)

theorem

quotientInfToContinuousPullback_surjective

L533 ↗

ProCGroups.Categorical.quotientInfToContinuousPullback_surjective

Documentation

Surjectivity of the continuous quotient-to-pullback map on the underlying groups.

Source context 8 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]
variable [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem quotientInfToContinuousPullback_surjective :
    Function.Surjective (quotientInfToContinuousPullback (G := G) U V)

theorem

quotientInfToContinuousPullback_bijective

L545 ↗

ProCGroups.Categorical.quotientInfToContinuousPullback_bijective

Documentation

The continuous quotient-to-pullback map is bijective on the underlying groups.

Source context 8 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]
variable [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem quotientInfToContinuousPullback_bijective :
    Function.Bijective (quotientInfToContinuousPullback (G := G) U V)

def

quotientInfContinuousPullbackEquiv

L551 ↗

ProCGroups.Categorical.quotientInfContinuousPullbackEquiv

Documentation

The quotient square is canonically isomorphic to the concrete continuous fiber product.

Source context 7 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]
variable [IsTopologicalGroup G]

Lean source · statement

def quotientInfContinuousPullbackEquiv
    [CompactSpace G] [T2Space G]
    (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
    G ⧸ (U ⊓ V) ≃ₜ*
      TopologicalFiberProduct.carrier (quotientToSupLeftCont (G := G) U V)
          (quotientToSupRightCont (G := G) U V)

theorem

quotientInfContinuousPullbackEquiv_toContinuousMonoidHom

L563 ↗

ProCGroups.Categorical.quotientInfContinuousPullbackEquiv_toContinuousMonoidHom

Documentation

The quotient pullback equivalence is induced by the canonical comparison map.

Source context 7 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]
variable [IsTopologicalGroup G]

Lean source · statement

theorem quotientInfContinuousPullbackEquiv_toContinuousMonoidHom
    [CompactSpace G] [T2Space G]
    (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
    ContinuousMonoidHom.toContinuousMonoidHom (quotientInfContinuousPullbackEquiv
        (G := G) (U := U) (V := V) hUclosed hVclosed) =
      quotientInfToContinuousPullback (G := G) U V

theorem

quotientInfContinuousPullbackEquiv_mk

L575 ↗

ProCGroups.Categorical.quotientInfContinuousPullbackEquiv_mk

Documentation

Evaluation formula for the continuous quotient pullback equivalence on a quotient class.

Source context 7 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]
variable [IsTopologicalGroup G]

Lean source · statement

theorem quotientInfContinuousPullbackEquiv_mk
    [CompactSpace G] [T2Space G]
    (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) (g : G) :
    quotientInfContinuousPullbackEquiv (G := G) (U := U) (V := V) hUclosed hVclosed
      (QuotientGroup.mk g) = ⟨(QuotientGroup.mk g, QuotientGroup.mk g), rfl⟩

theorem

quotientInfContinuousPullbackEquiv_fst

L586 ↗

ProCGroups.Categorical.quotientInfContinuousPullbackEquiv_fst

Documentation

The first coordinate of the continuous quotient pullback equivalence is the natural map to G/U.

Source context 7 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]
variable [IsTopologicalGroup G]

Lean source · statement

theorem quotientInfContinuousPullbackEquiv_fst
    [CompactSpace G] [T2Space G]
    (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
    (TopologicalFiberProduct.fst _ _).comp
        (ContinuousMonoidHom.toContinuousMonoidHom (quotientInfContinuousPullbackEquiv
          (G := G) (U := U) (V := V) hUclosed hVclosed)) =
      quotientInfToLeftCont (G := G) U V

theorem

quotientInfContinuousPullbackEquiv_snd

L600 ↗

ProCGroups.Categorical.quotientInfContinuousPullbackEquiv_snd

Documentation

The second coordinate of the continuous quotient pullback equivalence is the natural map to G/V.

Source context 7 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]
variable [IsTopologicalGroup G]

Lean source · statement

theorem quotientInfContinuousPullbackEquiv_snd
    [CompactSpace G] [T2Space G]
    (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
    (TopologicalFiberProduct.snd _ _).comp
        (ContinuousMonoidHom.toContinuousMonoidHom (quotientInfContinuousPullbackEquiv
          (G := G) (U := U) (V := V) hUclosed hVclosed)) =
      quotientInfToRightCont (G := G) U V

theorem

quotientInf_hasProfiniteTestPullbackProperty

L614 ↗

ProCGroups.Categorical.quotientInf_hasProfiniteTestPullbackProperty

Documentation

For closed normal subgroups of a compact Hausdorff topological group, the quotient square has the universal property when tested against profinite source groups.

Source context 7 commands

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

namespace ProCGroups.Categorical
universe u v
variable {G : Type u} [Group G]
variable (U V : Subgroup G) [U.Normal] [V.Normal]
section
variable [TopologicalSpace G]
variable [IsTopologicalGroup G]

Lean source · statement

theorem quotientInf_hasProfiniteTestPullbackProperty
    [CompactSpace G] [T2Space G]
    (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
    HasProfiniteTestPullbackProperty
      (quotientInfToLeftCont (G := G) U V)
      (quotientInfToRightCont (G := G) U V)
      (quotientToSupLeftCont (G := G) U V)
      (quotientToSupRightCont (G := G) U V)

Module documentation

Pro C Groups / Categorical / Quotient Pullback Equivalences

Declarations