Module

PullbackComparison.lean

Nyll.ProCGroups.Categorical.PullbackComparison

21 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / Categorical / Pullback Comparison

This module compares a profinite-tested continuous pullback square with its concrete fiber product and transports bijectivity and kernel criteria across the canonical comparison map.

Imports1

Nyll.ProCGroups.Categorical.ProfinitePullbacks

Imported by1

Nyll.ProCGroups.Categorical.All

def

toContinuousPullbackOfIsPullback

L40 ↗

ProCGroups.Categorical.toContinuousPullbackOfIsPullback

Documentation

The canonical comparison map from a profinite-tested pullback square to the concrete continuous fiber product.

Source context 12 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]

Lean source · statement

def toContinuousPullbackOfIsPullback
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
    G →ₜ* TopologicalFiberProduct.carrier β₁ β₂

theorem

toContinuousPullbackOfIsPullback_self

L55 ↗

ProCGroups.Categorical.toContinuousPullbackOfIsPullback_self

Documentation

The canonical comparison map from the concrete continuous fiber product to itself is the identity.

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
  [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
  [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
  [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂] in

Lean source · statement

theorem toContinuousPullbackOfIsPullback_self
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
    toContinuousPullbackOfIsPullback (TopologicalFiberProduct.fst β₁ β₂)
        (TopologicalFiberProduct.snd β₁ β₂) β₁ β₂
        (TopologicalFiberProduct.hasProfiniteTestPullbackProperty β₁ β₂) =
      ContinuousMonoidHom.id (TopologicalFiberProduct.carrier β₁ β₂)

theorem

fst_toContinuousPullbackOfIsPullback

L77 ↗

ProCGroups.Categorical.TopologicalFiberProduct.fst_toContinuousPullbackOfIsPullback

Documentation

The first coordinate of the canonical comparison map recovers the first leg of the square.

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup G] [IsTopologicalGroup H] [IsTopologicalGroup H₁]
  [IsTopologicalGroup H₂]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
  [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
  [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
  [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂] in

Lean source · statement

theorem TopologicalFiberProduct.fst_toContinuousPullbackOfIsPullback
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
    (TopologicalFiberProduct.fst β₁ β₂).comp (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)
        = α₁

theorem

snd_toContinuousPullbackOfIsPullback

L93 ↗

ProCGroups.Categorical.TopologicalFiberProduct.snd_toContinuousPullbackOfIsPullback

Documentation

The second coordinate of the canonical comparison map recovers the second leg of the square.

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup G] [IsTopologicalGroup H] [IsTopologicalGroup H₁]
  [IsTopologicalGroup H₂]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
  [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
  [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
  [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂] in

Lean source · statement

theorem TopologicalFiberProduct.snd_toContinuousPullbackOfIsPullback
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
    (TopologicalFiberProduct.snd β₁ β₂).comp (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)
        = α₂

def

fromContinuousPullbackOfIsPullback

L106 ↗

ProCGroups.Categorical.fromContinuousPullbackOfIsPullback

Documentation

The canonical inverse comparison map from the concrete continuous fiber product to a profinite-tested pullback square.

Source context 12 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]

Lean source · statement

def fromContinuousPullbackOfIsPullback
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
    TopologicalFiberProduct.carrier β₁ β₂ →ₜ* G

theorem

fromContinuousPullbackOfIsPullback_spec

L120 ↗

ProCGroups.Categorical.fromContinuousPullbackOfIsPullback_spec

Documentation

Specification of the inverse comparison map from the concrete pullback.

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup G] [IsTopologicalGroup H]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
  [CompactSpace H] [TotallyDisconnectedSpace H] in

Lean source · statement

theorem fromContinuousPullbackOfIsPullback_spec
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
    α₁.comp (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) =
        TopologicalFiberProduct.fst β₁ β₂ ∧
      α₂.comp (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) =
        TopologicalFiberProduct.snd β₁ β₂

theorem

fromContinuousPullbackOfIsPullback_uniq

L147 ↗

ProCGroups.Categorical.fromContinuousPullbackOfIsPullback_uniq

Documentation

Uniqueness of the inverse comparison map from the concrete pullback.

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup G] [IsTopologicalGroup H]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
  [CompactSpace H] [TotallyDisconnectedSpace H] in

Lean source · statement

theorem fromContinuousPullbackOfIsPullback_uniq
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
    {ψ : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* G}
    (hψ : α₁.comp ψ = TopologicalFiberProduct.fst β₁ β₂ ∧ α₂.comp ψ =
        TopologicalFiberProduct.snd β₁ β₂) :
    ψ = fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb

theorem

fromContinuousPullback_comp_toContinuousPullbackOfIsPullback

L163 ↗

ProCGroups.Categorical.fromContinuousPullback_comp_toContinuousPullbackOfIsPullback

Documentation

Composing the inverse comparison map with the canonical map gives the identity.

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in

Lean source · statement

theorem fromContinuousPullback_comp_toContinuousPullbackOfIsPullback
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
    (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
        (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) =
      ContinuousMonoidHom.id G

theorem

toContinuousPullback_comp_fromContinuousPullbackOfIsPullback

L212 ↗

ProCGroups.Categorical.toContinuousPullback_comp_fromContinuousPullbackOfIsPullback

Documentation

Composing the canonical map with the inverse comparison map gives the identity.

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup G] [IsTopologicalGroup H]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
  [CompactSpace H] [TotallyDisconnectedSpace H] in

Lean source · statement

theorem toContinuousPullback_comp_fromContinuousPullbackOfIsPullback
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
    (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
        (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) =
      ContinuousMonoidHom.id (TopologicalFiberProduct.carrier β₁ β₂)

theorem

fromContinuousPullbackOfIsPullback_toContinuousPullbackOfIsPullback_apply

L243 ↗

ProCGroups.Categorical.fromContinuousPullbackOfIsPullback_toContinuousPullbackOfIsPullback_apply

Documentation

Pointwise left-inverse formula for the canonical comparison maps.

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in

Lean source · statement

theorem fromContinuousPullbackOfIsPullback_toContinuousPullbackOfIsPullback_apply
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) (g : G) :
    fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb
      (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb g) = g

theorem

toContinuousPullbackOfIsPullback_fromContinuousPullbackOfIsPullback_apply

L256 ↗

ProCGroups.Categorical.toContinuousPullbackOfIsPullback_fromContinuousPullbackOfIsPullback_apply

Documentation

Pointwise right-inverse formula for the canonical comparison maps.

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup G] [IsTopologicalGroup H]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
  [CompactSpace H] [TotallyDisconnectedSpace H] in

