Explicit limits and colimits

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

Main definitions

• LightProfinite.pullback: Explicit pullback, defined in the "usual" way as a subset of the product.

• LightProfinite.finiteCoproduct: Explicit finite coproducts, defined as a disjoint union.

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

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

Equations

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

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

The projection from the pullback to the first component.

Equations

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

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

The projection from the pullback to the second component.

Equations

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

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

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

def LightProfinite.pullback.lift {X : LightProfinite} {Y : LightProfinite} {B : LightProfinite} (f : X ⟶ B) (g : Y ⟶ B) {Z : LightProfinite} (a : Z ⟶ X) (b : Z ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) : Z ⟶ LightProfinite.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

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

@[simp]

theorem LightProfinite.pullback.lift_fst_assoc {X : LightProfinite} {Y : LightProfinite} {B : LightProfinite} (f : X ⟶ B) (g : Y ⟶ B) {Z : LightProfinite} (a : Z✝ ⟶ X) (b : Z✝ ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) {Z : LightProfinite} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (LightProfinite.pullback.lift f g a b w) (CategoryTheory.CategoryStruct.comp (LightProfinite.pullback.fst f g) h) = CategoryTheory.CategoryStruct.comp a h

@[simp]

theorem LightProfinite.pullback.lift_fst {X : LightProfinite} {Y : LightProfinite} {B : LightProfinite} (f : X ⟶ B) (g : Y ⟶ B) {Z : LightProfinite} (a : Z ⟶ X) (b : Z ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) : CategoryTheory.CategoryStruct.comp (LightProfinite.pullback.lift f g a b w) (LightProfinite.pullback.fst f g) = a

@[simp]

theorem LightProfinite.pullback.lift_snd_assoc {X : LightProfinite} {Y : LightProfinite} {B : LightProfinite} (f : X ⟶ B) (g : Y ⟶ B) {Z : LightProfinite} (a : Z✝ ⟶ X) (b : Z✝ ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) {Z : LightProfinite} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (LightProfinite.pullback.lift f g a b w) (CategoryTheory.CategoryStruct.comp (LightProfinite.pullback.snd f g) h) = CategoryTheory.CategoryStruct.comp b h

@[simp]

theorem LightProfinite.pullback.lift_snd {X : LightProfinite} {Y : LightProfinite} {B : LightProfinite} (f : X ⟶ B) (g : Y ⟶ B) {Z : LightProfinite} (a : Z ⟶ X) (b : Z ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) : CategoryTheory.CategoryStruct.comp (LightProfinite.pullback.lift f g a b w) (LightProfinite.pullback.snd f g) = b

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

@[simp]

theorem LightProfinite.pullback.cone_π {X : LightProfinite} {Y : LightProfinite} {B : LightProfinite} (f : X ⟶ B) (g : Y ⟶ B) : (LightProfinite.pullback.cone f g).π = { app := fun (j : CategoryTheory.Limits.WalkingCospan) => Option.rec (CategoryTheory.CategoryStruct.comp (LightProfinite.pullback.fst f g) f) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (LightProfinite.pullback.fst f g) (LightProfinite.pullback.snd f g) val) j, naturality := ⋯ }

@[simp]

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

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

The pullback cone whose cone point is the explicit pullback.

Equations

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

@[simp]

theorem LightProfinite.pullback.isLimit_lift {X : LightProfinite} {Y : LightProfinite} {B : LightProfinite} (f : X ⟶ B) (g : Y ⟶ B) (s : CategoryTheory.Limits.PullbackCone f g) : (LightProfinite.pullback.isLimit f g).lift s = LightProfinite.pullback.lift f g s.fst s.snd ⋯

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

The explicit pullback cone is a limit cone.

Equations

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

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

The isomorphism from the explicit pullback to the abstract pullback.

Equations

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

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

The homeomorphism from the explicit pullback to the abstract pullback.

Equations

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

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

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

def LightProfinite.finiteCoproduct {α : Type w} [Finite α] (X : α → LightProfinite) : LightProfinite

The "explicit" coproduct of a finite family of objects in LightProfinite, whose underlying profinite set is the disjoint union with its usual topology.

Equations

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

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

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

Equations

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

