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.
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.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
The equivalence (forget C).obj (⊤_ C) ≃ PUnit
when C
is a concrete category.
Equations
Instances For
Equations
- CategoryTheory.Limits.Concrete.instUniqueObjForgetTerminal C = { default := (CategoryTheory.Limits.Concrete.terminalEquiv C).symm PUnit.unit, uniq := ⋯ }
If forget C
preserves initials and X
is initial, then (forget C).obj X
is empty.
If forget C
reflects initials and (forget C).obj X
is empty, then X
is initial.
If forget C
preserves and reflects initials, then X
is initial if and only if
(forget C).obj X
is empty.
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.
Instances For
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.
Instances For
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⟩
Instances For
An auxiliary equivalence to be used in multiequalizerEquiv
below.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The equivalence between the noncomputable multiequalizer and the concrete multiequalizer.
Equations
- One or more equations did not get rendered due to their size.