Limits in concrete categories #
In this file, we combine the description of limits in Types and the API about
the preservation of products and pullbacks in order to describe these limits in a
concrete category C.
If F : J → C is a family of objects in C, we define a bijection
Limits.Concrete.productEquiv F : (forget C).obj (∏ᶜ F) ≃ ∀ j, F j.
Similarly, if f₁ : X₁ ⟶ S and f₂ : X₂ ⟶ S are two morphisms, the elements
in pullback f₁ f₂ are identified by Limits.Concrete.pullbackEquiv
to compatible tuples of elements in X₁ × X₂.
Some results are also obtained for the terminal object, binary products, wide-pullbacks, wide-pushouts, multiequalizers and cokernels.
noncomputable def
CategoryTheory.Limits.Concrete.productEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type w}
(F : J → C)
[CategoryTheory.Limits.HasProduct F]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor F) (CategoryTheory.forget C)]
:
(CategoryTheory.forget C).obj (∏ᶜ F) ≃ ((j : J) → (CategoryTheory.forget C).obj (F j))
The equivalence (forget C).obj (∏ᶜ F) ≃ ∀ j, F j if F : J → C is a family of objects
in a concrete category C.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Concrete.productEquiv_apply_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type w}
(F : J → C)
[CategoryTheory.Limits.HasProduct F]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor F) (CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj (∏ᶜ F))
(j : J)
:
(CategoryTheory.Limits.Concrete.productEquiv F) x j = (CategoryTheory.Limits.Pi.π F j) x
@[simp]
theorem
CategoryTheory.Limits.Concrete.productEquiv_symm_apply_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type w}
(F : J → C)
[CategoryTheory.Limits.HasProduct F]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor F) (CategoryTheory.forget C)]
(x : (j : J) → (CategoryTheory.forget C).obj (F j))
(j : J)
:
(CategoryTheory.Limits.Pi.π F j) ((CategoryTheory.Limits.Concrete.productEquiv F).symm x) = x j
theorem
CategoryTheory.Limits.Concrete.Pi.map_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : Type w}
(f : J → C)
[CategoryTheory.Limits.HasProduct f]
{D : Type t}
[CategoryTheory.Category.{r, t} D]
[CategoryTheory.ConcreteCategory D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) F]
[CategoryTheory.Limits.HasProduct fun (j : J) => F.obj (f j)]
[CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.forget D)]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun (b : J) => F.obj (f b))
(CategoryTheory.forget D)]
(x : (CategoryTheory.forget D).obj (F.obj (∏ᶜ f)))
(y : (CategoryTheory.forget D).obj (F.obj (∏ᶜ f)))
(h : ∀ (i : J), (F.map (CategoryTheory.Limits.Pi.π f i)) x = (F.map (CategoryTheory.Limits.Pi.π f i)) y)
:
x = y
noncomputable def
CategoryTheory.Limits.Concrete.uniqueOfTerminalOfPreserves
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)]
(X : C)
(h : CategoryTheory.Limits.IsTerminal X)
:
Unique ((CategoryTheory.forget C).obj X)
If forget C preserves terminals and X is terminal, then (forget C).obj X is a
singleton.
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
CategoryTheory.Limits.Concrete.terminalOfUniqueOfReflects
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)]
(X : C)
(h : Unique ((CategoryTheory.forget C).obj X))
:
If forget C reflects terminals and (forget C).obj X is a singleton, then X is terminal.
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
CategoryTheory.Limits.Concrete.terminalIffUnique
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)]
[CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)]
(X : C)
:
CategoryTheory.Limits.IsTerminal X ≃ Unique ((CategoryTheory.forget C).obj X)
The equivalence IsTerminal X ≃ Unique ((forget C).obj X) if the forgetful functor
preserves and reflects terminals.
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
CategoryTheory.Limits.Concrete.terminalEquiv
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.Limits.HasTerminal C]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)]
:
(CategoryTheory.forget C).obj (⊤_ C) ≃ PUnit.{w + 1}
The equivalence (forget C).obj (⊤_ C) ≃ PUnit when C is a concrete category.
noncomputable instance
CategoryTheory.Limits.Concrete.instUniqueObjForgetTerminal
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.Limits.HasTerminal C]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)]
:
Unique ((CategoryTheory.forget C).obj (⊤_ C))
Equations
- CategoryTheory.Limits.Concrete.instUniqueObjForgetTerminal C = { default := (CategoryTheory.Limits.Concrete.terminalEquiv C).symm PUnit.unit, uniq := ⋯ }
theorem
CategoryTheory.Limits.Concrete.empty_of_initial_of_preserves
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)]
(X : C)
(h : Nonempty (CategoryTheory.Limits.IsInitial X))
:
IsEmpty ((CategoryTheory.forget C).obj X)
If forget C preserves initials and X is initial, then (forget C).obj X is empty.
theorem
CategoryTheory.Limits.Concrete.initial_of_empty_of_reflects
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)]
(X : C)
(h : IsEmpty ((CategoryTheory.forget C).obj X))
:
If forget C reflects initials and (forget C).obj X is empty, then X is initial.
theorem
CategoryTheory.Limits.Concrete.initial_iff_empty_of_preserves_of_reflects
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)]
[CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)]
(X : C)
:
Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty ((CategoryTheory.forget C).obj X)
If forget C preserves and reflects initials, then X is initial if and only if
(forget C).obj X is empty.
noncomputable def
CategoryTheory.Limits.Concrete.prodEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
(X₁ : C)
(X₂ : C)
[CategoryTheory.Limits.HasBinaryProduct X₁ X₂]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)]
:
(CategoryTheory.forget C).obj (X₁ ⨯ X₂) ≃ (CategoryTheory.forget C).obj X₁ × (CategoryTheory.forget C).obj X₂
The equivalence (forget C).obj (X₁ ⨯ X₂) ≃ ((forget C).obj X₁) × ((forget C).obj X₂)
if X₁ and X₂ are objects in a concrete category C.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Concrete.prodEquiv_apply_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
(X₁ : C)
(X₂ : C)
[CategoryTheory.Limits.HasBinaryProduct X₁ X₂]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj (X₁ ⨯ X₂))
:
((CategoryTheory.Limits.Concrete.prodEquiv X₁ X₂) x).1 = CategoryTheory.Limits.prod.fst x
@[simp]
theorem
CategoryTheory.Limits.Concrete.prodEquiv_apply_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
(X₁ : C)
(X₂ : C)
[CategoryTheory.Limits.HasBinaryProduct X₁ X₂]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj (X₁ ⨯ X₂))
:
((CategoryTheory.Limits.Concrete.prodEquiv X₁ X₂) x).2 = CategoryTheory.Limits.prod.snd x
@[simp]
theorem
CategoryTheory.Limits.Concrete.prodEquiv_symm_apply_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
(X₁ : C)
(X₂ : C)
[CategoryTheory.Limits.HasBinaryProduct X₁ X₂]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj X₁ × (CategoryTheory.forget C).obj X₂)
:
CategoryTheory.Limits.prod.fst ((CategoryTheory.Limits.Concrete.prodEquiv X₁ X₂).symm x) = x.1
@[simp]
theorem
CategoryTheory.Limits.Concrete.prodEquiv_symm_apply_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
(X₁ : C)
(X₂ : C)
[CategoryTheory.Limits.HasBinaryProduct X₁ X₂]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj X₁ × (CategoryTheory.forget C).obj X₂)
:
CategoryTheory.Limits.prod.snd ((CategoryTheory.Limits.Concrete.prodEquiv X₁ X₂).symm x) = x.2
noncomputable def
CategoryTheory.Limits.Concrete.pullbackEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{X₁ : C}
{X₂ : C}
{S : C}
(f₁ : X₁ ⟶ S)
(f₂ : X₂ ⟶ S)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂) (CategoryTheory.forget C)]
:
(CategoryTheory.forget C).obj (CategoryTheory.Limits.pullback f₁ f₂) ≃ { p : (CategoryTheory.forget C).obj X₁ × (CategoryTheory.forget C).obj X₂ // f₁ p.1 = f₂ p.2 }
In a concrete category C, given two morphisms f₁ : X₁ ⟶ S and f₂ : X₂ ⟶ S,
the elements in pullback f₁ f₁ can be identified to compatible tuples of
elements in X₁ and X₂.
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
CategoryTheory.Limits.Concrete.pullbackMk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{X₁ : C}
{X₂ : C}
{S : C}
(f₁ : X₁ ⟶ S)
(f₂ : X₂ ⟶ S)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂) (CategoryTheory.forget C)]
(x₁ : (CategoryTheory.forget C).obj X₁)
(x₂ : (CategoryTheory.forget C).obj X₂)
(h : f₁ x₁ = f₂ x₂)
:
(CategoryTheory.forget C).obj (CategoryTheory.Limits.pullback f₁ f₂)
Constructor for elements in a pullback in a concrete category.
Equations
- CategoryTheory.Limits.Concrete.pullbackMk f₁ f₂ x₁ x₂ h = (CategoryTheory.Limits.Concrete.pullbackEquiv f₁ f₂).symm ⟨(x₁, x₂), h⟩
theorem
CategoryTheory.Limits.Concrete.pullbackMk_surjective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{X₁ : C}
{X₂ : C}
{S : C}
(f₁ : X₁ ⟶ S)
(f₂ : X₂ ⟶ S)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂) (CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.pullback f₁ f₂))
:
∃ (x₁ : (CategoryTheory.forget C).obj X₁) (x₂ : (CategoryTheory.forget C).obj X₂) (h : f₁ x₁ = f₂ x₂),
x = CategoryTheory.Limits.Concrete.pullbackMk f₁ f₂ x₁ x₂ h
@[simp]
theorem
CategoryTheory.Limits.Concrete.pullbackMk_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{X₁ : C}
{X₂ : C}
{S : C}
(f₁ : X₁ ⟶ S)
(f₂ : X₂ ⟶ S)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂) (CategoryTheory.forget C)]
(x₁ : (CategoryTheory.forget C).obj X₁)
(x₂ : (CategoryTheory.forget C).obj X₂)
(h : f₁ x₁ = f₂ x₂)
:
(CategoryTheory.Limits.pullback.fst f₁ f₂) (CategoryTheory.Limits.Concrete.pullbackMk f₁ f₂ x₁ x₂ h) = x₁
@[simp]
theorem
CategoryTheory.Limits.Concrete.pullbackMk_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{X₁ : C}
{X₂ : C}
{S : C}
(f₁ : X₁ ⟶ S)
(f₂ : X₂ ⟶ S)
[CategoryTheory.Limits.HasPullback f₁ f₂]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂) (CategoryTheory.forget C)]
(x₁ : (CategoryTheory.forget C).obj X₁)
(x₂ : (CategoryTheory.forget C).obj X₂)
(h : f₁ x₁ = f₂ x₂)
:
(CategoryTheory.Limits.pullback.snd f₁ f₂) (CategoryTheory.Limits.Concrete.pullbackMk f₁ f₂ x₁ x₂ h) = x₂
theorem
CategoryTheory.Limits.Concrete.widePullback_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{B : C}
{ι : Type w}
{X : ι → C}
(f : (j : ι) → X j ⟶ B)
[CategoryTheory.Limits.HasWidePullback B X f]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.WidePullbackShape.wideCospan B X f)
(CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.widePullback B X f))
(y : (CategoryTheory.forget C).obj (CategoryTheory.Limits.widePullback B X f))
(h₀ : (CategoryTheory.Limits.WidePullback.base f) x = (CategoryTheory.Limits.WidePullback.base f) y)
(h : ∀ (j : ι), (CategoryTheory.Limits.WidePullback.π f j) x = (CategoryTheory.Limits.WidePullback.π f j) y)
:
x = y
theorem
CategoryTheory.Limits.Concrete.widePullback_ext'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{B : C}
{ι : Type w}
[Nonempty ι]
{X : ι → C}
(f : (j : ι) → X j ⟶ B)
[CategoryTheory.Limits.HasWidePullback B X f]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.WidePullbackShape.wideCospan B X f)
(CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.widePullback B X f))
(y : (CategoryTheory.forget C).obj (CategoryTheory.Limits.widePullback B X f))
(h : ∀ (j : ι), (CategoryTheory.Limits.WidePullback.π f j) x = (CategoryTheory.Limits.WidePullback.π f j) y)
:
x = y
theorem
CategoryTheory.Limits.Concrete.multiequalizer_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{I : CategoryTheory.Limits.MulticospanIndex C}
[CategoryTheory.Limits.HasMultiequalizer I]
[CategoryTheory.Limits.PreservesLimit I.multicospan (CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.multiequalizer I))
(y : (CategoryTheory.forget C).obj (CategoryTheory.Limits.multiequalizer I))
(h : ∀ (t : I.L), (CategoryTheory.Limits.Multiequalizer.ι I t) x = (CategoryTheory.Limits.Multiequalizer.ι I t) y)
:
x = y
def
CategoryTheory.Limits.Concrete.multiequalizerEquivAux
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
(I : CategoryTheory.Limits.MulticospanIndex C)
:
↑(I.multicospan.comp (CategoryTheory.forget C)).sections ≃ { x : (i : I.L) → (CategoryTheory.forget C).obj (I.left i) //
∀ (i : I.R), (I.fst i) (x (I.fstTo i)) = (I.snd i) (x (I.sndTo i)) }
An auxiliary equivalence to be used in multiequalizerEquiv below.
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
CategoryTheory.Limits.Concrete.multiequalizerEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
(I : CategoryTheory.Limits.MulticospanIndex C)
[CategoryTheory.Limits.HasMultiequalizer I]
[CategoryTheory.Limits.PreservesLimit I.multicospan (CategoryTheory.forget C)]
:
(CategoryTheory.forget C).obj (CategoryTheory.Limits.multiequalizer I) ≃ { x : (i : I.L) → (CategoryTheory.forget C).obj (I.left i) //
∀ (i : I.R), (I.fst i) (x (I.fstTo i)) = (I.snd i) (x (I.sndTo i)) }
The equivalence between the noncomputable multiequalizer and the concrete multiequalizer.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Concrete.multiequalizerEquiv_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
(I : CategoryTheory.Limits.MulticospanIndex C)
[CategoryTheory.Limits.HasMultiequalizer I]
[CategoryTheory.Limits.PreservesLimit I.multicospan (CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.multiequalizer I))
(i : I.L)
:
theorem
CategoryTheory.Limits.Concrete.widePushout_exists_rep
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{B : C}
{α : Type v}
{X : α → C}
(f : (j : α) → B ⟶ X j)
[CategoryTheory.Limits.HasWidePushout B X f]
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.WidePushoutShape.wideSpan B X f) (CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.widePushout B X f))
:
(∃ (y : (CategoryTheory.forget C).obj B), (CategoryTheory.Limits.WidePushout.head f) y = x) ∨ ∃ (i : α) (y : (CategoryTheory.forget C).obj (X i)), (CategoryTheory.Limits.WidePushout.ι f i) y = x
theorem
CategoryTheory.Limits.Concrete.widePushout_exists_rep'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{B : C}
{α : Type v}
[Nonempty α]
{X : α → C}
(f : (j : α) → B ⟶ X j)
[CategoryTheory.Limits.HasWidePushout B X f]
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.WidePushoutShape.wideSpan B X f) (CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.widePushout B X f))
:
∃ (i : α) (y : (CategoryTheory.forget C).obj (X i)), (CategoryTheory.Limits.WidePushout.ι f i) y = x
theorem
CategoryTheory.Limits.Concrete.cokernel_funext
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.ConcreteCategory C]
{M : C}
{N : C}
{K : C}
{f : M ⟶ N}
[CategoryTheory.Limits.HasCokernel f]
{g : CategoryTheory.Limits.cokernel f ⟶ K}
{h : CategoryTheory.Limits.cokernel f ⟶ K}
(w : ∀ (n : (CategoryTheory.forget C).obj N),
g ((CategoryTheory.Limits.cokernel.π f) n) = h ((CategoryTheory.Limits.cokernel.π f) n))
:
g = h