mathlib docs: category_theory.concrete_category.bundled

@[class]

structure category_theory.bundled_hom {c : Type u → Type u} :

(Π ⦃α β : Type u⦄, c α → c β → Type u) → Type (u+1)

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 (c_1.to_fun Iα Iβ)) . "obviously"
id_to_fun : (∀ {α : Type ?} (I : c α), c_1.to_fun I I (c_1.id I) = id) . "obviously"
comp_to_fun : (∀ {α β γ : Type ?} (Iα : c α) (Iβ : c β) (Iγ : c γ) (f : hom Iα Iβ) (g : hom Iβ Iγ), c_1.to_fun Iα Iγ (c_1.comp Iα Iβ Iγ g f) = c_1.to_fun Iβ Iγ g ∘ c_1.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

source

@[nolint, instance]

def category_theory.bundled_hom.category {c : Type u → Type u} (hom : Π ⦃α β : Type u⦄, c α → c β → Type u) [𝒞 : category_theory.bundled_hom hom] :

category_theory.category (category_theory.bundled c)

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_has_hom := {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' := _}

source

@[nolint, instance]

def category_theory.bundled_hom.category_theory.concrete_category {c : Type u → Type u} (hom : Π ⦃α β : Type u⦄, c α → c β → Type u) [𝒞 : category_theory.bundled_hom hom] :

category_theory.concrete_category (category_theory.bundled c)

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.category_theory.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' := _}

source

def category_theory.bundled_hom.mk_has_forget₂ {c : Type u → Type u} {hom : Π ⦃α β : Type u⦄, c α → c β → Type u} [𝒞 : category_theory.bundled_hom hom] {d : Type u → Type u} {hom_d : Π ⦃α β : Type u⦄, d α → d β → Type u} [category_theory.bundled_hom hom_d] (obj : Π ⦃α : Type u⦄, c α → d α) (map : Π {X Y : category_theory.bundled c}, (X ⟶ Y) → (category_theory.bundled.map obj X ⟶ category_theory.bundled.map obj Y)) :

(∀ {X Y : category_theory.bundled c} (f : X ⟶ Y), ⇑(map f) = ⇑f) → category_theory.has_forget₂ (category_theory.bundled c) (category_theory.bundled d)

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 _

source

def category_theory.bundled_hom.map_hom {c : Type u → Type u} (hom : Π ⦃α β : Type u⦄, c α → c β → Type u) {d : Type u → Type u} (F : Π {α : Type u}, d α → c α) ⦃α β : Type u⦄ :

d α → d β → Type u

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β)

source

def category_theory.bundled_hom.map {c : Type u → Type u} (hom : Π ⦃α β : Type u⦄, c α → c β → Type u) [𝒞 : category_theory.bundled_hom hom] {d : Type u → Type u} (F : Π {α : Type u}, d α → c α) :

category_theory.bundled_hom (category_theory.bundled_hom.map_hom hom F)

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 := _}

source

@[class]

inductive category_theory.bundled_hom.parent_projection {c d : Type u → Type u} :

(Π {α : Type u}, d α → c α) → Type

mk : Π {c d : Type u → Type u} (F : Π {α : Type u}, d α → c α), category_theory.bundled_hom.parent_projection F

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

source

@[nolint, instance]

def category_theory.bundled_hom.bundled_hom_of_parent_projection {c : Type u → Type u} (hom : Π ⦃α β : Type u⦄, c α → c β → Type u) [𝒞 : category_theory.bundled_hom hom] {d : Type u → Type u} (F : Π {α : Type u}, d α → c α) [category_theory.bundled_hom.parent_projection F] :

category_theory.bundled_hom (category_theory.bundled_hom.map_hom hom F)

Equations

category_theory.bundled_hom.bundled_hom_of_parent_projection hom F = category_theory.bundled_hom.map hom F

source

@[instance]

def category_theory.bundled_hom.forget₂ {c : Type u → Type u} (hom : Π ⦃α β : Type u⦄, c α → c β → Type u) [𝒞 : category_theory.bundled_hom hom] {d : Type u → Type u} (F : Π {α : Type u}, d α → c α) [category_theory.bundled_hom.parent_projection F] :

category_theory.has_forget₂ (category_theory.bundled d) (category_theory.bundled c)

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 := _}

source

@[instance]

def category_theory.bundled_hom.forget₂_full {c : Type u → Type u} (hom : Π ⦃α β : Type u⦄, c α → c β → Type u) [𝒞 : category_theory.bundled_hom hom] {d : Type u → Type u} (F : Π {α : Type u}, d α → c α) [category_theory.bundled_hom.parent_projection F] :

category_theory.full (category_theory.forget₂ (category_theory.bundled d) (category_theory.bundled c))

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' := _}

mathlib documentation

category_theory.concrete_category.bundled_hom

Category instances for algebraic structures that use bundled homs.

General documentation

Additional documentation

Library

mathlib documentation

category_theory.​concrete_category.​bundled_hom

Category instances for algebraic structures that use bundled homs.

General documentation

Additional documentation

Library

category_theory.concrete_category.bundled_hom