Joins of category #
Given categories C, D
, this file constructs a category C ⋆ D
. Its objects are either
objects of C
or objects of D
, morphisms between objects of C
are morphisms in C
,
morphisms between object of D
are morphisms in D
, and finally, given c : C
and d : D
,
there is a unique morphism c ⟶ d
in C ⋆ D
.
Main constructions #
Join.edge c d
: the unique map fromc
tod
.Join.inclLeft : C ⥤ C ⋆ D
, the left inclusion. Its action on morphism is the main entry point to construct maps inC ⋆ D
between objects coming fromC
.Join.inclRight : D ⥤ C ⋆ D
, the left inclusion. Its action on morphism is the main entry point to construct maps inC ⋆ D
between object coming fromD
.Join.mkFunctor
, A constructor for functors out of a join of categories.Join.mkNatTrans
, A constructor for natural transformations between functors out of a join of categories.Join.mkNatIso
, A constructor for natural isomorphisms between functors out of a join of categories.
References #
Elements of Join C D
are either elements of C
or elements of D
.
- left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] : C → Join C D
- right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] : D → Join C D
Instances For
Elements of Join C D
are either elements of C
or elements of D
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Morphisms in C ⋆ D
are those of C
and D
, plus an unique
morphism (left c ⟶ right d)
for every c : C
and d : D
.
Equations
- (CategoryTheory.Join.left x_2).Hom (CategoryTheory.Join.left y) = ULift.{?u.16, ?u.17} (x_2 ⟶ y)
- (CategoryTheory.Join.right x_2).Hom (CategoryTheory.Join.right y) = ULift.{?u.47, ?u.46} (x_2 ⟶ y)
- (CategoryTheory.Join.left a).Hom (CategoryTheory.Join.right a_1) = PUnit.{max (?u.77 + 1) (?u.76 + 1)}
- (CategoryTheory.Join.right a).Hom (CategoryTheory.Join.left a_1) = PEmpty.{max (?u.103 + 1) (?u.102 + 1)}
Instances For
Identity morphisms in C ⋆ D
are inherited from those in C
and D
.
Equations
- (CategoryTheory.Join.left x_1).id = { down := CategoryTheory.CategoryStruct.id x_1 }
- (CategoryTheory.Join.right x_1).id = { down := CategoryTheory.CategoryStruct.id x_1 }
Instances For
Composition in C ⋆ D
is inherited from the compositions in C
and D
.
Equations
- CategoryTheory.Join.comp f g = { down := CategoryTheory.CategoryStruct.comp f.down g.down }
- CategoryTheory.Join.comp x_5 x_6 = PUnit.unit
- CategoryTheory.Join.comp x_5 x_6 = PUnit.unit
- CategoryTheory.Join.comp f g = { down := CategoryTheory.CategoryStruct.comp f.down g.down }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Join.edge c d is the unique morphism from c to d.
Equations
Instances For
The canonical inclusion from C to C ⋆ D
.
Terms of the form (inclLeft C D).map f
should be treated as primitive when working with joins
and one should avoid trying to reduce them. For this reason, there is no inclLeft_map
simp
lemma.
Equations
- CategoryTheory.Join.inclLeft C D = { obj := CategoryTheory.Join.left, map := fun {X Y : C} => ULift.up, map_id := ⋯, map_comp := ⋯ }
Instances For
The canonical inclusion from D to C ⋆ D
.
Terms of the form (inclRight C D).map f
should be treated as primitive when working with joins
and one should avoid trying to reduce them. For this reason, there is no inclRight_map
simp
lemma.
Equations
- CategoryTheory.Join.inclRight C D = { obj := CategoryTheory.Join.right, map := fun {X Y : D} => ULift.up, map_id := ⋯, map_comp := ⋯ }
Instances For
An induction principle for morphisms in a join of category: a morphism is either of the form
(inclLeft _ _).map _
, (inclRight _ _).map _
, or is edge _ _
.
Equations
- CategoryTheory.Join.homInduction left right edge { down := f_2 } = left x_2 y_2 f_2
- CategoryTheory.Join.homInduction left right edge { down := f_2 } = right x_2 y_2 f_2
- CategoryTheory.Join.homInduction left right edge x_3 = edge x_2 y_2
Instances For
The left inclusion is fully faithful.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The right inclusion is fully faithful.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A situational lemma to help putting identities in the form (inclLeft _ _).map _
when using
homInduction
.
A situational lemma to help putting identities in the form (inclRight _ _).map _
when using
homInduction
.
The "canonical" natural transformation from (Prod.fst C D) ⋙ inclLeft C D
to
(Prod.snd C D) ⋙ inclRight C D
. This is bundling together all the edge morphisms
into the data of a natural transformation.
Equations
- CategoryTheory.Join.edgeTransform C D = { app := fun (x : C × D) => match x with | (c, d) => CategoryTheory.Join.edge c d, naturality := ⋯ }
Instances For
A pair of functor F : C ⥤ E, G : D ⥤ E
as well as a natural transformation
α : (Prod.fst C D) ⋙ F ⟶ (Prod.snd C D) ⋙ G
. defines a functor out of C ⋆ D
.
This is the main entry point to define functors out of a join of categories.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Precomposing mkFunctor F G α
with the left inclusion gives back F
.
Equations
Instances For
Precomposing mkFunctor F G α
with the right inclusion gives back G
.
Equations
Instances For
Whiskering mkFunctor F G α
with the universal transformation gives back α
.
Construct a natural transformation between functors from a join from the data of natural transformations between each side that are compatible with the action on edge maps.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Two natural transformations between functors out of a join are equal if they are so after whiskering with the inclusions.
mkNatTrans
respects vertical composition.
Two functors out of a join of category are naturally isomorphic if their compositions with the inclusions are isomorphic and the whiskering with the canonical transformation is respected through these isomorphisms.
Equations
- CategoryTheory.Join.mkNatIso eₗ eᵣ h = { hom := CategoryTheory.Join.mkNatTrans eₗ.hom eᵣ.hom h, inv := CategoryTheory.Join.mkNatTrans eₗ.inv eᵣ.inv ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
A pair of functors ((C ⥤ E), (D ⥤ E')) induces a functor C ⋆ D ⥤ E ⋆ E'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Characterizing mapPair
on left morphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Characterizing mapPair
on right morphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Any functor out of a join is naturally isomorphic to a functor of the form mkFunctor F G α
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
mapPair
respects identities
Equations
- One or more equations did not get rendered due to their size.
Instances For
mapPair
respects composition
Equations
- One or more equations did not get rendered due to their size.
Instances For
A natural transformation Fₗ ⟶ Gₗ
induces a natural transformation
mapPair Fₗ H ⟶ mapPair Gₗ H
for every H : D ⥤ E'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A natural transformation Fᵣ ⟶ Gᵣ
induces a natural transformation
mapPair H Fᵣ ⟶ mapPair H Gᵣ
for every H : C ⥤ E
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
One can exchange mapWhiskerLeft
and mapWhiskerRight
.
A natural isomorphism Fᵣ ≅ Gᵣ
induces a natural isomorphism
mapPair H Fᵣ ≅ mapPair H Gᵣ
for every H : C ⥤ E
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A natural isomorphism Fᵣ ≅ Gᵣ
induces a natural isomorphism
mapPair Fₗ H ≅ mapPair Gₗ H
for every H : C ⥤ E
.
Equations
- One or more equations did not get rendered due to their size.