NYLL
Module

PushoutSquares.lean

Nyll.ProCGroups.Categorical.PushoutSquares
30 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / Categorical / Pushout Squares

This module constructs algebraic group pushouts from free products and normal closures, and develops algebraic and profinite-tested pushout universal properties.

Imports5
Imported by1

Declarations

abbrev

PushoutFreeProduct

L33 ↗
ProCGroups.Categorical.PushoutFreeProduct
Documentation

The abstract free product used as the carrier before imposing pushout relations.

Source context 7 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
Lean source · statement
abbrev PushoutFreeProduct (H₁ H₂ : Type u) [Group H₁] [Group H₂]
def

pushoutRelators

L37 ↗
ProCGroups.Categorical.pushoutRelators
Documentation

The relators identifying the two legs of a group cospan inside the free product.

Source context 7 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
Lean source · statement
def pushoutRelators (β₁ : H →* H₁) (β₂ : H →* H₂) :
    Set (PushoutFreeProduct H₁ H₂)
def

pushoutNormalClosure

L44 ↗
ProCGroups.Categorical.pushoutNormalClosure
Documentation

The normal subgroup generated by the cospan-identifying relators.

Source context 7 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
Lean source · statement
def pushoutNormalClosure (β₁ : H →* H₁) (β₂ : H →* H₂) :
    Subgroup (PushoutFreeProduct H₁ H₂)
instance

pushoutNormalClosure_normal

L49 ↗
ProCGroups.Categorical.pushoutNormalClosure_normal
Documentation

The relator closure used in the concrete pushout is normal.

Source context 7 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
Lean source · statement
instance pushoutNormalClosure_normal (β₁ : H →* H₁) (β₂ : H →* H₂) :
    (pushoutNormalClosure β₁ β₂).Normal
abbrev

Carrier

L59 ↗
ProCGroups.Categorical.AlgebraicPushout.Carrier
Documentation

Algebraic group pushout carrier: the free product modulo the normal closure of \(\operatorname{inl}(\beta_1 h)^{-1} * \operatorname{inr}(\beta_2 h)\).

Source context 8 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
namespace AlgebraicPushout
Lean source · statement
abbrev Carrier (β₁ : H →* H₁) (β₂ : H →* H₂)
def

inl

L63 ↗
ProCGroups.Categorical.AlgebraicPushout.inl
Documentation

The left structural map into the algebraic pushout.

Source context 8 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
namespace AlgebraicPushout
Lean source · statement
def inl (β₁ : H →* H₁) (β₂ : H →* H₂) :
    H₁ →* Carrier β₁ β₂
def

inr

L68 ↗
ProCGroups.Categorical.AlgebraicPushout.inr
Documentation

The right structural map into the algebraic pushout.

Source context 8 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
namespace AlgebraicPushout
Lean source · statement
def inr (β₁ : H →* H₁) (β₂ : H →* H₂) :
    H₂ →* Carrier β₁ β₂
theorem

inl_comp_eq_inr_comp

L73 ↗
ProCGroups.Categorical.AlgebraicPushout.inl_comp_eq_inr_comp
Documentation

The algebraic pushout maps coequalize the original cospan.

Source context 8 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
namespace AlgebraicPushout
Lean source · statement
theorem inl_comp_eq_inr_comp
    (β₁ : H →* H₁) (β₂ : H →* H₂) :
    (inl β₁ β₂).comp β₁ = (inr β₁ β₂).comp β₂
def

concretePushoutDesc

L88 ↗
ProCGroups.Categorical.AlgebraicPushout.concretePushoutDesc
Documentation

The concrete pushout descent map is characterized by its compatibility with the two canonical inclusions.

