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) : Profinite

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.

def Profinite.pullback.fst {X : Profinite} {Y : Profinite} {B : Profinite} (f : X ⟶ B) (g : Y ⟶ B) : Profinite.pullback f g ⟶ X

The projection from the pullback to the first component.

def Profinite.pullback.snd {X : Profinite} {Y : Profinite} {B : Profinite} (f : X ⟶ B) (g : Y ⟶ B) : Profinite.pullback f g ⟶ Y

The projection from the pullback to the second component.

theorem Profinite.pullback.condition_assoc {X : Profinite} {Y : Profinite} {B : Profinite} (f : X ⟶ B) (g : Y ⟶ B) {Z : Profinite} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (Profinite.pullback.fst f g) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (Profinite.pullback.snd f g) (CategoryTheory.CategoryStruct.comp g h)

theorem Profinite.pullback.condition {X : Profinite} {Y : Profinite} {B : Profinite} (f : X ⟶ B) (g : Y ⟶ B) : CategoryTheory.CategoryStruct.comp (Profinite.pullback.fst f g) f = CategoryTheory.CategoryStruct.comp (Profinite.pullback.snd f g) g

def Profinite.pullback.lift {X : Profinite} {Y : Profinite} {B : Profinite} (f : X ⟶ B) (g : Y ⟶ B) {Z : Profinite} (a : Z ⟶ X) (b : Z ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) : Z ⟶ Profinite.pullback f g

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.

@[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) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) {Z : Profinite} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (Profinite.pullback.lift f g a b w) (CategoryTheory.CategoryStruct.comp (Profinite.pullback.fst f g) h) = CategoryTheory.CategoryStruct.comp a h

@[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) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) : CategoryTheory.CategoryStruct.comp (Profinite.pullback.lift f g a b w) (Profinite.pullback.fst f g) = 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) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) {Z : Profinite} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (Profinite.pullback.lift f g a b w) (CategoryTheory.CategoryStruct.comp (Profinite.pullback.snd f g) h) = CategoryTheory.CategoryStruct.comp b h

@[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) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) : CategoryTheory.CategoryStruct.comp (Profinite.pullback.lift f g a b w) (Profinite.pullback.snd f g) = b

theorem Profinite.pullback.hom_ext {X : Profinite} {Y : Profinite} {B : Profinite} (f : X ⟶ B) (g : Y ⟶ B) {Z : Profinite} (a : Z ⟶ Profinite.pullback f g) (b : Z ⟶ Profinite.pullback f g) (hfst : CategoryTheory.CategoryStruct.comp a (Profinite.pullback.fst f g) = CategoryTheory.CategoryStruct.comp b (Profinite.pullback.fst f g)) (hsnd : CategoryTheory.CategoryStruct.comp a (Profinite.pullback.snd f g) = CategoryTheory.CategoryStruct.comp b (Profinite.pullback.snd f g)) : a = b

@[simp]

theorem Profinite.pullback.cone_π {X : Profinite} {Y : Profinite} {B : Profinite} (f : X ⟶ B) (g : Y ⟶ B) : (Profinite.pullback.cone f g).π = CategoryTheory.NatTrans.mk fun j => Option.rec (CategoryTheory.CategoryStruct.comp (Profinite.pullback.fst f g) f) (fun val => CategoryTheory.Limits.WalkingPair.rec (Profinite.pullback.fst f g) (Profinite.pullback.snd f g) val) j

@[simp]

theorem Profinite.pullback.cone_pt {X : Profinite} {Y : Profinite} {B : Profinite} (f : X ⟶ B) (g : Y ⟶ B) : (Profinite.pullback.cone f g).pt = Profinite.pullback f g

def Profinite.pullback.cone {X : Profinite} {Y : Profinite} {B : Profinite} (f : X ⟶ B) (g : Y ⟶ B) : CategoryTheory.Limits.PullbackCone f g

The pullback cone whose cone point is the explicit pullback.

@[simp]

theorem Profinite.pullback.isLimit_lift {X : Profinite} {Y : Profinite} {B : Profinite} (f : X ⟶ B) (g : Y ⟶ B) (s : CategoryTheory.Limits.PullbackCone f g) : CategoryTheory.Limits.IsLimit.lift (Profinite.pullback.isLimit f g) s = Profinite.pullback.lift f g (CategoryTheory.Limits.PullbackCone.fst s) (CategoryTheory.Limits.PullbackCone.snd s) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.fst s) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.snd s) g)

def Profinite.pullback.isLimit {X : Profinite} {Y : Profinite} {B : Profinite} (f : X ⟶ B) (g : Y ⟶ B) : CategoryTheory.Limits.IsLimit (Profinite.pullback.cone f g)

The explicit pullback cone is a limit cone.

noncomputable def Profinite.pullbackIsoPullback {X : Profinite} {Y : Profinite} {B : Profinite} (f : X ⟶ B) (g : Y ⟶ B) : Profinite.pullback f g ≅ CategoryTheory.Limits.pullback f g

The isomorphism from the explicit pullback to the abstract pullback.

noncomputable def Profinite.pullbackHomeoPullback {X : Profinite} {Y : Profinite} {B : Profinite} (f : X ⟶ B) (g : Y ⟶ B) : ↑(Profinite.pullback f g).toCompHaus.toTop ≃ₜ ↑(CategoryTheory.Limits.pullback f g).toCompHaus.toTop

The homeomorphism from the explicit pullback to the abstract pullback.

