feat(category_theory/closed): golf definition and proofs (#5623)

Using the new mates framework, simplify the definition of `pre` and shorten proofs about it. 
To be more specific,

- `pre` is now explicitly a natural transformation, rather than indexed morphisms with a naturality property
- The new definition of `pre` means things like `pre_map` which I complained about before are easier to prove, and `pre_post_comm` is automatic
- There are now more lemmas relating `pre` to `coev`, `ev` and `uncurry`: `uncurry_pre` in particular was a hole in the API.
- `internal_hom` has a shorter construction. In particular I changed the type to `Cᵒᵖ ⥤ C ⥤ C`, which I think is better since the usual external hom functor is given as `Cᵒᵖ ⥤ C ⥤ Type*`, so this is consistent with that. 

In a subsequent PR I'll do the same for `exp_comparison`, but that's a bigger change with improved API so they're separate for now.

src/category_theory/closed/cartesian.lean

@@ -9,6 +9,7 @@ import category_theory.limits.preserves.shapes.binary_products
 import category_theory.closed.monoidal
 import category_theory.monoidal.of_has_finite_products
 import category_theory.adjunction
+import category_theory.adjunction.mates
 import category_theory.epi_mono
 
 /-!
@@ -97,6 +98,9 @@ closed.is_adj.adj.counit
 def coev : 𝟭 C ⟶ prod.functor.obj A ⋙ exp A :=
 closed.is_adj.adj.unit
 
+@[simp] lemma exp_adjunction_counit : (exp.adjunction A).counit = ev A := rfl
+@[simp] lemma exp_adjunction_unit : (exp.adjunction A).unit = coev A := rfl
+
 @[simp, reassoc]
 lemma ev_naturality {X Y : C} (f : X ⟶ Y) :
   limits.prod.map (𝟙 A) ((exp A).map f) ≫ (ev A).app Y = (ev A).app X ≫ f :=
@@ -219,41 +223,40 @@ section pre
 variables {B}
 
 /-- Pre-compose an internal hom with an external hom. -/
-def pre (X : C) (f : B ⟶ A) [exponentiable B] : (A⟹X) ⟶ B⟹X :=
-curry (limits.prod.map f (𝟙 _) ≫ (ev A).app X)
+def pre (f : B ⟶ A) [exponentiable B] : exp A ⟶ exp B :=
+transfer_nat_trans_self (exp.adjunction _) (exp.adjunction _) (prod.functor.map f)
 
-lemma pre_id (A X : C) [exponentiable A] : pre X (𝟙 A) = 𝟙 (A⟹X) :=
-by { rw [pre, prod.map_id_id, id_comp, ← uncurry_id_eq_ev], simp }
+lemma prod_map_pre_app_comp_ev (f : B ⟶ A) [exponentiable B] (X : C) :
+  limits.prod.map (𝟙 B) ((pre f).app X) ≫ (ev B).app X =
+    limits.prod.map f (𝟙 (A ⟹ X)) ≫ (ev A).app X :=
+transfer_nat_trans_self_counit _ _ (prod.functor.map f) X
 
--- There's probably a better proof of this somehow
-/-- Precomposition is contrafunctorial. -/
-lemma pre_map [exponentiable B] {D : C} [exponentiable D] (f : A ⟶ B) (g : B ⟶ D) :
-  pre X (f ≫ g) = pre X g ≫ pre X f :=
+lemma uncurry_pre (f : B ⟶ A) [exponentiable B] (X : C) :
+  uncurry ((pre f).app X) = limits.prod.map f (𝟙 _) ≫ (ev A).app X :=
 begin
-  rw [pre, curry_eq_iff, pre, uncurry_natural_left, pre, uncurry_curry, prod.map_swap_assoc,
-      prod.map_comp_id, assoc, ← uncurry_id_eq_ev, ← uncurry_id_eq_ev, ← uncurry_natural_left,
-      curry_natural_right, comp_id, uncurry_natural_right, uncurry_curry],
+  rw [uncurry_eq, prod_map_pre_app_comp_ev]
 end
 
-end pre
+lemma coev_app_comp_pre_app (f : B ⟶ A) [exponentiable B] :
+  (coev A).app X ≫ (pre f).app (A ⨯ X) = (coev B).app X ≫ (exp B).map (limits.prod.map f (𝟙 _)) :=
+unit_transfer_nat_trans_self _ _ (prod.functor.map f) X
 
-lemma pre_post_comm [cartesian_closed C] {A B : C} {X Y : Cᵒᵖ} (f : A ⟶ B) (g : X ⟶ Y) :
-  pre A g.unop ≫ (exp Y.unop).map f = (exp X.unop).map f ≫ pre B g.unop :=
-begin
-  rw [pre, pre, ← curry_natural_left, eq_curry_iff, uncurry_natural_right, uncurry_curry,
-      prod.map_swap_assoc, ev_naturality, assoc],
-end
+@[simp]
+lemma pre_id (A : C) [exponentiable A] : pre (𝟙 A) = 𝟙 _ :=
+by simp [pre]
+
+@[simp]
+lemma pre_map {A₁ A₂ A₃ : C} [exponentiable A₁] [exponentiable A₂] [exponentiable A₃]
+  (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) :
+  pre (f ≫ g) = pre g ≫ pre f :=
+by rw [pre, pre, pre, transfer_nat_trans_self_comp, prod.functor.map_comp]
+
+end pre
 
 /-- The internal hom functor given by the cartesian closed structure. -/
-def internal_hom [cartesian_closed C] : C ⥤ Cᵒᵖ ⥤ C :=
-{ obj := λ X,
-  { obj := λ Y, Y.unop ⟹ X,
-    map := λ Y Y' f, pre _ f.unop,
-    map_id' := λ Y, pre_id _ _,
-    map_comp' := λ Y Y' Y'' f g, pre_map _ _ },
-  map := λ A B f, { app := λ X, (exp X.unop).map f, naturality' := λ X Y g, pre_post_comm _ _ },
-  map_id' := λ X, by { ext, apply functor.map_id },
-  map_comp' := λ X Y Z f g, by { ext, apply functor.map_comp } }
+def internal_hom [cartesian_closed C] : Cᵒᵖ ⥤ C ⥤ C :=
+{ obj := λ X, exp X.unop,
+  map := λ X Y f, pre f.unop }
 
 /-- If an initial object `I` exists in a CCC, then `A ⨯ I ≅ I`. -/
 @[simps]
@@ -385,16 +388,14 @@ curry (inv (prod_comparison F A _) ≫ F.map ((ev _).app _))
 
 /-- The exponential comparison map is natural in its left argument. -/
 lemma exp_comparison_natural_left (A A' B : C) (f : A' ⟶ A) :
-  exp_comparison F A B ≫ pre (F.obj B) (F.map f) = F.map (pre B f) ≫ exp_comparison F A' B :=
+  exp_comparison F A B ≫ (pre (F.map f)).app (F.obj B) =
+    F.map ((pre f).app B) ≫ exp_comparison F A' B :=
 begin
-  rw [exp_comparison, exp_comparison, ← curry_natural_left, eq_curry_iff, uncurry_natural_left,
-       pre, uncurry_curry, prod.map_swap_assoc, curry_eq, prod.map_id_comp, assoc, ev_naturality],
+  rw [exp_comparison, exp_comparison, ←curry_natural_left, eq_curry_iff, uncurry_natural_left,
+    uncurry_pre, prod.map_swap_assoc, curry_eq, prod.map_id_comp, assoc, ev_naturality],
   dsimp only [prod.functor_obj_obj],
   rw [ev_coev_assoc, ← F.map_id, ← F.map_id, ← prod_comparison_inv_natural_assoc,
-      ← prod_comparison_inv_natural_assoc, ← F.map_comp, ← F.map_comp, pre, curry_eq,
-      prod.map_id_comp, assoc, ev_naturality],
-  dsimp only [prod.functor_obj_obj],
-  rw ev_coev_assoc,
+      ← prod_comparison_inv_natural_assoc, ← F.map_comp, ← F.map_comp, prod_map_pre_app_comp_ev],
 end
 
 /-- The exponential comparison map is natural in its right argument. -/