NYLL
Module

UniversalProperty.lean

Nyll.ProCGroups.FreeProducts.UniversalProperty
18 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / Free Products / Universal Property

This module defines the binary free pro-C universal property and its canonical comparison maps and equivalences.

Imports1
Imported by2

Declarations

structure

IsFreeProCProduct

L33 ↗
ProCGroups.FreeProducts.IsFreeProCProduct
Documentation

Binary free pro-\(C\) products via the strengthened universal property used elsewhere in the project: every pair of continuous homomorphisms into a pro-\(C\) target extends uniquely.

Source context 8 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
Lean source · full declaration
structure IsFreeProCProduct
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    (ι₁ : G₁ →ₜ* F) (ι₂ : G₂ →ₜ* F) : Prop where
  /--
  Open normal subgroups with quotients in `C` form a neighborhood basis at one in the proposed
  free product.
  -/
  hasOpenNormalBasisInClass : ProCGroups.ProC.HasOpenNormalBasisInClass C F
  /--
  Any pair of continuous homomorphisms from the two factors into a pro-`C` target extends to a
  unique continuous homomorphism from `F`, with the two prescribed composites.
  -/
  existsUnique_lift :
    ∀ {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
      [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K],
    ProCGroups.ProC.HasOpenNormalBasisInClass C (K) →
      ∀ (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K),
        ∃! φ : F →ₜ* K, φ.comp ι₁ = φ₁ ∧ φ.comp ι₂ = φ₂
def

lift

L59 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.lift
Documentation

The universal property selects a descent morphism from a binary free product object.

Source context 11 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
Lean source · statement
def lift (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    (hK : ProCGroups.ProC.HasOpenNormalBasisInClass C (K))
    (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K) : F →ₜ* K
theorem

lift_spec

L68 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.lift_spec
Documentation

The chosen free-product descent morphism has the prescribed composites.

Source context 12 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
omit [IsTopologicalGroup F] in
Lean source · statement
theorem lift_spec (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    (hK : ProCGroups.ProC.HasOpenNormalBasisInClass C (K))
    (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K) :
    (hF.lift hK φ₁ φ₂).comp ι₁ = φ₁ ∧ (hF.lift hK φ₁ φ₂).comp ι₂ = φ₂
theorem

lift_left

L78 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.lift_left
Documentation

The left composite of the chosen free-product descent morphism is the prescribed left leg.

Source context 12 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
omit [IsTopologicalGroup F] in
Lean source · statement
theorem lift_left (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    (hK : ProCGroups.ProC.HasOpenNormalBasisInClass C (K))
    (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K) :
    (hF.lift hK φ₁ φ₂).comp ι₁ = φ₁
theorem

lift_right

L88 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.lift_right
Documentation

The right composite of the chosen free-product descent morphism is the prescribed right leg.

Source context 12 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
omit [IsTopologicalGroup F] in
Lean source · statement
theorem lift_right (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    (hK : ProCGroups.ProC.HasOpenNormalBasisInClass C (K))
    (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K) :
    (hF.lift hK φ₁ φ₂).comp ι₂ = φ₂
theorem

lift_unique

L98 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.lift_unique
Documentation

Uniqueness of the chosen free-product descent morphism.

Source context 12 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
omit [IsTopologicalGroup F] in
Lean source · statement
theorem lift_unique (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    (hK : ProCGroups.ProC.HasOpenNormalBasisInClass C (K))
    (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K)
    {ψ : F →ₜ* K} (hψ : ψ.comp ι₁ = φ₁ ∧ ψ.comp ι₂ = φ₂) :
    ψ = hF.lift hK φ₁ φ₂
theorem

lift_self

L110 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.lift_self
Documentation

The distinguished descent map from a free product object to itself is the identity.

Source context 11 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
Lean source · statement
theorem lift_self (hF : IsFreeProCProduct (C := C) ι₁ ι₂) :
    hF.lift hF.hasOpenNormalBasisInClass ι₁ ι₂ = ContinuousMonoidHom.id F
theorem

hom_ext

L119 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.hom_ext
Documentation

Homomorphisms out of a free-product object are equal when they agree on the canonical factors.

Source context 12 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
omit [IsTopologicalGroup F] in
Lean source · statement
theorem hom_ext (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    (hK : ProCGroups.ProC.HasOpenNormalBasisInClass C (K))
    {ψ ψ' : F →ₜ* K}
    (h₁ : ψ.comp ι₁ = ψ'.comp ι₁) (h₂ : ψ.comp ι₂ = ψ'.comp ι₂) :
    ψ = ψ'
def

compare

L137 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.compare
Documentation

The canonical comparison morphism between two free product objects on the same pair of factors.

Source context 14 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι₁' : G₁ →ₜ* F'} {ι₂' : G₂ →ₜ* F'}
Lean source · statement
def compare (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
    (hF' : IsFreeProCProduct (C := C) ι₁' ι₂') :
    F →ₜ* F'
theorem

compare_left

L147 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.compare_left
Documentation

The left composite of the canonical comparison map between free product objects is the prescribed left leg.

Source context 15 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι₁' : G₁ →ₜ* F'} {ι₂' : G₂ →ₜ* F'}
omit [IsTopologicalGroup F] in
Lean source · statement
theorem compare_left (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
    (hF' : IsFreeProCProduct (C := C) ι₁' ι₂') :
    (hF.compare hF').comp ι₁ = ι₁'
theorem

compare_right

L157 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.compare_right
Documentation

The right composite of the canonical comparison map between free product objects is the prescribed right leg.

Source context 15 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι₁' : G₁ →ₜ* F'} {ι₂' : G₂ →ₜ* F'}
omit [IsTopologicalGroup F] in
Lean source · statement
theorem compare_right (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
    (hF' : IsFreeProCProduct (C := C) ι₁' ι₂') :
    (hF.compare hF').comp ι₂ = ι₂'
theorem

compare_self

L163 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.compare_self
Documentation

The canonical comparison map from a free product object to itself is the identity.

Source context 14 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι₁' : G₁ →ₜ* F'} {ι₂' : G₂ →ₜ* F'}
Lean source · statement
theorem compare_self (hF : IsFreeProCProduct (C := C) ι₁ ι₂) :
    hF.compare hF = ContinuousMonoidHom.id F
theorem

compare_comp

L173 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.compare_comp
Documentation

Composition of free-product comparison maps is the expected direct comparison map.

Source context 18 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι₁' : G₁ →ₜ* F'} {ι₂' : G₂ →ₜ* F'}
variable {F'' : Type u} [Group F''] [TopologicalSpace F''] [IsTopologicalGroup F'']
variable [CompactSpace F''] [T2Space F''] [TotallyDisconnectedSpace F'']
variable {ι₁'' : G₁ →ₜ* F''} {ι₂'' : G₂ →ₜ* F''}
omit [IsTopologicalGroup F] in
Lean source · statement
theorem compare_comp (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
    (hF' : IsFreeProCProduct (C := C) ι₁' ι₂')
    (hF'' : IsFreeProCProduct (C := C) ι₁'' ι₂'') :
    (hF'.compare hF'').comp (hF.compare hF') = hF.compare hF''
def

equiv

L192 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.equiv
Documentation

Any two binary free product objects on the same factors are canonically isomorphic.

Source context 17 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι₁' : G₁ →ₜ* F'} {ι₂' : G₂ →ₜ* F'}
variable {F'' : Type u} [Group F''] [TopologicalSpace F''] [IsTopologicalGroup F'']
variable [CompactSpace F''] [T2Space F''] [TotallyDisconnectedSpace F'']
variable {ι₁'' : G₁ →ₜ* F''} {ι₂'' : G₂ →ₜ* F''}
Lean source · statement
def equiv (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
    (hF' : IsFreeProCProduct (C := C) ι₁' ι₂') :
    F ≃ₜ* F'
theorem

equiv_left

L227 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.equiv_left
Documentation

The left composite of the canonical equivalence between free-product objects is the canonical left map.

Source context 17 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι₁' : G₁ →ₜ* F'} {ι₂' : G₂ →ₜ* F'}
variable {F'' : Type u} [Group F''] [TopologicalSpace F''] [IsTopologicalGroup F'']
variable [CompactSpace F''] [T2Space F''] [TotallyDisconnectedSpace F'']
variable {ι₁'' : G₁ →ₜ* F''} {ι₂'' : G₂ →ₜ* F''}
Lean source · statement
theorem equiv_left (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
    (hF' : IsFreeProCProduct (C := C) ι₁' ι₂') :
    ((hF.equiv hF' : F →ₜ* F').comp ι₁) = ι₁'
theorem

equiv_right

L236 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.equiv_right
Documentation

The right composite of the canonical equivalence between free product objects is the prescribed right leg.

Source context 17 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι₁' : G₁ →ₜ* F'} {ι₂' : G₂ →ₜ* F'}
variable {F'' : Type u} [Group F''] [TopologicalSpace F''] [IsTopologicalGroup F'']
variable [CompactSpace F''] [T2Space F''] [TotallyDisconnectedSpace F'']
variable {ι₁'' : G₁ →ₜ* F''} {ι₂'' : G₂ →ₜ* F''}
Lean source · statement
theorem equiv_right (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
    (hF' : IsFreeProCProduct (C := C) ι₁' ι₂') :
    ((hF.equiv hF' : F →ₜ* F').comp ι₂) = ι₂'
theorem

equiv_symm_left

L242 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.equiv_symm_left
Documentation

Left-leg formula for the inverse canonical free-product equivalence.

Source context 17 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι₁' : G₁ →ₜ* F'} {ι₂' : G₂ →ₜ* F'}
variable {F'' : Type u} [Group F''] [TopologicalSpace F''] [IsTopologicalGroup F'']
variable [CompactSpace F''] [T2Space F''] [TotallyDisconnectedSpace F'']
variable {ι₁'' : G₁ →ₜ* F''} {ι₂'' : G₂ →ₜ* F''}
Lean source · statement
theorem equiv_symm_left (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
    (hF' : IsFreeProCProduct (C := C) ι₁' ι₂') :
    (((hF.equiv hF').symm : F' →ₜ* F).comp ι₁') = ι₁
theorem

equiv_symm_right

L249 ↗
ProCGroups.FreeProducts.IsFreeProCProduct.equiv_symm_right
Documentation

Right-leg formula for the inverse canonical free-product equivalence.

Source context 17 commands

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

namespace ProCGroups.FreeProducts
universe u
section FreeProCProducts
variable {C : ProCGroups.FiniteGroupClass}
variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
variable [Group G₁] [TopologicalSpace G₁]
variable [Group G₂] [TopologicalSpace G₂]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
namespace IsFreeProCProduct
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
variable {ι₁' : G₁ →ₜ* F'} {ι₂' : G₂ →ₜ* F'}
variable {F'' : Type u} [Group F''] [TopologicalSpace F''] [IsTopologicalGroup F'']
variable [CompactSpace F''] [T2Space F''] [TotallyDisconnectedSpace F'']
variable {ι₁'' : G₁ →ₜ* F''} {ι₂'' : G₂ →ₜ* F''}
Lean source · statement
theorem equiv_symm_right (hF : IsFreeProCProduct (C := C) ι₁ ι₂)
    (hF' : IsFreeProCProduct (C := C) ι₁' ι₂') :
    (((hF.equiv hF').symm : F' →ₜ* F).comp ι₂') = ι₂

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