Module

Pullbacks.lean

Nyll.ProCGroups.ProC.Category.Pullbacks

2 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / pro-C / Category / Pullbacks

This module relates mathlib's CategoryTheory.IsPullback predicate in ProCGrp C to the concrete universal property tested against profinite source groups.

Imports3

Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Nyll.ProCGroups.Categorical.ProfinitePullbacks
Nyll.ProCGroups.ProC.Category.Basic

Imported by1

Nyll.ProCGroups.ProC.Category.All

theorem

isPullback_of_hasProfiniteTestPullbackProperty

L31 ↗

ProCGrp.isPullback_of_hasProfiniteTestPullbackProperty

Documentation

A continuous profinite-test pullback square is a pullback in ProCGrp.

Source context 7 commands

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

open CategoryTheory
open CategoryTheory.Limits
open ProCGroups.Categorical
universe u
namespace ProCGrp
variable {ProC : ProCGroups.FiniteGroupClass.{u}}
variable {G H H1 H2 : ProCGrp ProC}

Lean source · statement

theorem isPullback_of_hasProfiniteTestPullbackProperty
    {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
    {beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}
    (hpb : HasProfiniteTestPullbackProperty
      (continuousHom alpha1) (continuousHom alpha2)
      (continuousHom beta1) (continuousHom beta2)) :
    CategoryTheory.IsPullback alpha1 alpha2 beta1 beta2

theorem

hasProfiniteTestPullbackProperty_of_isPullback_allFinite

L92 ↗

ProCGrp.hasProfiniteTestPullbackProperty_of_isPullback_allFinite