Source context 8 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
namespace AlgebraicPushout
Lean source · statement
def concretePushoutDesc
    (β₁ : H →* H₁) (β₂ : H →* H₂)
    {K : Type u} [Group K]
    (φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
    (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
    Carrier β₁ β₂ →* K
theorem

concretePushoutDesc_inl

L112 ↗
ProCGroups.Categorical.AlgebraicPushout.concretePushoutDesc_inl
Documentation

The concrete pushout descent map is compatible with the left inclusion.

Source context 8 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
namespace AlgebraicPushout
Lean source · statement
theorem concretePushoutDesc_inl
    (β₁ : H →* H₁) (β₂ : H →* H₂)
    {K : Type u} [Group K]
    (φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
    (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
    (concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp (inl β₁ β₂) = φ₁
theorem

concretePushoutDesc_inr

L124 ↗
ProCGroups.Categorical.AlgebraicPushout.concretePushoutDesc_inr
Documentation

The concrete pushout descent map is compatible with the right inclusion.

Source context 8 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
namespace AlgebraicPushout
Lean source · statement
theorem concretePushoutDesc_inr
    (β₁ : H →* H₁) (β₂ : H →* H₂)
    {K : Type u} [Group K]
    (φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
    (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
    (concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp (inr β₁ β₂) = φ₂
theorem

isPushout

L138 ↗
ProCGroups.Categorical.AlgebraicPushout.isPushout
Documentation

The concrete free-product quotient is a pushout in mathlib's category of groups.

Source context 7 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
Lean source · statement
theorem AlgebraicPushout.isPushout (β₁ : H →* H₁) (β₂ : H →* H₂) :
    CategoryTheory.IsPushout
      (GrpCat.ofHom β₁) (GrpCat.ofHom β₂)
      (GrpCat.ofHom (AlgebraicPushout.inl β₁ β₂))
      (GrpCat.ofHom (AlgebraicPushout.inr β₁ β₂))
def

HasProfiniteTestPushoutProperty

L232 ↗
ProCGroups.Categorical.HasProfiniteTestPushoutProperty
Documentation

Continuous pushout property tested by profinite target objects.

This definition does not assert that the four objects in the square are themselves profinite.

Source context 13 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
Lean source · statement
def HasProfiniteTestPushoutProperty (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
    (α₁ : H₁ →ₜ* G) (α₂ : H₂ →ₜ* G) : Prop
def

pushoutDescCont

L242 ↗
ProCGroups.Categorical.pushoutDescCont
Documentation

Chosen continuous morphism induced by the profinite pushout universal property.

Source context 13 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
Lean source · statement
def pushoutDescCont
    {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
    (hφ : φ₁.comp β₁ = φ₂.comp β₂) : G →ₜ* K
theorem

pushoutDescCont_spec

L256 ↗
ProCGroups.Categorical.pushoutDescCont_spec
Documentation

Specification of the chosen continuous pushout descent map.

Source context 14 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
omit [IsTopologicalGroup G] [IsTopologicalGroup H]
    [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem pushoutDescCont_spec
    {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
    (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
    (pushoutDescCont hpo φ₁ φ₂ hφ).comp α₁ = φ₁ ∧
      (pushoutDescCont hpo φ₁ φ₂ hφ).comp α₂ = φ₂
theorem

pushoutDescCont_left

L273 ↗
ProCGroups.Categorical.pushoutDescCont_left
Documentation

Left composite of the chosen continuous pushout descent map.

Source context 14 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
omit [IsTopologicalGroup G] [IsTopologicalGroup H]
    [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem pushoutDescCont_left
    {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
    (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
    (pushoutDescCont hpo φ₁ φ₂ hφ).comp α₁ = φ₁
theorem

pushoutDescCont_right

L289 ↗
ProCGroups.Categorical.pushoutDescCont_right
Documentation

Right composite of the chosen continuous pushout descent map.

Source context 14 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
omit [IsTopologicalGroup G] [IsTopologicalGroup H]
    [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem pushoutDescCont_right
    {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
    (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
    (pushoutDescCont hpo φ₁ φ₂ hφ).comp α₂ = φ₂
theorem

pushoutDescCont_uniq

L304 ↗
ProCGroups.Categorical.pushoutDescCont_uniq
Documentation

Uniqueness of the chosen continuous pushout descent map.

Source context 14 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
omit [IsTopologicalGroup G] [IsTopologicalGroup H]
    [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem pushoutDescCont_uniq
    {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
    (hφ : φ₁.comp β₁ = φ₂.comp β₂)
    {ψ : G →ₜ* K}
    (hψ : ψ.comp α₁ = φ₁ ∧ ψ.comp α₂ = φ₂) :
    ψ = pushoutDescCont hpo φ₁ φ₂ hφ
theorem

pushoutDescCont_self

L320 ↗
ProCGroups.Categorical.pushoutDescCont_self
Documentation

The distinguished map from a profinite pushout object to itself is the identity.

Source context 14 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
Lean source · statement
theorem pushoutDescCont_self
    {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    : pushoutDescCont hpo α₁ α₂ hpo.1 = ContinuousMonoidHom.id G
theorem

pushoutCont_hom_ext

L334 ↗
ProCGroups.Categorical.pushoutCont_hom_ext
Documentation

Extensionality of continuous morphisms out of a profinite pushout object.

Source context 14 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
omit [IsTopologicalGroup G] [IsTopologicalGroup H]
    [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem pushoutCont_hom_ext
    {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    {ψ ψ' : G →ₜ* K}
    (h₁ : ψ.comp α₁ = ψ'.comp α₁)
    (h₂ : ψ.comp α₂ = ψ'.comp α₂) :
    ψ = ψ'
def

pushoutContMapOfIsPushout

L358 ↗
ProCGroups.Categorical.pushoutContMapOfIsPushout
Documentation

Canonical comparison map between two profinite pushout objects of the same cospan.

Source context 13 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
Lean source · statement
def pushoutContMapOfIsPushout
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
    (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
    : G →ₜ* G'
theorem

pushoutContMapOfIsPushout_self

L369 ↗
ProCGroups.Categorical.pushoutContMapOfIsPushout_self
Documentation

The canonical comparison map from a profinite pushout object to itself is the identity.

Source context 14 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
Lean source · statement
theorem pushoutContMapOfIsPushout_self
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    : pushoutContMapOfIsPushout β₁ β₂ hpo hpo = ContinuousMonoidHom.id G
theorem

pushoutContMapOfIsPushout_left

L382 ↗
ProCGroups.Categorical.pushoutContMapOfIsPushout_left
Documentation

Left composite of the canonical comparison map between profinite pushout objects.

Source context 14 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
omit [IsTopologicalGroup G] [IsTopologicalGroup H]
    [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem pushoutContMapOfIsPushout_left
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
    (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
    : (pushoutContMapOfIsPushout β₁ β₂ hpo hpo').comp α₁ = α₁'
theorem

pushoutContMapOfIsPushout_right

L398 ↗
ProCGroups.Categorical.pushoutContMapOfIsPushout_right
Documentation

Right composite of the canonical comparison map between profinite pushout objects.

Source context 14 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
omit [IsTopologicalGroup G] [IsTopologicalGroup H]
    [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem pushoutContMapOfIsPushout_right
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
    (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
    : (pushoutContMapOfIsPushout β₁ β₂ hpo hpo').comp α₂ = α₂'
theorem

bijective_pushoutContMapOfIsPushout

L412 ↗
ProCGroups.Categorical.bijective_pushoutContMapOfIsPushout
Documentation

Any two profinite pushout objects of the same cospan are canonically bijective.

Source context 14 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
Lean source · statement
theorem bijective_pushoutContMapOfIsPushout
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
    (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
    : Function.Bijective (pushoutContMapOfIsPushout β₁ β₂ hpo hpo')
def

pushoutContEquivOfIsPushout

L457 ↗
ProCGroups.Categorical.pushoutContEquivOfIsPushout
Documentation

Canonical continuous multiplicative equivalence between two profinite pushout objects.

Source context 13 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
Lean source · statement
def pushoutContEquivOfIsPushout
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
    (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
    : G ≃ₜ* G'
theorem

pushoutContEquivOfIsPushout_left

L472 ↗
ProCGroups.Categorical.pushoutContEquivOfIsPushout_left
Documentation

Left composite of the canonical continuous pushout equivalence.

Source context 14 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
Lean source · statement
theorem pushoutContEquivOfIsPushout_left
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
    (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
    : ((pushoutContEquivOfIsPushout β₁ β₂ hpo hpo' : G →ₜ* G').comp α₁) = α₁'
theorem

pushoutContEquivOfIsPushout_right

L485 ↗
ProCGroups.Categorical.pushoutContEquivOfIsPushout_right
Documentation

Right composite of the canonical continuous pushout equivalence.

Source context 14 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
Lean source · statement
theorem pushoutContEquivOfIsPushout_right
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
    (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
    : ((pushoutContEquivOfIsPushout β₁ β₂ hpo hpo' : G →ₜ* G').comp α₂) = α₂'
theorem

pushoutContEquivOfIsPushout_symm_left

L497 ↗
ProCGroups.Categorical.pushoutContEquivOfIsPushout_symm_left
Documentation

Left-leg formula for the inverse profinite pushout comparison equivalence.

Source context 14 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
Lean source · statement
theorem pushoutContEquivOfIsPushout_symm_left
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
    (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
    : (((pushoutContEquivOfIsPushout β₁ β₂ hpo hpo').symm : G' →ₜ* G).comp α₁') = α₁
theorem

pushoutContEquivOfIsPushout_symm_right

L523 ↗
ProCGroups.Categorical.pushoutContEquivOfIsPushout_symm_right
Documentation

Right-leg formula for the inverse profinite pushout comparison equivalence.

Source context 14 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
open scoped Monoid.Coprod
universe u v
section
variable {G G' H H₁ H₂ : Type u}
variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
variable [TopologicalSpace H₁] [TopologicalSpace H₂]
variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
Lean source · statement
theorem pushoutContEquivOfIsPushout_symm_right
    {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
    {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
    (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
    (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
    (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
    : (((pushoutContEquivOfIsPushout β₁ β₂ hpo hpo').symm : G' →ₜ* G).comp α₂') = α₂

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