Category instances for algebraic structures that use bundled homs. #
Many algebraic structures in Lean initially used unbundled homs (e.g. a bare function between types,
along with an is_monoid_hom
typeclass), but the general trend is towards using bundled homs.
This file provides a basic infrastructure to define concrete categories using bundled homs, and define forgetful functors between them.
- to_fun : Π {α β : Type ?} (Iα : c α) (Iβ : c β), hom Iα Iβ → α → β
- id : Π {α : Type ?} (I : c α), hom I I
- comp : Π {α β γ : Type ?} (Iα : c α) (Iβ : c β) (Iγ : c γ), hom Iβ Iγ → hom Iα Iβ → hom Iα Iγ
- hom_ext : (∀ {α β : Type ?} (Iα : c α) (Iβ : c β), function.injective (self.to_fun Iα Iβ)) . "obviously"
- id_to_fun : (∀ {α : Type ?} (I : c α), self.to_fun I I (self.id I) = id) . "obviously"
- comp_to_fun : (∀ {α β γ : Type ?} (Iα : c α) (Iβ : c β) (Iγ : c γ) (f : hom Iα Iβ) (g : hom Iβ Iγ), self.to_fun Iα Iγ (self.comp Iα Iβ Iγ g f) = self.to_fun Iβ Iγ g ∘ self.to_fun Iα Iβ f) . "obviously"
Class for bundled homs. Note that the arguments order follows that of lemmas for monoid_hom
.
This way we can use ⟨@monoid_hom.to_fun, @monoid_hom.id ...⟩
in an instance.
Instances of this typeclass
- category_theory.bundled_hom.bundled_hom_of_parent_projection
- Mon.bundled_hom
- AddMon.bundled_hom
- SemiRing.bundled_hom
- Preorder.order_hom.category_theory.bundled_hom
- Lattice.lattice_hom.category_theory.bundled_hom
- Magma.bundled_hom
- AddMagma.bundled_hom
- Top.bundled_hom
- SemiNormedGroup.bundled_hom
- category_theory.unbundled_hom.bundled_hom
- CompleteLattice.complete_lattice_hom.category_theory.bundled_hom
- Frame.bundled_hom
- ωCPO.omega_complete_partial_order.continuous_hom.category_theory.bundled_hom
- Born.locally_bounded_map.category_theory.bundled_hom
Instances of other typeclasses for category_theory.bundled_hom
- category_theory.bundled_hom.has_sizeof_inst
Every @bundled_hom c _
defines a category with objects in bundled c
.
This instance generates the type-class problem bundled_hom ?m
(which is why this is marked as
[nolint]
). Currently that is not a problem, as there are almost no instances of bundled_hom
.
Equations
- category_theory.bundled_hom.category hom = {to_category_struct := {to_quiver := {hom := λ (X Y : category_theory.bundled c), hom X.str Y.str}, id := λ (X : category_theory.bundled c), 𝒞.id X.str, comp := λ (X Y Z : category_theory.bundled c) (f : X ⟶ Y) (g : Y ⟶ Z), 𝒞.comp X.str Y.str Z.str g f}, id_comp' := _, comp_id' := _, assoc' := _}
A category given by bundled_hom
is a concrete category.
This instance generates the type-class problem bundled_hom ?m
(which is why this is marked as
[nolint]
). Currently that is not a problem, as there are almost no instances of bundled_hom
.
Equations
- category_theory.bundled_hom.concrete_category hom = category_theory.concrete_category.mk {obj := λ (X : category_theory.bundled c), ↥X, map := λ (X Y : category_theory.bundled c) (f : X ⟶ Y), 𝒞.to_fun X.str Y.str f, map_id' := _, map_comp' := _}
A version of has_forget₂.mk'
for categories defined using @bundled_hom
.
Equations
- category_theory.bundled_hom.mk_has_forget₂ obj map h_map = category_theory.has_forget₂.mk' (category_theory.bundled.map obj) _ map _
The hom
corresponding to first forgetting along F
, then taking the hom
associated to c
.
For typical usage, see the construction of CommMon
from Mon
.
Equations
- category_theory.bundled_hom.map_hom hom F = λ (α β : Type u) (iα : d α) (iβ : d β), hom (F iα) (F iβ)
Construct the bundled_hom
induced by a map between type classes.
This is useful for building categories such as CommMon
from Mon
.
Equations
- category_theory.bundled_hom.map hom F = {to_fun := λ (α β : Type u) (iα : d α) (iβ : d β) (f : category_theory.bundled_hom.map_hom hom F iα iβ), 𝒞.to_fun (F iα) (F iβ) f, id := λ (α : Type u) (iα : d α), 𝒞.id (F iα), comp := λ (α β γ : Type u) (iα : d α) (iβ : d β) (iγ : d γ) (f : category_theory.bundled_hom.map_hom hom F iβ iγ) (g : category_theory.bundled_hom.map_hom hom F iα iβ), 𝒞.comp (F iα) (F iβ) (F iγ) f g, hom_ext := _, id_to_fun := _, comp_to_fun := _}
We use the empty parent_projection
class to label functions like comm_monoid.to_monoid
,
which we would like to use to automatically construct bundled_hom
instances from.
Once we've set up Mon
as the category of bundled monoids,
this allows us to set up CommMon
by defining an instance
instance : parent_projection (comm_monoid.to_monoid) := ⟨⟩
Instances of this typeclass
- CommMon.comm_monoid.to_monoid.category_theory.bundled_hom.parent_projection
- AddCommMon.comm_monoid.to_monoid.category_theory.bundled_hom.parent_projection
- Group.group.to_monoid.category_theory.bundled_hom.parent_projection
- AddGroup.group.to_monoid.category_theory.bundled_hom.parent_projection
- CommGroup.comm_group.to_group.category_theory.bundled_hom.parent_projection
- AddCommGroup.comm_group.to_group.category_theory.bundled_hom.parent_projection
- Ring.ring.to_semiring.category_theory.bundled_hom.parent_projection
- CommSemiRing.comm_semiring.to_semiring.category_theory.bundled_hom.parent_projection
- CommRing.comm_ring.to_ring.category_theory.bundled_hom.parent_projection
- PartialOrder.partial_order.to_preorder.category_theory.bundled_hom.parent_projection
- DistribLattice.distrib_lattice.to_lattice.category_theory.bundled_hom.parent_projection
- BoolRing.boolean_ring.to_comm_ring.category_theory.bundled_hom.parent_projection
- Semigroup.semigroup.to_has_mul.category_theory.bundled_hom.parent_projection
- AddSemigroup.semigroup.to_has_mul.category_theory.bundled_hom.parent_projection
- LinearOrder.linear_order.to_partial_order.category_theory.bundled_hom.parent_projection
- NonemptyFinLinOrd.nonempty_fin_lin_ord.to_linear_order.category_theory.bundled_hom.parent_projection
Instances of other typeclasses for category_theory.bundled_hom.parent_projection
- category_theory.bundled_hom.parent_projection.has_sizeof_inst
Equations
Equations
- category_theory.bundled_hom.forget₂ hom F = {forget₂ := {obj := λ (X : category_theory.bundled d), {α := ↥X, str := F X.str}, map := λ (X Y : category_theory.bundled d) (f : X ⟶ Y), f, map_id' := _, map_comp' := _}, forget_comp := _}
Equations
- category_theory.bundled_hom.forget₂_full hom F = {preimage := λ (X Y : category_theory.bundled d) (f : (category_theory.forget₂ (category_theory.bundled d) (category_theory.bundled c)).obj X ⟶ (category_theory.forget₂ (category_theory.bundled d) (category_theory.bundled c)).obj Y), f, witness' := _}