Lean source · statement

theorem toContinuousPullbackOfIsPullback_fromContinuousPullbackOfIsPullback_apply
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) (x : TopologicalFiberProduct.carrier β₁
        β₂) :
    toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb
      (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb x) = x

theorem

bijective_toContinuousPullbackOfIsPullback

L269 ↗

ProCGroups.Categorical.bijective_toContinuousPullbackOfIsPullback

Documentation

The canonical comparison map from a profinite-tested pullback square is bijective.

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in

Lean source · statement

theorem bijective_toContinuousPullbackOfIsPullback
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
    Function.Bijective (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)

theorem

toContinuousPullbackOfIsPullback_comp_pullbackDescCont

L301 ↗

ProCGroups.Categorical.toContinuousPullbackOfIsPullback_comp_pullbackDescCont

Documentation

The canonical comparison map sends the chosen pullback descent map to the concrete continuous pullback lift.

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup G] [IsTopologicalGroup H] [IsTopologicalGroup H₁]
  [IsTopologicalGroup H₂]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
  [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
  [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
  [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂] in

Lean source · full declaration

theorem toContinuousPullbackOfIsPullback_comp_pullbackDescCont
    {A : Type u} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
    [CompactSpace A] [T2Space A] [TotallyDisconnectedSpace A]
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
    (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
    (hφ : β₁.comp φ₁ = β₂.comp φ₂) :
    (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
        (pullbackDescCont hpb φ₁ φ₂ hφ) =
      TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hφ a) := by
  apply TopologicalFiberProduct.hom_ext
  · intro a
    have hleft :
        (TopologicalFiberProduct.fst β₁ β₂).comp
            ((toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
              (pullbackDescCont hpb φ₁ φ₂ hφ)) = φ₁ := by
      calc
        (TopologicalFiberProduct.fst β₁ β₂).comp
            ((toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
              (pullbackDescCont hpb φ₁ φ₂ hφ)) =
            ((TopologicalFiberProduct.fst β₁ β₂).comp
              (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)).comp
                (pullbackDescCont hpb φ₁ φ₂ hφ) := by
                  rfl
        _ = α₁.comp (pullbackDescCont hpb φ₁ φ₂ hφ) := by
              rw [TopologicalFiberProduct.fst_toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb]
        _ = φ₁ := pullbackDescCont_left hpb φ₁ φ₂ hφ
    have hright :
        (TopologicalFiberProduct.fst β₁ β₂).comp
            (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hφ a)) = φ₁ :=
      TopologicalFiberProduct.fst_lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hφ a)
    exact congrArg (fun f : A →ₜ* H₁ => f a) (hleft.trans hright.symm)
  · intro a
    have hleft :
        (TopologicalFiberProduct.snd β₁ β₂).comp
            ((toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
              (pullbackDescCont hpb φ₁ φ₂ hφ)) = φ₂ := by
      calc
        (TopologicalFiberProduct.snd β₁ β₂).comp
            ((toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
              (pullbackDescCont hpb φ₁ φ₂ hφ)) =
            ((TopologicalFiberProduct.snd β₁ β₂).comp
              (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)).comp
                (pullbackDescCont hpb φ₁ φ₂ hφ) := by
                  rfl
        _ = α₂.comp (pullbackDescCont hpb φ₁ φ₂ hφ) := by
              rw [TopologicalFiberProduct.snd_toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb]
        _ = φ₂ := pullbackDescCont_right hpb φ₁ φ₂ hφ
    have hright :
        (TopologicalFiberProduct.snd β₁ β₂).comp
            (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hφ a)) = φ₂ :=
      TopologicalFiberProduct.snd_lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hφ a)
    exact congrArg (fun f : A →ₜ* H₂ => f a) (hleft.trans hright.symm)

theorem

surjective_pullbackDescCont_of_ker_eq

L359 ↗

ProCGroups.Categorical.surjective_pullbackDescCont_of_ker_eq

Documentation

Surjective coordinate maps whose underlying composite kernel is the supremum of their kernels induce a surjective descent map for a profinite-tested pullback square.

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in

Lean source · statement

theorem surjective_pullbackDescCont_of_ker_eq
    {A : Type u} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
    [CompactSpace A] [T2Space A] [TotallyDisconnectedSpace A]
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
    (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
    (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
    (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
    (hker : (β₁.comp φ₁).toMonoidHom.ker = φ₁.toMonoidHom.ker ⊔ φ₂.toMonoidHom.ker) :
    Function.Surjective (pullbackDescCont hpb φ₁ φ₂ hcomp)

def

pullbackContEquivOfIsPullback

L395 ↗

ProCGroups.Categorical.pullbackContEquivOfIsPullback

Documentation

Any profinite-tested pullback square is canonically isomorphic to the concrete continuous fiber product.

Source context 12 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]

Lean source · full declaration

def pullbackContEquivOfIsPullback
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
    G ≃ₜ* TopologicalFiberProduct.carrier β₁ β₂ where
  toMulEquiv :=
    { toFun := toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb
      invFun := fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb
      left_inv := by
        intro g
        exact congrArg (fun f : G →ₜ* G => f g)
          (fromContinuousPullback_comp_toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)
      right_inv := by
        intro x
        exact congrArg
          (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* TopologicalFiberProduct.carrier β₁
              β₂ => f x)
          (toContinuousPullback_comp_fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)
      map_mul' := by
        intro x y
        exact (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).map_mul x y }
  continuous_toFun := (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).continuous_toFun
  continuous_invFun :=
    (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).continuous_toFun

theorem

pullbackContEquivOfIsPullback_symm_toContinuousMonoidHom

L425 ↗

ProCGroups.Categorical.pullbackContEquivOfIsPullback_symm_toContinuousMonoidHom

Documentation

Forgetting continuity from the inverse of the canonical pullback equivalence recovers the inverse comparison map.

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in

Lean source · statement

theorem pullbackContEquivOfIsPullback_symm_toContinuousMonoidHom
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
    (ContinuousMonoidHom.toContinuousMonoidHom (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂
        hpb).symm) =
      fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb

theorem

pullbackContEquivOfIsPullback_fst

L437 ↗

ProCGroups.Categorical.pullbackContEquivOfIsPullback_fst

Documentation

The first coordinate of the canonical pullback equivalence recovers \(\alpha_1\).

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in

Lean source · statement

theorem pullbackContEquivOfIsPullback_fst
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
    (TopologicalFiberProduct.fst β₁ β₂).comp
        (ContinuousMonoidHom.toContinuousMonoidHom (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂
            hpb)) =
      α₁

theorem

pullbackContEquivOfIsPullback_snd

L449 ↗

ProCGroups.Categorical.pullbackContEquivOfIsPullback_snd

Documentation

The second coordinate of the canonical pullback equivalence recovers \(\alpha_2\).

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in

Lean source · statement

theorem pullbackContEquivOfIsPullback_snd
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
    (TopologicalFiberProduct.snd β₁ β₂).comp
        (ContinuousMonoidHom.toContinuousMonoidHom (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂
            hpb)) =
      α₂

theorem

pullbackContEquivOfIsPullback_symm_fst_apply

L461 ↗

ProCGroups.Categorical.pullbackContEquivOfIsPullback_symm_fst_apply

Documentation

Pointwise first-coordinate formula for the inverse of the canonical pullback equivalence.

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in

Lean source · statement

theorem pullbackContEquivOfIsPullback_symm_fst_apply
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) (x : TopologicalFiberProduct.carrier β₁
        β₂) :
    α₁ ((pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂ hpb).symm x) =
      TopologicalFiberProduct.fst β₁ β₂ x

theorem

pullbackContEquivOfIsPullback_symm_snd_apply

L486 ↗

ProCGroups.Categorical.pullbackContEquivOfIsPullback_symm_snd_apply

Documentation

Pointwise second-coordinate formula for the inverse of the canonical pullback equivalence.

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in

Lean source · statement

theorem pullbackContEquivOfIsPullback_symm_snd_apply
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) (x : TopologicalFiberProduct.carrier β₁
        β₂) :
    α₂ ((pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂ hpb).symm x) =
      TopologicalFiberProduct.snd β₁ β₂ x

theorem

hasProfiniteTestPullbackProperty_iff_bijective_toConcretePullback

L512 ↗

ProCGroups.Categorical.hasProfiniteTestPullbackProperty_iff_bijective_toConcretePullback

Documentation

A commutative square has the universal property against profinite source groups if and only if its canonical comparison map to the concrete continuous fiber product is bijective.

Source context 13 commands

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

namespace ProCGroups.Categorical
universe u
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {G H H₁ H₂ : Type u}
variable [Group G] [Group H] [Group H₁] [Group H₂]
variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
variable
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
omit [IsTopologicalGroup H] in

Lean source · full declaration

theorem hasProfiniteTestPullbackProperty_iff_bijective_toConcretePullback
    {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
    {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
    (hcomm : β₁.comp α₁ = β₂.comp α₂) :
    HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂ ↔
      Function.Bijective
        (TopologicalFiberProduct.lift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hcomm g)) := by
  constructor
  · intro hpb
    simpa [toContinuousPullbackOfIsPullback] using
      (bijective_toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)
  · intro hbij
    exact hasProfiniteTestPullbackProperty_of_bijective_toConcretePullback
      α₁ α₂ β₁ β₂
      (TopologicalFiberProduct.lift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hcomm g))
      hbij
      (TopologicalFiberProduct.fst_lift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hcomm g))
      (TopologicalFiberProduct.snd_lift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hcomm g))

Module documentation

Pro C Groups / Categorical / Pullback Comparison

Declarations