def LightProfinite.finiteCoproduct.desc {α : Type w} [Finite α] (X : α → LightProfinite) {B : LightProfinite} (e : (a : α) → X a ⟶ B) : LightProfinite.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 the universal property of the coproduct.

Equations

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

@[simp]

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

@[simp]

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

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

@[reducible, inline]

abbrev LightProfinite.finiteCoproduct.cofan {α : Type w} [Finite α] (X : α → LightProfinite) : CategoryTheory.Limits.Cofan X

The coproduct cocone associated to the explicit finite coproduct.

Equations

• LightProfinite.finiteCoproduct.cofan X = CategoryTheory.Limits.Cofan.mk (LightProfinite.finiteCoproduct X) (LightProfinite.finiteCoproduct.ι X)

def LightProfinite.finiteCoproduct.isColimit {α : Type w} [Finite α] (X : α → LightProfinite) : CategoryTheory.Limits.IsColimit (LightProfinite.finiteCoproduct.cofan X)

The explicit finite coproduct cocone is a colimit cocone.

Equations

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

instance LightProfinite.instHasColimitDiscreteFinFunctorCompObjMk (n : ℕ) (F : CategoryTheory.Functor (CategoryTheory.Discrete (Fin n)) LightProfinite) : CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor (F.obj ∘ CategoryTheory.Discrete.mk))

Equations

• ⋯ = ⋯

instance LightProfinite.instHasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts LightProfinite

Equations

• LightProfinite.instHasFiniteCoproducts = ⋯

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

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

Equations

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

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

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

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

Equations

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

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

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

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

instance LightProfinite.instHasPullbacks : CategoryTheory.Limits.HasPullbacks LightProfinite

Equations

• LightProfinite.instHasPullbacks = ⋯

noncomputable instance LightProfinite.instPreservesFiniteCoproductsProfiniteLightToProfinite : CategoryTheory.Limits.PreservesFiniteCoproducts lightToProfinite

Equations

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

noncomputable instance LightProfinite.instPreservesLimitsOfShapeProfiniteWalkingCospanLightToProfinite : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan lightToProfinite

Equations

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

instance LightProfinite.instUniqueHomOfPUnit (X : LightProfinite) : Unique (X ⟶ LightProfinite.of PUnit.{u + 1} )

Equations

• X.instUniqueHomOfPUnit = { default := { toFun := fun (x : ↑X.toCompHaus.toTop) => PUnit.unit, continuous_toFun := ⋯ }, uniq := ⋯ }

def LightProfinite.isTerminalPUnit : CategoryTheory.Limits.IsTerminal (LightProfinite.of PUnit.{u + 1} )

A one-element space is terminal in LightProfinite

Equations

• LightProfinite.isTerminalPUnit = CategoryTheory.Limits.IsTerminal.ofUnique (LightProfinite.of PUnit.{u + 1} )

instance LightProfinite.instHasTerminal : CategoryTheory.Limits.HasTerminal LightProfinite

Equations

• LightProfinite.instHasTerminal = ⋯

noncomputable def LightProfinite.terminalIsoPUnit : ⊤_ LightProfinite ≅ LightProfinite.of PUnit.{u + 1}

The isomorphism from an arbitrary terminal object of LightProfinite to a one-element space.

Equations

• LightProfinite.terminalIsoPUnit = CategoryTheory.Limits.terminalIsTerminal.uniqueUpToIso LightProfinite.isTerminalPUnit

noncomputable instance LightProfinite.instPreservesFiniteCoproductsTopCatToTopCat : CategoryTheory.Limits.PreservesFiniteCoproducts LightProfinite.toTopCat

Equations

• LightProfinite.instPreservesFiniteCoproductsTopCatToTopCat = { preserves := fun (x : Type) (x_1 : Fintype x) => inferInstance }

noncomputable instance LightProfinite.instPreservesLimitsOfShapeTopCatWalkingCospanToTopCat : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan LightProfinite.toTopCat

Equations

• LightProfinite.instPreservesLimitsOfShapeTopCatWalkingCospanToTopCat = inferInstance

instance LightProfinite.instFinitaryExtensive : CategoryTheory.FinitaryExtensive LightProfinite

Equations

• LightProfinite.instFinitaryExtensive = ⋯