Prelax functors and locally discrete bicategories #
In a locally discrete bicategory every 2-morphism η : f ⟶ g forces f = g, so a prelax
functor (in particular a pseudofunctor) sends η to an eqToHom. This lets the coherence
data of a pseudofunctor out of LocallyDiscrete B₀, such as F.map₂ (α_ f g h).hom, be
computed componentwise.
Dually, the unit and composition comparisons of a pseudofunctor P into a locally discrete
bicategory are determined by equalities of 1-morphisms. So the comparisons of a composite
P.comp F are the flexible comparisons F.mapId' and F.mapComp' of F at the images of
P, for instance for P = Functor.toPseudofunctor ψ induced by a functor of categories.
Consequently, pulling F : LocallyDiscrete Λ ⥤ᵖ C back along the identity functor, or along a
composite f ⋙ g instead of first along g and then along f, does not change its unit and
composition comparisons.
Finally, CategoryTheory.LocallyDiscrete.mkCatPseudofunctor builds a pseudofunctor
LocallyDiscrete B₀ ⥤ᵖ Cat from functors, unit isomorphisms and composition isomorphisms
map fg ≅ map f ⋙ map g given at arbitrary factorizations f ≫ g = fg, from componentwise
associativity and unit laws.
theorem
CategoryTheory.PrelaxFunctor.map₂_eq_eqToHom
{B : Type u_1}
{C : Type u_2}
[Bicategory B]
[Bicategory.IsLocallyDiscrete B]
[Bicategory C]
(F : PrelaxFunctor B C)
{a b : B}
{f g : a ⟶ b}
(η : f ⟶ g)
:
A prelax functor out of a locally discrete bicategory sends every 2-morphism to an
eqToHom.
theorem
CategoryTheory.PrelaxFunctor.map₂_comp_map₂
{B : Type u_1}
{C : Type u_2}
[Bicategory B]
[Bicategory.IsLocallyDiscrete B]
[Bicategory C]
(F : PrelaxFunctor B C)
{a b : B}
{f g h : a ⟶ b}
(η : f ⟶ g)
(θ : g ⟶ h)
(ι : f ⟶ h)
:
A prelax functor out of a locally discrete bicategory sends a composite of two 2-morphisms
to the image of any 2-morphism with the same source and target.
theorem
CategoryTheory.PrelaxFunctor.map₂_comp_map₂_assoc
{B : Type u_1}
{C : Type u_2}
[Bicategory B]
[Bicategory.IsLocallyDiscrete B]
[Bicategory C]
(F : PrelaxFunctor B C)
{a b : B}
{f g h : a ⟶ b}
(η : f ⟶ g)
(θ : g ⟶ h)
(ι : f ⟶ h)
{Z : F.obj a ⟶ F.obj b}
(h✝ : F.map h ⟶ Z)
:
CategoryStruct.comp (F.map₂ η) (CategoryStruct.comp (F.map₂ θ) h✝) = CategoryStruct.comp (F.map₂ ι) h✝
A prelax functor out of a locally discrete bicategory sends a composite of two 2-morphisms
to the image of any 2-morphism with the same source and target.
theorem
CategoryTheory.Pseudofunctor.comp_mapId_eq_mapId'
{B₀ : Type u_1}
[Bicategory B₀]
{B₁ : Type u_2}
[Bicategory B₁]
[Bicategory.IsLocallyDiscrete B₁]
{C : Type u_3}
[Bicategory C]
(P : Pseudofunctor B₀ B₁)
(F : Pseudofunctor B₁ C)
(a : B₀)
:
The unit comparison of the composite of a pseudofunctor P into a locally discrete
bicategory with F is the unit comparison of F at the 1-morphism P.map (𝟙 a), which
equals 𝟙 (P.obj a).
theorem
CategoryTheory.Pseudofunctor.comp_mapComp_eq_mapComp'
{B₀ : Type u_1}
[Bicategory B₀]
{B₁ : Type u_2}
[Bicategory B₁]
[Bicategory.IsLocallyDiscrete B₁]
{C : Type u_3}
[Bicategory C]
(P : Pseudofunctor B₀ B₁)
(F : Pseudofunctor B₁ C)
{a b c : B₀}
(f : a ⟶ b)
(g : b ⟶ c)
:
The composition comparison of the composite of a pseudofunctor P into a locally discrete
bicategory with F is the composition comparison of F at the factorization
P.map f ≫ P.map g = P.map (f ≫ g).
theorem
CategoryTheory.Pseudofunctor.comp_mapId'_eq_mapId'
{B₀ : Type u_1}
[Bicategory B₀]
{B₁ : Type u_2}
[Bicategory B₁]
[Bicategory.IsLocallyDiscrete B₁]
{C : Type u_3}
[Bicategory C]
(P : Pseudofunctor B₀ B₁)
(F : Pseudofunctor B₁ C)
{a : B₀}
(u : a ⟶ a)
(hu : u = CategoryStruct.id a)
:
The flexible unit comparison of the composite of a pseudofunctor P into a locally discrete
bicategory with F, at a 1-morphism u equal to an identity, is the flexible unit comparison
of F at P.map u.
theorem
CategoryTheory.Pseudofunctor.comp_mapComp'_eq_mapComp'
{B₀ : Type u_1}
[Bicategory B₀]
{B₁ : Type u_2}
[Bicategory B₁]
[Bicategory.IsLocallyDiscrete B₁]
{C : Type u_3}
[Bicategory C]
(P : Pseudofunctor B₀ B₁)
(F : Pseudofunctor B₁ C)
{a b c : B₀}
(u : a ⟶ b)
(v : b ⟶ c)
(uv : a ⟶ c)
(huv : CategoryStruct.comp u v = uv)
:
The flexible composition comparison of the composite of a pseudofunctor P into a locally
discrete bicategory with F is the flexible composition comparison of F at the images under
P.
Pulling back along identities and composites of functors #
theorem
CategoryTheory.Pseudofunctor.toPseudofunctor_id_comp_mapId
{Γ : Type u_4}
[Category.{u_8, u_4} Γ]
{C : Type u_7}
[Bicategory C]
(F : Pseudofunctor (LocallyDiscrete Γ) C)
(x : LocallyDiscrete Γ)
:
Pulling back along the identity functor does not change the unit comparisons.
theorem
CategoryTheory.Pseudofunctor.toPseudofunctor_id_comp_mapComp
{Γ : Type u_4}
[Category.{u_8, u_4} Γ]
{C : Type u_7}
[Bicategory C]
(F : Pseudofunctor (LocallyDiscrete Γ) C)
{x y z : LocallyDiscrete Γ}
(φ : x ⟶ y)
(ψ : y ⟶ z)
:
Pulling back along the identity functor does not change the composition comparisons.
theorem
CategoryTheory.Pseudofunctor.toPseudofunctor_comp_comp_mapId
{Γ : Type u_4}
[Category.{u_8, u_4} Γ]
{Λ : Type u_5}
[Category.{u_9, u_5} Λ]
{Λ' : Type u_6}
[Category.{u_10, u_6} Λ']
{C : Type u_7}
[Bicategory C]
(f : Functor Γ Λ)
(g : Functor Λ Λ')
(F : Pseudofunctor (LocallyDiscrete Λ') C)
(x : LocallyDiscrete Γ)
:
((f.comp g).toPseudofunctor.comp F).mapId x = (f.toPseudofunctor.comp (g.toPseudofunctor.comp F)).mapId x
Pulling back along a composite functor f ⋙ g has the same unit comparisons as pulling back
along g and then along f.
theorem
CategoryTheory.Pseudofunctor.toPseudofunctor_comp_comp_mapComp
{Γ : Type u_4}
[Category.{u_8, u_4} Γ]
{Λ : Type u_5}
[Category.{u_9, u_5} Λ]
{Λ' : Type u_6}
[Category.{u_10, u_6} Λ']
{C : Type u_7}
[Bicategory C]
(f : Functor Γ Λ)
(g : Functor Λ Λ')
(F : Pseudofunctor (LocallyDiscrete Λ') C)
{x y z : LocallyDiscrete Γ}
(φ : x ⟶ y)
(ψ : y ⟶ z)
:
((f.comp g).toPseudofunctor.comp F).mapComp φ ψ = (f.toPseudofunctor.comp (g.toPseudofunctor.comp F)).mapComp φ ψ
Pulling back along a composite functor f ⋙ g has the same composition comparisons as
pulling back along g and then along f.
theorem
CategoryTheory.LocallyDiscrete.inv_associativity_of_hom_associativity
{B₀ : Type u_1}
[Category.{u_2, u_1} B₀]
{obj : B₀ → Cat}
{map : {b b' : B₀} → (b ⟶ b') → Functor ↑(obj b) ↑(obj b')}
(mapComp :
{b₀ b₁ b₂ : B₀} →
(f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → (fg : b₀ ⟶ b₂) → CategoryStruct.comp f g = fg → ((map f).comp (map g) ≅ map fg))
(associativity :
∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃) (fg : b₀ ⟶ b₂) (gh : b₁ ⟶ b₃) (fgh : b₀ ⟶ b₃)
(hfg : CategoryStruct.comp f g = fg) (hgh : CategoryStruct.comp g h = gh) (hfgh : CategoryStruct.comp fg h = fgh)
(hfgh' : CategoryStruct.comp f gh = fgh) (x : ↑(obj b₀)),
CategoryStruct.comp ((map h).map ((mapComp f g fg hfg).hom.app x)) ((mapComp fg h fgh hfgh).hom.app x) = CategoryStruct.comp ((mapComp g h gh hgh).hom.app ((map f).obj x)) ((mapComp f gh fgh hfgh').hom.app x))
{b₀ b₁ b₂ b₃ : B₀}
(f : b₀ ⟶ b₁)
(g : b₁ ⟶ b₂)
(h : b₂ ⟶ b₃)
(fg : b₀ ⟶ b₂)
(gh : b₁ ⟶ b₃)
(fgh : b₀ ⟶ b₃)
(hfg : CategoryStruct.comp f g = fg)
(hgh : CategoryStruct.comp g h = gh)
(hfgh : CategoryStruct.comp fg h = fgh)
(hfgh' : CategoryStruct.comp f gh = fgh)
(x : ↑(obj b₀))
:
Associativity of composition isomorphisms map f ⋙ map g ≅ map fg of a family of functors,
given at arbitrary factorizations, implies the associativity of their inverses.
theorem
CategoryTheory.LocallyDiscrete.inv_associativity_of_hom_associativity_assoc
{B₀ : Type u_1}
[Category.{u_2, u_1} B₀]
{obj : B₀ → Cat}
{map : {b b' : B₀} → (b ⟶ b') → Functor ↑(obj b) ↑(obj b')}
(mapComp :
{b₀ b₁ b₂ : B₀} →
(f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → (fg : b₀ ⟶ b₂) → CategoryStruct.comp f g = fg → ((map f).comp (map g) ≅ map fg))
(associativity :
∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃) (fg : b₀ ⟶ b₂) (gh : b₁ ⟶ b₃) (fgh : b₀ ⟶ b₃)
(hfg : CategoryStruct.comp f g = fg) (hgh : CategoryStruct.comp g h = gh) (hfgh : CategoryStruct.comp fg h = fgh)
(hfgh' : CategoryStruct.comp f gh = fgh) (x : ↑(obj b₀)),
CategoryStruct.comp ((map h).map ((mapComp f g fg hfg).hom.app x)) ((mapComp fg h fgh hfgh).hom.app x) = CategoryStruct.comp ((mapComp g h gh hgh).hom.app ((map f).obj x)) ((mapComp f gh fgh hfgh').hom.app x))
{b₀ b₁ b₂ b₃ : B₀}
(f : b₀ ⟶ b₁)
(g : b₁ ⟶ b₂)
(h : b₂ ⟶ b₃)
(fg : b₀ ⟶ b₂)
(gh : b₁ ⟶ b₃)
(fgh : b₀ ⟶ b₃)
(hfg : CategoryStruct.comp f g = fg)
(hgh : CategoryStruct.comp g h = gh)
(hfgh : CategoryStruct.comp fg h = fgh)
(hfgh' : CategoryStruct.comp f gh = fgh)
(x : ↑(obj b₀))
{Z : ↑(obj b₃)}
(h✝ : (map h).obj ((map g).obj ((map f).obj x)) ⟶ Z)
:
CategoryStruct.comp ((mapComp fg h fgh hfgh).inv.app x)
(CategoryStruct.comp ((map h).map ((mapComp f g fg hfg).inv.app x)) h✝) = CategoryStruct.comp ((mapComp f gh fgh hfgh').inv.app x)
(CategoryStruct.comp ((mapComp g h gh hgh).inv.app ((map f).obj x)) h✝)
Associativity of composition isomorphisms map f ⋙ map g ≅ map fg of a family of functors,
given at arbitrary factorizations, implies the associativity of their inverses.
def
CategoryTheory.LocallyDiscrete.mkCatPseudofunctor
{B₀ : Type u_1}
[Category.{u_2, u_1} B₀]
{obj : B₀ → Cat}
(map : {b b' : B₀} → (b ⟶ b') → Functor ↑(obj b) ↑(obj b'))
(mapId : (b : B₀) → map (CategoryStruct.id b) ≅ Functor.id ↑(obj b))
(mapComp :
{b₀ b₁ b₂ : B₀} →
(f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → (fg : b₀ ⟶ b₂) → CategoryStruct.comp f g = fg → (map fg ≅ (map f).comp (map g)))
(associativity :
∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃) (fg : b₀ ⟶ b₂) (gh : b₁ ⟶ b₃) (fgh : b₀ ⟶ b₃)
(hfg : CategoryStruct.comp f g = fg) (hgh : CategoryStruct.comp g h = gh) (hfgh : CategoryStruct.comp fg h = fgh)
(hfgh' : CategoryStruct.comp f gh = fgh) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp fg h fgh hfgh).hom.app x) ((map h).map ((mapComp f g fg hfg).hom.app x)) = CategoryStruct.comp ((mapComp f gh fgh hfgh').hom.app x) ((mapComp g h gh hgh).hom.app ((map f).obj x)))
(left_unitality :
∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁) (hf : CategoryStruct.comp (CategoryStruct.id b₀) f = f) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp (CategoryStruct.id b₀) f f hf).hom.app x) ((map f).map ((mapId b₀).hom.app x)) = CategoryStruct.id ((map f).obj x))
(right_unitality :
∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁) (hf : CategoryStruct.comp f (CategoryStruct.id b₁) = f) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp f (CategoryStruct.id b₁) f hf).hom.app x) ((mapId b₁).hom.app ((map f).obj x)) = CategoryStruct.id ((map f).obj x))
:
Constructor for pseudofunctors LocallyDiscrete B₀ ⥤ᵖ Cat with value obj b at b, from
functors map f, unit isomorphisms map (𝟙 b) ≅ 𝟭 and composition isomorphisms
map fg ≅ map f ⋙ map g at arbitrary factorizations f ≫ g = fg. Since the coherence
conditions are required at arbitrary factorizations, they are stated componentwise without the
eqToHom relating (f ≫ g) ≫ h and f ≫ g ≫ h.
Instances For
@[simp]
theorem
CategoryTheory.LocallyDiscrete.mkCatPseudofunctor_obj
{B₀ : Type u_1}
[Category.{u_2, u_1} B₀]
{obj : B₀ → Cat}
(map : {b b' : B₀} → (b ⟶ b') → Functor ↑(obj b) ↑(obj b'))
{mapId : (b : B₀) → map (CategoryStruct.id b) ≅ Functor.id ↑(obj b)}
{mapComp :
{b₀ b₁ b₂ : B₀} →
(f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → (fg : b₀ ⟶ b₂) → CategoryStruct.comp f g = fg → (map fg ≅ (map f).comp (map g))}
{associativity :
∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃) (fg : b₀ ⟶ b₂) (gh : b₁ ⟶ b₃) (fgh : b₀ ⟶ b₃)
(hfg : CategoryStruct.comp f g = fg) (hgh : CategoryStruct.comp g h = gh) (hfgh : CategoryStruct.comp fg h = fgh)
(hfgh' : CategoryStruct.comp f gh = fgh) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp fg h fgh hfgh).hom.app x) ((map h).map ((mapComp f g fg hfg).hom.app x)) = CategoryStruct.comp ((mapComp f gh fgh hfgh').hom.app x) ((mapComp g h gh hgh).hom.app ((map f).obj x))}
{left_unitality :
∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁) (hf : CategoryStruct.comp (CategoryStruct.id b₀) f = f) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp (CategoryStruct.id b₀) f f hf).hom.app x) ((map f).map ((mapId b₀).hom.app x)) = CategoryStruct.id ((map f).obj x)}
{right_unitality :
∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁) (hf : CategoryStruct.comp f (CategoryStruct.id b₁) = f) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp f (CategoryStruct.id b₁) f hf).hom.app x) ((mapId b₁).hom.app ((map f).obj x)) = CategoryStruct.id ((map f).obj x)}
(b : LocallyDiscrete B₀)
:
(mkCatPseudofunctor (fun {b b' : B₀} => map) mapId (fun {b₀ b₁ b₂ : B₀} => mapComp) ⋯ ⋯ ⋯).obj b = obj b.as
@[simp]
theorem
CategoryTheory.LocallyDiscrete.mkCatPseudofunctor_map_toFunctor
{B₀ : Type u_1}
[Category.{u_2, u_1} B₀]
{obj : B₀ → Cat}
(map : {b b' : B₀} → (b ⟶ b') → Functor ↑(obj b) ↑(obj b'))
{mapId : (b : B₀) → map (CategoryStruct.id b) ≅ Functor.id ↑(obj b)}
{mapComp :
{b₀ b₁ b₂ : B₀} →
(f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → (fg : b₀ ⟶ b₂) → CategoryStruct.comp f g = fg → (map fg ≅ (map f).comp (map g))}
{associativity :
∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃) (fg : b₀ ⟶ b₂) (gh : b₁ ⟶ b₃) (fgh : b₀ ⟶ b₃)
(hfg : CategoryStruct.comp f g = fg) (hgh : CategoryStruct.comp g h = gh) (hfgh : CategoryStruct.comp fg h = fgh)
(hfgh' : CategoryStruct.comp f gh = fgh) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp fg h fgh hfgh).hom.app x) ((map h).map ((mapComp f g fg hfg).hom.app x)) = CategoryStruct.comp ((mapComp f gh fgh hfgh').hom.app x) ((mapComp g h gh hgh).hom.app ((map f).obj x))}
{left_unitality :
∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁) (hf : CategoryStruct.comp (CategoryStruct.id b₀) f = f) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp (CategoryStruct.id b₀) f f hf).hom.app x) ((map f).map ((mapId b₀).hom.app x)) = CategoryStruct.id ((map f).obj x)}
{right_unitality :
∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁) (hf : CategoryStruct.comp f (CategoryStruct.id b₁) = f) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp f (CategoryStruct.id b₁) f hf).hom.app x) ((mapId b₁).hom.app ((map f).obj x)) = CategoryStruct.id ((map f).obj x)}
{b b' : LocallyDiscrete B₀}
(f : b ⟶ b')
:
((mkCatPseudofunctor (fun {b b' : B₀} => map) mapId (fun {b₀ b₁ b₂ : B₀} => mapComp) ⋯ ⋯ ⋯).map f).toFunctor = map f.as
@[simp]
theorem
CategoryTheory.LocallyDiscrete.mkCatPseudofunctor_mapId_hom_toNatTrans_app
{B₀ : Type u_1}
[Category.{u_2, u_1} B₀]
{obj : B₀ → Cat}
(map : {b b' : B₀} → (b ⟶ b') → Functor ↑(obj b) ↑(obj b'))
{mapId : (b : B₀) → map (CategoryStruct.id b) ≅ Functor.id ↑(obj b)}
{mapComp :
{b₀ b₁ b₂ : B₀} →
(f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → (fg : b₀ ⟶ b₂) → CategoryStruct.comp f g = fg → (map fg ≅ (map f).comp (map g))}
{associativity :
∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃) (fg : b₀ ⟶ b₂) (gh : b₁ ⟶ b₃) (fgh : b₀ ⟶ b₃)
(hfg : CategoryStruct.comp f g = fg) (hgh : CategoryStruct.comp g h = gh) (hfgh : CategoryStruct.comp fg h = fgh)
(hfgh' : CategoryStruct.comp f gh = fgh) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp fg h fgh hfgh).hom.app x) ((map h).map ((mapComp f g fg hfg).hom.app x)) = CategoryStruct.comp ((mapComp f gh fgh hfgh').hom.app x) ((mapComp g h gh hgh).hom.app ((map f).obj x))}
{left_unitality :
∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁) (hf : CategoryStruct.comp (CategoryStruct.id b₀) f = f) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp (CategoryStruct.id b₀) f f hf).hom.app x) ((map f).map ((mapId b₀).hom.app x)) = CategoryStruct.id ((map f).obj x)}
{right_unitality :
∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁) (hf : CategoryStruct.comp f (CategoryStruct.id b₁) = f) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp f (CategoryStruct.id b₁) f hf).hom.app x) ((mapId b₁).hom.app ((map f).obj x)) = CategoryStruct.id ((map f).obj x)}
(b : LocallyDiscrete B₀)
(x : ↑(obj b.as))
:
((mkCatPseudofunctor (fun {b b' : B₀} => map) mapId (fun {b₀ b₁ b₂ : B₀} => mapComp) ⋯ ⋯ ⋯).mapId b).hom.toNatTrans.app
x = (mapId b.as).hom.app x
@[simp]
theorem
CategoryTheory.LocallyDiscrete.mkCatPseudofunctor_mapId_inv_toNatTrans_app
{B₀ : Type u_1}
[Category.{u_2, u_1} B₀]
{obj : B₀ → Cat}
(map : {b b' : B₀} → (b ⟶ b') → Functor ↑(obj b) ↑(obj b'))
{mapId : (b : B₀) → map (CategoryStruct.id b) ≅ Functor.id ↑(obj b)}
{mapComp :
{b₀ b₁ b₂ : B₀} →
(f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → (fg : b₀ ⟶ b₂) → CategoryStruct.comp f g = fg → (map fg ≅ (map f).comp (map g))}
{associativity :
∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃) (fg : b₀ ⟶ b₂) (gh : b₁ ⟶ b₃) (fgh : b₀ ⟶ b₃)
(hfg : CategoryStruct.comp f g = fg) (hgh : CategoryStruct.comp g h = gh) (hfgh : CategoryStruct.comp fg h = fgh)
(hfgh' : CategoryStruct.comp f gh = fgh) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp fg h fgh hfgh).hom.app x) ((map h).map ((mapComp f g fg hfg).hom.app x)) = CategoryStruct.comp ((mapComp f gh fgh hfgh').hom.app x) ((mapComp g h gh hgh).hom.app ((map f).obj x))}
{left_unitality :
∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁) (hf : CategoryStruct.comp (CategoryStruct.id b₀) f = f) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp (CategoryStruct.id b₀) f f hf).hom.app x) ((map f).map ((mapId b₀).hom.app x)) = CategoryStruct.id ((map f).obj x)}
{right_unitality :
∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁) (hf : CategoryStruct.comp f (CategoryStruct.id b₁) = f) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp f (CategoryStruct.id b₁) f hf).hom.app x) ((mapId b₁).hom.app ((map f).obj x)) = CategoryStruct.id ((map f).obj x)}
(b : LocallyDiscrete B₀)
(x : ↑(obj b.as))
:
((mkCatPseudofunctor (fun {b b' : B₀} => map) mapId (fun {b₀ b₁ b₂ : B₀} => mapComp) ⋯ ⋯ ⋯).mapId b).inv.toNatTrans.app
x = (mapId b.as).inv.app x
@[simp]
theorem
CategoryTheory.LocallyDiscrete.mkCatPseudofunctor_mapComp_hom_toNatTrans_app
{B₀ : Type u_1}
[Category.{u_2, u_1} B₀]
{obj : B₀ → Cat}
(map : {b b' : B₀} → (b ⟶ b') → Functor ↑(obj b) ↑(obj b'))
{mapId : (b : B₀) → map (CategoryStruct.id b) ≅ Functor.id ↑(obj b)}
{mapComp :
{b₀ b₁ b₂ : B₀} →
(f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → (fg : b₀ ⟶ b₂) → CategoryStruct.comp f g = fg → (map fg ≅ (map f).comp (map g))}
{associativity :
∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃) (fg : b₀ ⟶ b₂) (gh : b₁ ⟶ b₃) (fgh : b₀ ⟶ b₃)
(hfg : CategoryStruct.comp f g = fg) (hgh : CategoryStruct.comp g h = gh) (hfgh : CategoryStruct.comp fg h = fgh)
(hfgh' : CategoryStruct.comp f gh = fgh) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp fg h fgh hfgh).hom.app x) ((map h).map ((mapComp f g fg hfg).hom.app x)) = CategoryStruct.comp ((mapComp f gh fgh hfgh').hom.app x) ((mapComp g h gh hgh).hom.app ((map f).obj x))}
{left_unitality :
∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁) (hf : CategoryStruct.comp (CategoryStruct.id b₀) f = f) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp (CategoryStruct.id b₀) f f hf).hom.app x) ((map f).map ((mapId b₀).hom.app x)) = CategoryStruct.id ((map f).obj x)}
{right_unitality :
∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁) (hf : CategoryStruct.comp f (CategoryStruct.id b₁) = f) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp f (CategoryStruct.id b₁) f hf).hom.app x) ((mapId b₁).hom.app ((map f).obj x)) = CategoryStruct.id ((map f).obj x)}
{b₀ b₁ b₂ : LocallyDiscrete B₀}
(f : b₀ ⟶ b₁)
(g : b₁ ⟶ b₂)
(x : ↑(obj b₀.as))
:
((mkCatPseudofunctor (fun {b b' : B₀} => map) mapId (fun {b₀ b₁ b₂ : B₀} => mapComp) ⋯ ⋯ ⋯).mapComp f
g).hom.toNatTrans.app
x = (mapComp f.as g.as (CategoryStruct.comp f.as g.as) ⋯).hom.app x
@[simp]
theorem
CategoryTheory.LocallyDiscrete.mkCatPseudofunctor_mapComp_inv_toNatTrans_app
{B₀ : Type u_1}
[Category.{u_2, u_1} B₀]
{obj : B₀ → Cat}
(map : {b b' : B₀} → (b ⟶ b') → Functor ↑(obj b) ↑(obj b'))
{mapId : (b : B₀) → map (CategoryStruct.id b) ≅ Functor.id ↑(obj b)}
{mapComp :
{b₀ b₁ b₂ : B₀} →
(f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → (fg : b₀ ⟶ b₂) → CategoryStruct.comp f g = fg → (map fg ≅ (map f).comp (map g))}
{associativity :
∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃) (fg : b₀ ⟶ b₂) (gh : b₁ ⟶ b₃) (fgh : b₀ ⟶ b₃)
(hfg : CategoryStruct.comp f g = fg) (hgh : CategoryStruct.comp g h = gh) (hfgh : CategoryStruct.comp fg h = fgh)
(hfgh' : CategoryStruct.comp f gh = fgh) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp fg h fgh hfgh).hom.app x) ((map h).map ((mapComp f g fg hfg).hom.app x)) = CategoryStruct.comp ((mapComp f gh fgh hfgh').hom.app x) ((mapComp g h gh hgh).hom.app ((map f).obj x))}
{left_unitality :
∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁) (hf : CategoryStruct.comp (CategoryStruct.id b₀) f = f) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp (CategoryStruct.id b₀) f f hf).hom.app x) ((map f).map ((mapId b₀).hom.app x)) = CategoryStruct.id ((map f).obj x)}
{right_unitality :
∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁) (hf : CategoryStruct.comp f (CategoryStruct.id b₁) = f) (x : ↑(obj b₀)),
CategoryStruct.comp ((mapComp f (CategoryStruct.id b₁) f hf).hom.app x) ((mapId b₁).hom.app ((map f).obj x)) = CategoryStruct.id ((map f).obj x)}
{b₀ b₁ b₂ : LocallyDiscrete B₀}
(f : b₀ ⟶ b₁)
(g : b₁ ⟶ b₂)
(x : ↑(obj b₀.as))
:
((mkCatPseudofunctor (fun {b b' : B₀} => map) mapId (fun {b₀ b₁ b₂ : B₀} => mapComp) ⋯ ⋯ ⋯).mapComp f
g).inv.toNatTrans.app
x = (mapComp f.as g.as (CategoryStruct.comp f.as g.as) ⋯).inv.app x