# Explicit limits and colimits #

This file collects some constructions of explicit limits and colimits in Profinite, which may be useful due to their definitional properties.

## Main definitions #

• Profinite.pullback: Explicit pullback, defined in the "usual" way as a subset of the product.
• Profinite.finiteCoproduct: Explicit finite coproducts, defined as a disjoint union.
def Profinite.pullback {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :

The pullback of two morphisms f, g in Profinite, constructed explicitly as the set of pairs (x, y) such that f x = g y, with the topology induced by the product.

Equations
• = Profinite.of {xy : X.toCompHaus.toTop × Y.toCompHaus.toTop | f xy.1 = g xy.2}
Instances For
def Profinite.pullback.fst {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :
X

The projection from the pullback to the first component.

Equations
• = { toFun := fun (x : ().toCompHaus.toTop) => match x with | (x, snd), property => x, continuous_toFun := }
Instances For
def Profinite.pullback.snd {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :
Y

The projection from the pullback to the second component.

Equations
• = { toFun := fun (x : ().toCompHaus.toTop) => match x with | (fst, y), property => y, continuous_toFun := }
Instances For
theorem Profinite.pullback.condition_assoc {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) {Z : Profinite} (h : B Z) :
theorem Profinite.pullback.condition {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :
def Profinite.pullback.lift {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) {Z : Profinite} (a : Z X) (b : Z Y) :
Z

Construct a morphism to the explicit pullback given morphisms to the factors which are compatible with the maps to the base. This is essentially the universal property of the pullback.

Equations
• = { toFun := fun (z : Z.toCompHaus.toTop) => (a z, b z), , continuous_toFun := }
Instances For
@[simp]
theorem Profinite.pullback.lift_fst_assoc {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) {Z : Profinite} (a : Z✝ X) (b : Z✝ Y) {Z : Profinite} (h : X Z) :
@[simp]
theorem Profinite.pullback.lift_fst {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) {Z : Profinite} (a : Z X) (b : Z Y) :
= a
@[simp]
theorem Profinite.pullback.lift_snd_assoc {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) {Z : Profinite} (a : Z✝ X) (b : Z✝ Y) {Z : Profinite} (h : Y Z) :
@[simp]
theorem Profinite.pullback.lift_snd {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) {Z : Profinite} (a : Z X) (b : Z Y) :
= b
theorem Profinite.pullback.hom_ext {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) {Z : Profinite} (a : Z ) (b : Z ) (hfst : ) (hsnd : ) :
a = b
@[simp]
theorem Profinite.pullback.cone_pt {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :
().pt =
@[simp]
theorem Profinite.pullback.cone_π {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :
() = { app := fun (j : CategoryTheory.Limits.WalkingCospan) => Option.rec (fun (val : CategoryTheory.Limits.WalkingPair) => ) j, naturality := }
def Profinite.pullback.cone {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :

The pullback cone whose cone point is the explicit pullback.

Equations
Instances For
@[simp]
theorem Profinite.pullback.isLimit_lift {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) (s : ) :
.lift s = Profinite.pullback.lift f g s.fst s.snd
def Profinite.pullback.isLimit {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :

The explicit pullback cone is a limit cone.

Equations
Instances For
noncomputable def Profinite.pullbackIsoPullback {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :

The isomorphism from the explicit pullback to the abstract pullback.

Equations
• = .conePointUniqueUpToIso
Instances For
noncomputable def Profinite.pullbackHomeoPullback {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :
().toCompHaus.toTop ≃ₜ .toCompHaus.toTop

The homeomorphism from the explicit pullback to the abstract pullback.

Equations
Instances For
theorem Profinite.pullback_fst_eq {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :
= CategoryTheory.CategoryStruct.comp .hom CategoryTheory.Limits.pullback.fst
theorem Profinite.pullback_snd_eq {X : Profinite} {Y : Profinite} {B : Profinite} (f : X B) (g : Y B) :
= CategoryTheory.CategoryStruct.comp .hom CategoryTheory.Limits.pullback.snd
def Profinite.finiteCoproduct {α : Type w} [] (X : ) :

The coproduct of a finite family of objects in Profinite, constructed as the disjoint union with its usual topology.

Equations
Instances For
def Profinite.finiteCoproduct.ι {α : Type w} [] (X : ) (a : α) :

The inclusion of one of the factors into the explicit finite coproduct.

Equations
• = { toFun := fun (x : (X a).toCompHaus.toTop) => a, x, continuous_toFun := }
Instances For
def Profinite.finiteCoproduct.desc {α : Type w} [] (X : ) {B : Profinite} (e : (a : α) → X a B) :

To construct a morphism from the explicit finite coproduct, it suffices to specify a morphism from each of its factors. This is essentially the universal property of the coproduct.

Equations
• = { toFun := fun (x : .toCompHaus.toTop) => match x with | a, x => (e a) x, continuous_toFun := }
Instances For
@[simp]
theorem Profinite.finiteCoproduct.ι_desc_assoc {α : Type w} [] (X : ) {B : Profinite} (e : (a : α) → X a B) (a : α) {Z : Profinite} (h : B Z) :
@[simp]
theorem Profinite.finiteCoproduct.ι_desc {α : Type w} [] (X : ) {B : Profinite} (e : (a : α) → X a B) (a : α) :
theorem Profinite.finiteCoproduct.hom_ext {α : Type w} [] (X : ) {B : Profinite} (f : ) (g : ) (h : ∀ (a : α), ) :
f = g
@[reducible, inline]
abbrev Profinite.finiteCoproduct.cofan {α : Type w} [] (X : ) :

The coproduct cocone associated to the explicit finite coproduct.

Equations
Instances For
def Profinite.finiteCoproduct.isColimit {α : Type w} [] (X : ) :

The explicit finite coproduct cocone is a colimit cocone.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def Profinite.coproductIsoCoproduct {α : Type w} [] (X : ) :

The isomorphism from the explicit finite coproducts to the abstract coproduct.

Equations
• = .coconePointUniqueUpToIso
Instances For
theorem Profinite.Sigma.ι_comp_toFiniteCoproduct {α : Type w} [] (X : ) (a : α) :
noncomputable def Profinite.coproductHomeoCoproduct {α : Type w} [] (X : ) :
.toCompHaus.toTop ≃ₜ ( X).toCompHaus.toTop

The homeomorphism from the explicit finite coproducts to the abstract coproduct.

Equations
Instances For
theorem Profinite.finiteCoproduct.ι_injective {α : Type w} [] (X : ) (a : α) :
theorem Profinite.finiteCoproduct.ι_jointly_surjective {α : Type w} [] (X : ) (R : .toCompHaus.toTop) :
∃ (a : α) (r : (X a).toCompHaus.toTop), R = r
theorem Profinite.finiteCoproduct.ι_desc_apply {α : Type w} [] (X : ) {B : Profinite} {π : (a : α) → X a B} (a : α) (x : (X a)) :
( x) = (π a) x
Equations
• One or more equations did not get rendered due to their size.
Equations