Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(category_theory/currying): bifunctor version of whiskering_right #15504

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat(category_theory/currying): bifunctor version of whiskering_right #15504

Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
924bcd2
feat(category_theory/products/basic): equivalence ((A ⥤ B) × (A ⥤ C))…
antoinelab01 Jul 17, 2022
fda6962
add docstrings
antoinelab01 Jul 17, 2022
3369cd7
separate into different definitions
antoinelab01 Jul 18, 2022
df07734
Merge remote-tracking branch 'origin/master' into functor_prod_functo…
antoinelab01 Jul 18, 2022
b65d9a5
feat(category_theory/currying): bifunctor version of whiskering_right
antoinelab01 Jul 19, 2022
945e8fc
Update src/category_theory/functor/currying.lean
antoinelab01 Jul 19, 2022
2ef9a9e
move B first
antoinelab01 Jul 19, 2022
3bff2a6
Merge remote-tracking branch 'origin/master' into biwhiskering
antoinelab01 Aug 17, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 15 additions & 4 deletions src/category_theory/functor/currying.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,11 +15,12 @@ and verify that they provide an equivalence of categories
-/
namespace category_theory

universes v₁ v₂ v₃ u₁ u₂ u₃
universes v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄

variables {C : Type u₁} [category.{v₁} C]
{D : Type u₂} [category.{v₂} D]
{E : Type u₃} [category.{v₃} E]
variables {B : Type u₁} [category.{v₁} B]
{C : Type u₂} [category.{v₂} C]
{D : Type u₃} [category.{v₃} D]
{E : Type u₄} [category.{v₄} E]

/--
The uncurrying functor, taking a functor `C ⥤ (D ⥤ E)` and producing a functor `(C × D) ⥤ E`.
Expand Down Expand Up @@ -99,4 +100,14 @@ swapping the factors followed by the uncurrying of `F`. -/
def uncurry_obj_flip (F : C ⥤ D ⥤ E) : uncurry.obj F.flip ≅ prod.swap _ _ ⋙ uncurry.obj F :=
nat_iso.of_components (λ p, iso.refl _) (by tidy)

variables (B C D E)

/--
A version of `category_theory.whiskering_right` for bifunctors, obtained by uncurrying,
applying `whiskering_right` and currying back
-/
@[simps] def whiskering_right₂ : (C ⥤ D ⥤ E) ⥤ ((B ⥤ C) ⥤ (B ⥤ D) ⥤ (B ⥤ E)) :=
uncurry ⋙ (whiskering_right _ _ _) ⋙
((whiskering_left _ _ _).obj (prod_functor_to_functor_prod _ _ _)) ⋙ curry

end category_theory