Module

ProfinitePullbacks.lean

Nyll.ProCGroups.Categorical.ProfinitePullbacks

36 declarations indexed from sourceView source ↗

Module documentation

Continuous pullbacks of topological groups

This module develops continuous fiber products and the universal property obtained by testing a continuous square against profinite source groups. The four objects in a tested square are not required to be profinite.

Imports4

Imported by4

abbrev

carrier

L33 ↗

ProCGroups.Categorical.TopologicalFiberProduct.carrier

Documentation

Continuous pullback carrier attached to two continuous homomorphisms.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

abbrev TopologicalFiberProduct.carrier
    [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)

def

fst

L40 ↗

ProCGroups.Categorical.TopologicalFiberProduct.fst

Documentation

The first projection from the continuous pullback.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

def TopologicalFiberProduct.fst
    [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
    TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₁

def

snd

L49 ↗

ProCGroups.Categorical.TopologicalFiberProduct.snd

Documentation

The second projection from the continuous pullback.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

def TopologicalFiberProduct.snd
    [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
    TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₂

theorem

hom_ext

L58 ↗

ProCGroups.Categorical.TopologicalFiberProduct.hom_ext

Documentation

Extensionality for continuous homomorphisms into the concrete continuous fiber product.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem TopologicalFiberProduct.hom_ext
    [Group H] [Group H₁] [Group H₂] [Group K]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
    {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
    {ψ ψ' : K →ₜ* TopologicalFiberProduct.carrier β₁ β₂}
    (h₁ : ∀ k, TopologicalFiberProduct.fst β₁ β₂ (ψ k) = TopologicalFiberProduct.fst β₁ β₂ (ψ' k))
    (h₂ : ∀ k, TopologicalFiberProduct.snd β₁ β₂ (ψ k) = TopologicalFiberProduct.snd β₁ β₂ (ψ' k)) :
    ψ = ψ'

theorem

pullbackFstCont_surjective_of_right_surjective

L74 ↗

ProCGroups.Categorical.pullbackFstCont_surjective_of_right_surjective

Documentation

If the right map in the pullback square is surjective, then the first projection from the continuous pullback is surjective.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem pullbackFstCont_surjective_of_right_surjective
    [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hβ₂ : Function.Surjective β₂) :
    Function.Surjective (TopologicalFiberProduct.fst β₁ β₂)

theorem

pullbackSndCont_surjective_of_left_surjective

L89 ↗

ProCGroups.Categorical.pullbackSndCont_surjective_of_left_surjective

Documentation

If the left map in the pullback square is surjective, then the second projection from the continuous pullback is surjective.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem pullbackSndCont_surjective_of_left_surjective
    [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hβ₁ : Function.Surjective β₁) :
    Function.Surjective (TopologicalFiberProduct.snd β₁ β₂)

theorem

pullbackFstCont_injective_of_right_injective

L101 ↗

ProCGroups.Categorical.pullbackFstCont_injective_of_right_injective

Documentation

If \(\beta_2\) is injective, then the first continuous pullback projection is injective.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem pullbackFstCont_injective_of_right_injective
    [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hβ₂ : Function.Injective β₂) :
    Function.Injective (TopologicalFiberProduct.fst β₁ β₂)

theorem

pullbackSndCont_injective_of_left_injective

L113 ↗

ProCGroups.Categorical.pullbackSndCont_injective_of_left_injective

Documentation

If \(\beta_1\) is injective, then the second continuous pullback projection is injective.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem pullbackSndCont_injective_of_left_injective
    [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (hβ₁ : Function.Injective β₁) :
    Function.Injective (TopologicalFiberProduct.snd β₁ β₂)

def

lift

L125 ↗

ProCGroups.Categorical.TopologicalFiberProduct.lift

Documentation

The canonical continuous map into the pullback.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

def TopologicalFiberProduct.lift
    [Group H] [Group H₁] [Group H₂] [Group K]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
    (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
    K →ₜ* TopologicalFiberProduct.carrier β₁ β₂

theorem

pullbackFstCont_pullbackLiftCont

L142 ↗

ProCGroups.Categorical.pullbackFstCont_pullbackLiftCont

Documentation

Composing the first projection with the continuous pullback lift gives \(\varphi_1\).

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem pullbackFstCont_pullbackLiftCont
    [Group H] [Group H₁] [Group H₂] [Group K]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
    (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
    (TopologicalFiberProduct.fst β₁ β₂).comp (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ h) = φ₁

theorem

pullbackSndCont_pullbackLiftCont

L153 ↗

ProCGroups.Categorical.pullbackSndCont_pullbackLiftCont

Documentation

Composing the second projection with the continuous pullback lift gives \(\varphi_2\).

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem pullbackSndCont_pullbackLiftCont
    [Group H] [Group H₁] [Group H₂] [Group K]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
    (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
    (TopologicalFiberProduct.snd β₁ β₂).comp (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ h) = φ₂

theorem

pullbackLiftCont_eta

L164 ↗

ProCGroups.Categorical.pullbackLiftCont_eta

Documentation

The continuous pullback is reconstructed from its two projections by the canonical lift.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · full declaration

theorem pullbackLiftCont_eta
    [Group H] [Group H₁] [Group H₂] [Group K]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
    {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
    (ψ : K →ₜ* TopologicalFiberProduct.carrier β₁ β₂) :
    TopologicalFiberProduct.lift β₁ β₂
      ((TopologicalFiberProduct.fst β₁ β₂).comp ψ)
      ((TopologicalFiberProduct.snd β₁ β₂).comp ψ)
      (fun k => by exact (ψ k).2) = ψ := by
  apply TopologicalFiberProduct.hom_ext
  · intro k
    rfl
  · intro k
    rfl

def

cone

L180 ↗

ProCGroups.Categorical.TopologicalFiberProduct.cone

Documentation

The concrete topological fiber product as a categorical pullback cone in TopGrp.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

def TopologicalFiberProduct.cone
    [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
    PullbackCone (TopGrp.ofHom β₁) (TopGrp.ofHom β₂)

def

isLimit

L195 ↗

ProCGroups.Categorical.TopologicalFiberProduct.isLimit

Documentation

The concrete topological fiber product cone is a limit cone in TopGrp.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

def TopologicalFiberProduct.isLimit
    [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
    IsLimit (TopologicalFiberProduct.cone β₁ β₂)

theorem

pullbackLiftCont_injective_of_left_injective

L235 ↗

ProCGroups.Categorical.pullbackLiftCont_injective_of_left_injective

Documentation

If \(\varphi_1\) is injective, then the continuous canonical map into the continuous fiber product is injective.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem pullbackLiftCont_injective_of_left_injective
    [Group H] [Group H₁] [Group H₂] [Group K]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
    (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k))
    (hφ₁ : Function.Injective φ₁) :
    Function.Injective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ h)

theorem

pullbackLiftCont_injective_of_right_injective

L255 ↗

ProCGroups.Categorical.pullbackLiftCont_injective_of_right_injective

Documentation

If \(\varphi_2\) is injective, then the continuous canonical map into the continuous fiber product is injective.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem pullbackLiftCont_injective_of_right_injective
    [Group H] [Group H₁] [Group H₂] [Group K]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
    (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k))
    (hφ₂ : Function.Injective φ₂) :
    Function.Injective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ h)

def

HasProfiniteTestPullbackProperty

L276 ↗

ProCGroups.Categorical.HasProfiniteTestPullbackProperty

Documentation

Continuous pullback property tested by profinite source objects. The property tests the square against profinite objects without requiring the four objects of the square themselves to be profinite.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

def HasProfiniteTestPullbackProperty
    [Group G] [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) : Prop

def

pullbackDescCont

L292 ↗

ProCGroups.Categorical.pullbackDescCont

Documentation

Chosen continuous morphism induced by the pullback universal property.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

def pullbackDescCont
    [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
    [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    [TopologicalSpace K]
    [IsTopologicalGroup K] [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
    {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
    (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
    (hφ : β₁.comp φ₁ = β₂.comp φ₂) : K →ₜ* G

theorem

pullbackDescCont_spec

L305 ↗

ProCGroups.Categorical.pullbackDescCont_spec

Documentation

Specification of the chosen continuous pullback descent map.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem pullbackDescCont_spec
    [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
    [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    [TopologicalSpace K]
    [IsTopologicalGroup K] [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
    {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
    (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
    (hφ : β₁.comp φ₁ = β₂.comp φ₂) :
    α₁.comp (pullbackDescCont hpb φ₁ φ₂ hφ) = φ₁ ∧
      α₂.comp (pullbackDescCont hpb φ₁ φ₂ hφ) = φ₂

theorem

pullbackDescCont_left

L320 ↗

ProCGroups.Categorical.pullbackDescCont_left

Documentation

The left composite of the chosen continuous pullback descent map is the prescribed left leg.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem pullbackDescCont_left
    [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
    [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    [TopologicalSpace K]
    [IsTopologicalGroup K] [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
    {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
    (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
    (hφ : β₁.comp φ₁ = β₂.comp φ₂) :
    α₁.comp (pullbackDescCont hpb φ₁ φ₂ hφ) = φ₁

theorem

pullbackDescCont_right

L336 ↗

ProCGroups.Categorical.pullbackDescCont_right

Documentation

The right composite of the chosen continuous pullback descent map is the prescribed right leg.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem pullbackDescCont_right
    [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
    [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    [TopologicalSpace K]
    [IsTopologicalGroup K] [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
    {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
    (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
    (hφ : β₁.comp φ₁ = β₂.comp φ₂) :
    α₂.comp (pullbackDescCont hpb φ₁ φ₂ hφ) = φ₂

theorem

pullbackDescCont_uniq

L350 ↗

ProCGroups.Categorical.pullbackDescCont_uniq

Documentation

Uniqueness of the chosen continuous pullback descent map.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem pullbackDescCont_uniq
    [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
    [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    [TopologicalSpace K]
    [IsTopologicalGroup K] [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
    {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
    {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
    (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
    (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
    (hφ : β₁.comp φ₁ = β₂.comp φ₂)
    {ψ : K →ₜ* G}
    (hψ : α₁.comp ψ = φ₁ ∧ α₂.comp ψ = φ₂) :
    ψ = pullbackDescCont hpb φ₁ φ₂ hφ

theorem

pullback_isClosed

L367 ↗

ProCGroups.Categorical.pullback_isClosed

Documentation

The concrete pullback subgroup is closed in \(H_1 \times H_2\).

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem pullback_isClosed
    {H H₁ H₂ : Type u}
    [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [T2Space H]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
    IsClosed ((FiberProduct.subgroup (β₁ : H₁ →* H) (β₂ : H₂ →* H) : Subgroup (H₁ × H₂)) :
      Set (H₁ × H₂))

instance

compactSpace

L379 ↗

ProCGroups.Categorical.TopologicalFiberProduct.compactSpace

Documentation

The concrete pullback of continuous maps between compact Hausdorff groups is compact.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

instance TopologicalFiberProduct.compactSpace
    {H H₁ H₂ : Type u}
    [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    [CompactSpace H₁] [CompactSpace H₂] [T2Space H]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    : CompactSpace (TopologicalFiberProduct.carrier β₁ β₂)

theorem

hasProfiniteTestPullbackProperty

L391 ↗

ProCGroups.Categorical.TopologicalFiberProduct.hasProfiniteTestPullbackProperty

Documentation

The concrete continuous fiber product has the restricted profinite-source test property.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem TopologicalFiberProduct.hasProfiniteTestPullbackProperty
    {H H₁ H₂ : Type u}
    [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
    HasProfiniteTestPullbackProperty (TopologicalFiberProduct.fst β₁ β₂)
        (TopologicalFiberProduct.snd β₁ β₂) β₁ β₂

theorem

hasProfiniteTestPullbackProperty_of_bijective_toConcretePullback

L444 ↗

ProCGroups.Categorical.hasProfiniteTestPullbackProperty_of_bijective_toConcretePullback

Documentation

A profinite square with a bijective continuous comparison map to the concrete fiber product has the profinite-source test property.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem hasProfiniteTestPullbackProperty_of_bijective_toConcretePullback
    {G H H₁ H₂ : Type u}
    [Group G] [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace 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₂]
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (τ : G →ₜ* TopologicalFiberProduct.carrier β₁ β₂)
    (hτ : Function.Bijective τ)
    (h₁ : (TopologicalFiberProduct.fst β₁ β₂).comp τ = α₁)
    (h₂ : (TopologicalFiberProduct.snd β₁ β₂).comp τ = α₂) :
    HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂

theorem

hasProfiniteTestPullbackProperty_of_equiv_toConcretePullback

L548 ↗

ProCGroups.Categorical.hasProfiniteTestPullbackProperty_of_equiv_toConcretePullback

Documentation

A continuous multiplicative equivalence with the concrete fiber product transports the profinite-source test property.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · statement

theorem hasProfiniteTestPullbackProperty_of_equiv_toConcretePullback
    [Group G] [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (e : G ≃ₜ* TopologicalFiberProduct.carrier β₁ β₂)
    (h₁ : (TopologicalFiberProduct.fst β₁ β₂).comp (ContinuousMonoidHom.toContinuousMonoidHom e)
        = α₁)
    (h₂ : (TopologicalFiberProduct.snd β₁ β₂).comp (ContinuousMonoidHom.toContinuousMonoidHom e)
        = α₂) :
    HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂

theorem

pullbackLiftCont_surjective_iff_ker_comp_le_sup_ker

L649 ↗

ProCGroups.Categorical.pullbackLiftCont_surjective_iff_ker_comp_le_sup_ker

Documentation

The continuous pullback lift is surjective exactly when the underlying composite kernel is contained in the supremum of the two underlying coordinate kernels.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · full declaration

theorem pullbackLiftCont_surjective_iff_ker_comp_le_sup_ker
    [Group A] [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace A] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    {β₁ : H₁ →ₜ* H} (β₂ : H₂ →ₜ* H)
    {φ₁ : A →ₜ* H₁} {φ₂ : A →ₜ* H₂}
    (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
    (hcomp : β₁.comp φ₁ = β₂.comp φ₂) :
    Function.Surjective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂
        (fun a => DFunLike.congr_fun hcomp a)) ↔
      ((β₁.comp φ₁ : A →ₜ* H).toMonoidHom).ker ≤
        ((φ₁ : A →ₜ* H₁).toMonoidHom).ker ⊔
          ((φ₂ : A →ₜ* H₂).toMonoidHom).ker := by
  have hcomp' :
      ((β₁ : H₁ →* H).comp (φ₁ : A →* H₁)) =
        ((β₂ : H₂ →* H).comp (φ₂ : A →* H₂)) := by
    ext a
    exact DFunLike.congr_fun hcomp a
  change
    Function.Surjective
        (FiberProduct.lift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
          (φ₁ : A →* H₁) (φ₂ : A →* H₂) _) ↔
      ((β₁ : H₁ →* H).comp (φ₁ : A →* H₁)).ker ≤
        (φ₁ : A →* H₁).ker ⊔ (φ₂ : A →* H₂).ker
  exact pullbackLift_surjective_iff_ker_comp_le_sup_ker
    (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H))
    (φ₁ := (φ₁ : A →* H₁)) (φ₂ := (φ₂ : A →* H₂))
    hφ₁ hφ₂ hcomp'

theorem

pullbackLiftCont_surjective_iff_ker_eq

L678 ↗

ProCGroups.Categorical.pullbackLiftCont_surjective_iff_ker_eq

Documentation

Surjectivity of the continuous pullback lift is equivalent to the required kernel equality.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · full declaration

theorem pullbackLiftCont_surjective_iff_ker_eq
    [Group A] [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace A] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    {β₁ : H₁ →ₜ* H} (β₂ : H₂ →ₜ* H)
    {φ₁ : A →ₜ* H₁} {φ₂ : A →ₜ* H₂}
    (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
    (hcomp : β₁.comp φ₁ = β₂.comp φ₂) :
    Function.Surjective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂
        (fun a => DFunLike.congr_fun hcomp a)) ↔
      ((β₁.comp φ₁ : A →ₜ* H).toMonoidHom).ker =
        ((φ₁ : A →ₜ* H₁).toMonoidHom).ker ⊔
          ((φ₂ : A →ₜ* H₂).toMonoidHom).ker := by
  have hcomp' :
      ((β₁ : H₁ →* H).comp (φ₁ : A →* H₁)) =
        ((β₂ : H₂ →* H).comp (φ₂ : A →* H₂)) := by
    ext a
    exact DFunLike.congr_fun hcomp a
  change
    Function.Surjective
        (FiberProduct.lift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
          (φ₁ : A →* H₁) (φ₂ : A →* H₂) _) ↔
      ((β₁ : H₁ →* H).comp (φ₁ : A →* H₁)).ker =
        (φ₁ : A →* H₁).ker ⊔ (φ₂ : A →* H₂).ker
  exact pullbackLift_surjective_iff_ker_eq
    (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H))
    (φ₁ := (φ₁ : A →* H₁)) (φ₂ := (φ₂ : A →* H₂))
    hφ₁ hφ₂ hcomp'

theorem

surjective_pullbackLiftCont_of_ker_eq

L708 ↗

ProCGroups.Categorical.surjective_pullbackLiftCont_of_ker_eq

Documentation

Surjective continuous coordinate maps whose underlying composite kernel is the supremum of their kernels induce a surjective continuous map into the fiber product.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · full declaration

theorem surjective_pullbackLiftCont_of_ker_eq
    [Group A] [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace A] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
    (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
    (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
    (hker : ((β₁.comp φ₁ : A →ₜ* H).toMonoidHom).ker =
      ((φ₁ : A →ₜ* H₁).toMonoidHom).ker ⊔ ((φ₂ : A →ₜ* H₂).toMonoidHom).ker) :
    Function.Surjective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by
      exact DFunLike.congr_fun hcomp a)) := by
  exact (pullbackLiftCont_surjective_iff_ker_eq
    (β₁ := β₁) (β₂ := β₂) (φ₁ := φ₁) (φ₂ := φ₂) hφ₁ hφ₂ hcomp).2 hker

theorem

bijective_pullbackLiftCont_of_left_injective_of_ker_eq

L726 ↗

ProCGroups.Categorical.bijective_pullbackLiftCont_of_left_injective_of_ker_eq

Documentation

The continuous pullback lift is bijective when the left map is injective and the required kernel equality holds.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · full declaration

theorem bijective_pullbackLiftCont_of_left_injective_of_ker_eq
    [Group A] [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace A] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
    (hφ₁surj : Function.Surjective φ₁) (hφ₂surj : Function.Surjective φ₂)
    (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
    (hker : ((β₁.comp φ₁ : A →ₜ* H).toMonoidHom).ker =
      ((φ₁ : A →ₜ* H₁).toMonoidHom).ker ⊔ ((φ₂ : A →ₜ* H₂).toMonoidHom).ker)
    (hφ₁inj : Function.Injective φ₁) :
    Function.Bijective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by
      exact DFunLike.congr_fun hcomp a)) := by
  refine ⟨?_, ?_⟩
  · exact pullbackLiftCont_injective_of_left_injective β₁ β₂ φ₁ φ₂
      (fun a => DFunLike.congr_fun hcomp a) hφ₁inj
  · exact surjective_pullbackLiftCont_of_ker_eq β₁ β₂ φ₁ φ₂
      hφ₁surj hφ₂surj hcomp hker

theorem

bijective_pullbackLiftCont_of_right_injective_of_ker_eq

L748 ↗

ProCGroups.Categorical.bijective_pullbackLiftCont_of_right_injective_of_ker_eq

Documentation

The continuous pullback lift is bijective when the right map is injective and the required kernel equality holds.

Source context 6 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}

Lean source · full declaration

theorem bijective_pullbackLiftCont_of_right_injective_of_ker_eq
    [Group A] [Group H] [Group H₁] [Group H₂]
    [TopologicalSpace A] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
    (hφ₁surj : Function.Surjective φ₁) (hφ₂surj : Function.Surjective φ₂)
    (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
    (hker : ((β₁.comp φ₁ : A →ₜ* H).toMonoidHom).ker =
      ((φ₁ : A →ₜ* H₁).toMonoidHom).ker ⊔ ((φ₂ : A →ₜ* H₂).toMonoidHom).ker)
    (hφ₂inj : Function.Injective φ₂) :
    Function.Bijective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by
      exact DFunLike.congr_fun hcomp a)) := by
  refine ⟨?_, ?_⟩
  · exact pullbackLiftCont_injective_of_right_injective β₁ β₂ φ₁ φ₂
      (fun a => DFunLike.congr_fun hcomp a) hφ₂inj
  · exact surjective_pullbackLiftCont_of_ker_eq β₁ β₂ φ₁ φ₂
      hφ₁surj hφ₂surj hcomp hker

theorem

fst_lift

L769 ↗

ProCGroups.Categorical.TopologicalFiberProduct.fst_lift

Documentation

Composing the first projection with a topological fiber-product lift gives the left map.

Source context 7 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}
namespace TopologicalFiberProduct

Lean source · statement

theorem fst_lift
    [Group H] [Group H₁] [Group H₂] [Group K]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
    (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
    (fst β₁ β₂).comp (lift β₁ β₂ φ₁ φ₂ h) = φ₁

theorem

snd_lift

L779 ↗

ProCGroups.Categorical.TopologicalFiberProduct.snd_lift

Documentation

Composing the second projection with a topological fiber-product lift gives the right map.

Source context 7 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}
namespace TopologicalFiberProduct

Lean source · statement

theorem snd_lift
    [Group H] [Group H₁] [Group H₂] [Group K]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
    (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
    (snd β₁ β₂).comp (lift β₁ β₂ φ₁ φ₂ h) = φ₂

theorem

fst_lift_apply

L789 ↗

ProCGroups.Categorical.TopologicalFiberProduct.fst_lift_apply

Documentation

The first projection of a lifted element is the value of the first coordinate map.

Source context 7 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}
namespace TopologicalFiberProduct

Lean source · statement

theorem fst_lift_apply
    [Group H] [Group H₁] [Group H₂] [Group K]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
    (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) (k : K) :
    fst β₁ β₂ (lift β₁ β₂ φ₁ φ₂ h k) = φ₁ k

theorem

snd_lift_apply

L799 ↗

ProCGroups.Categorical.TopologicalFiberProduct.snd_lift_apply

Documentation

The second projection of a lifted element is the value of the second coordinate map.

Source context 7 commands

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

namespace ProCGroups.Categorical
open CategoryTheory Limits
universe u v
section
open _root_.ProCGroups.ContinuousMonoidHom
variable {A G H H₁ H₂ K : Type u}
namespace TopologicalFiberProduct

Lean source · statement

theorem snd_lift_apply
    [Group H] [Group H₁] [Group H₂] [Group K]
    [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
    (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
    (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
    (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) (k : K) :
    snd β₁ β₂ (lift β₁ β₂ φ₁ φ₂ h k) = φ₂ k

Module documentation

Continuous pullbacks of topological groups

Declarations