theorem Profinite.pullback_fst_eq {X : Profinite} {Y : Profinite} {B : Profinite} (f : X ⟶ B) (g : Y ⟶ B) : Profinite.pullback.fst f g = CategoryTheory.CategoryStruct.comp (Profinite.pullbackIsoPullback f g).hom CategoryTheory.Limits.pullback.fst

theorem Profinite.pullback_snd_eq {X : Profinite} {Y : Profinite} {B : Profinite} (f : X ⟶ B) (g : Y ⟶ B) : Profinite.pullback.snd f g = CategoryTheory.CategoryStruct.comp (Profinite.pullbackIsoPullback f g).hom CategoryTheory.Limits.pullback.snd

def Profinite.finiteCoproduct {α : Type} [Fintype α] (X : α → Profinite) : Profinite

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

def Profinite.finiteCoproduct.ι {α : Type} [Fintype α] (X : α → Profinite) (a : α) : X a ⟶ Profinite.finiteCoproduct X

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

def Profinite.finiteCoproduct.desc {α : Type} [Fintype α] (X : α → Profinite) {B : Profinite} (e : (a : α) → X a ⟶ B) : Profinite.finiteCoproduct X ⟶ 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.

@[simp]

theorem Profinite.finiteCoproduct.ι_desc_assoc {α : Type} [Fintype α] (X : α → Profinite) {B : Profinite} (e : (a : α) → X a ⟶ B) (a : α) {Z : Profinite} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (Profinite.finiteCoproduct.ι X a) (CategoryTheory.CategoryStruct.comp (Profinite.finiteCoproduct.desc X e) h) = CategoryTheory.CategoryStruct.comp (e a) h

@[simp]

theorem Profinite.finiteCoproduct.ι_desc {α : Type} [Fintype α] (X : α → Profinite) {B : Profinite} (e : (a : α) → X a ⟶ B) (a : α) : CategoryTheory.CategoryStruct.comp (Profinite.finiteCoproduct.ι X a) (Profinite.finiteCoproduct.desc X e) = e a

theorem Profinite.finiteCoproduct.hom_ext {α : Type} [Fintype α] (X : α → Profinite) {B : Profinite} (f : Profinite.finiteCoproduct X ⟶ B) (g : Profinite.finiteCoproduct X ⟶ B) (h : ∀ (a : α), CategoryTheory.CategoryStruct.comp (Profinite.finiteCoproduct.ι X a) f = CategoryTheory.CategoryStruct.comp (Profinite.finiteCoproduct.ι X a) g) : f = g

@[simp]

theorem Profinite.finiteCoproduct.cocone_ι {α : Type} [Fintype α] (X : α → Profinite) : (Profinite.finiteCoproduct.cocone X).ι = CategoryTheory.Discrete.natTrans fun x => match x with | { as := a } => Profinite.finiteCoproduct.ι X a

@[simp]

theorem Profinite.finiteCoproduct.cocone_pt {α : Type} [Fintype α] (X : α → Profinite) : (Profinite.finiteCoproduct.cocone X).pt = Profinite.finiteCoproduct X

def Profinite.finiteCoproduct.cocone {α : Type} [Fintype α] (X : α → Profinite) : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor X)

The coproduct cocone associated to the explicit finite coproduct.

@[simp]

theorem Profinite.finiteCoproduct.isColimit_desc {α : Type} [Fintype α] (X : α → Profinite) (s : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor X)) : CategoryTheory.Limits.IsColimit.desc (Profinite.finiteCoproduct.isColimit X) s = Profinite.finiteCoproduct.desc (fun a => X a) fun a => s.ι.app { as := a }

def Profinite.finiteCoproduct.isColimit {α : Type} [Fintype α] (X : α → Profinite) : CategoryTheory.Limits.IsColimit (Profinite.finiteCoproduct.cocone X)

The explicit finite coproduct cocone is a colimit cocone.

noncomputable def Profinite.coproductIsoCoproduct {α : Type} [Fintype α] (X : α → Profinite) : Profinite.finiteCoproduct X ≅ ∐ X

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

theorem Profinite.Sigma.ι_comp_toFiniteCoproduct {α : Type} [Fintype α] (X : α → Profinite) (a : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι X a) (Profinite.coproductIsoCoproduct X).inv = Profinite.finiteCoproduct.ι X a

noncomputable def Profinite.coproductHomeoCoproduct {α : Type} [Fintype α] (X : α → Profinite) : ↑(Profinite.finiteCoproduct X).toCompHaus.toTop ≃ₜ ↑(∐ X).toCompHaus.toTop

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

theorem Profinite.finiteCoproduct.ι_injective {α : Type} [Fintype α] (X : α → Profinite) (a : α) : Function.Injective ↑(Profinite.finiteCoproduct.ι X a)

theorem Profinite.finiteCoproduct.ι_jointly_surjective {α : Type} [Fintype α] (X : α → Profinite) (R : ↑(Profinite.finiteCoproduct X).toCompHaus.toTop) : ∃ a r, R = ↑(Profinite.finiteCoproduct.ι X a) r

theorem Profinite.finiteCoproduct.ι_desc_apply {α : Type} [Fintype α] (X : α → Profinite) {B : Profinite} {π : (a : α) → X a ⟶ B} (a : α) (x : (CategoryTheory.forget Profinite).obj (X a)) : ↑(Profinite.finiteCoproduct.desc X π) (↑(Profinite.finiteCoproduct.ι X a) x) = ↑(π a) x