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.

Equations

• Profinite.pullback f g = Profinite.of ↑{xy : ↑X.toCompHaus.toTop × ↑Y.toCompHaus.toTop | f xy.1 = g xy.2}

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.

Equations

• Profinite.pullback.fst f g = { toFun := fun (x : ↑(Profinite.pullback f g).toCompHaus.toTop) => match x with | ⟨(x, snd), property⟩ => x, continuous_toFun := ⋯ }

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.

Equations

• Profinite.pullback.snd f g = { toFun := fun (x : ↑(Profinite.pullback f g).toCompHaus.toTop) => match x with | ⟨(fst, y), property⟩ => y, continuous_toFun := ⋯ }

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.

Equations

• Profinite.pullback.lift f g a b w = { toFun := fun (z : ↑Z.toCompHaus.toTop) => ⟨(a z, b z), ⋯⟩, continuous_toFun := ⋯ }

@[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).π = { app := fun (j : CategoryTheory.Limits.WalkingCospan) => Option.rec (CategoryTheory.CategoryStruct.comp (Profinite.pullback.fst f g) f) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (Profinite.pullback.fst f g) (Profinite.pullback.snd f g) val) j, naturality := ⋯ }

@[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.

Equations

• Profinite.pullback.cone f g = CategoryTheory.Limits.PullbackCone.mk (Profinite.pullback.fst f g) (Profinite.pullback.snd f g) ⋯

@[simp]

theorem Profinite.pullback.isLimit_lift {X : Profinite} {Y : Profinite} {B : Profinite} (f : X ⟶ B) (g : Y ⟶ B) (s : CategoryTheory.Limits.PullbackCone f g) : (Profinite.pullback.isLimit f g).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) : CategoryTheory.Limits.IsLimit (Profinite.pullback.cone f g)

The explicit pullback cone is a limit cone.

Equations

• Profinite.pullback.isLimit f g = (Profinite.pullback.cone f g).isLimitAux (fun (s : CategoryTheory.Limits.PullbackCone f g) => Profinite.pullback.lift f g s.fst s.snd ⋯) ⋯ ⋯ ⋯

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.

Equations

• Profinite.pullbackIsoPullback f g = (Profinite.pullback.isLimit f g).conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.cospan f g))

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.

Equations

• Profinite.pullbackHomeoPullback f g = Profinite.homeoOfIso (Profinite.pullbackIsoPullback f g)

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} [Finite α] (X : α → Profinite) : Profinite

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

Equations

• Profinite.finiteCoproduct X = Profinite.of ((a : α) × ↑(X a).toCompHaus.toTop)

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

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

Equations

• Profinite.finiteCoproduct.ι X a = { toFun := fun (x : ↑(X a).toCompHaus.toTop) => ⟨a, x⟩, continuous_toFun := ⋯ }

def Profinite.finiteCoproduct.desc {α : Type} [Finite α] (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.

Equations

• Profinite.finiteCoproduct.desc X e = { toFun := fun (x : ↑(Profinite.finiteCoproduct X).toCompHaus.toTop) => match x with | ⟨a, x⟩ => (e a) x, continuous_toFun := ⋯ }

@[simp]

theorem Profinite.finiteCoproduct.ι_desc_assoc {α : Type} [Finite α] (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} [Finite α] (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} [Finite α] (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_pt {α : Type} [Finite α] (X : α → Profinite) : (Profinite.finiteCoproduct.cocone X).pt = Profinite.finiteCoproduct X

@[simp]

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

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

The coproduct cocone associated to the explicit finite coproduct.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

The explicit finite coproduct cocone is a colimit cocone.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Profinite.coproductIsoCoproduct X = (Profinite.finiteCoproduct.isColimit X).coconePointUniqueUpToIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor X))

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

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

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

Equations

• Profinite.coproductHomeoCoproduct X = Profinite.homeoOfIso (Profinite.coproductIsoCoproduct X)

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

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

theorem Profinite.finiteCoproduct.ι_desc_apply {α : Type} [Finite α] (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

instance Profinite.instPreservesFiniteCoproductsCompHausProfiniteToCompHaus : CategoryTheory.Limits.PreservesFiniteCoproducts profiniteToCompHaus

Equations

• One or more equations did not get rendered due to their size.

instance Profinite.instFinitaryExtensive : CategoryTheory.FinitaryExtensive Profinite

Equations

• Profinite.instFinitaryExtensive = ⋯