Make opposite irreducible, take 2

rwbarton · rwbarton · commit 89379bc6faed · 2019-01-25T08:21:52.000-05:00
diff --git a/src/category_theory/limits/cones.lean b/src/category_theory/limits/cones.lean
@@ -32,14 +32,14 @@ An object representing this functor is a limit of `F`.
 -/
 def cones : Cᵒᵖ ⥤ Type v := (const Jᵒᵖ ⋙ op_inv J C) ⋙ (yoneda.obj F)
 
-lemma cones_obj (X : C) : F.cones.obj X = ((const J).obj X ⟹ F) := rfl
+lemma cones_obj (X : C) : F.cones.obj (op X) = ((const J).obj X ⟹ F) := rfl
 
 /--
 `F.cocones` is the functor assigning to an object `X` the type of
 natural transformations from `F` to the constant functor with value `X`.
 An object corepresenting this functor is a colimit of `F`.
 -/
-def cocones : C ⥤ Type v := (const J) ⋙ (coyoneda.obj F)
+def cocones : C ⥤ Type v := const J ⋙ coyoneda.obj (op F)
 
 lemma cocones_obj (X : C) : F.cocones.obj X = (F ⟹ (const J).obj X) := rfl
 
@@ -53,7 +53,7 @@ def cones : (J ⥤ C) ⥤ (Cᵒᵖ ⥤ Type v) :=
   map := λ F G f, whisker_left _ (yoneda.map f) }
 
 def cocones : (J ⥤ C)ᵒᵖ ⥤ (C ⥤ Type v) :=
-{ obj := functor.cocones,
+{ obj := λ F, functor.cocones (unop F),
   map := λ F G f, whisker_left _ (coyoneda.map f) }
 
 variables {J C}
@@ -62,8 +62,8 @@ variables {J C}
 @[simp] lemma cones_map  {F G : J ⥤ C} {f : F ⟶ G} :
 (cones J C).map f = (whisker_left _ (yoneda.map f)) := rfl
 
-@[simp] lemma cocones_obj (F : J ⥤ C) : (cocones J C).obj F = F.cocones := rfl
-@[simp] lemma cocones_map  {F G : J ⥤ C} {f : F ⟶ G} :
+@[simp] lemma cocones_obj (F : (J ⥤ C)ᵒᵖ) : (cocones J C).obj F = (unop F).cocones := rfl
+@[simp] lemma cocones_map  {F G : (J ⥤ C)ᵒᵖ} {f : F ⟶ G} :
 (cocones J C).map f = (whisker_left _ (coyoneda.map f)) := rfl
 
 end
@@ -111,7 +111,7 @@ namespace cone
 /-- A map to the vertex of a cone induces a cone by composition. -/
 @[simp] def extend (c : cone F) {X : C} (f : X ⟶ c.X) : cone F :=
 { X := X,
-  π := c.extensions.app X f }
+  π := c.extensions.app (op X) f }
 
 def postcompose {G : J ⥤ C} (α : F ⟹ G) (c : cone F) : cone G :=
 { X := c.X,
@@ -126,7 +126,7 @@ def whisker {K : Type v} [small_category K] (E : K ⥤ J) (c : cone F) : cone (E
 end cone
 
 namespace cocone
-@[simp] def extensions (c : cocone F) : coyoneda.obj c.X ⟶ F.cocones :=
+@[simp] def extensions (c : cocone F) : coyoneda.obj (op c.X) ⟶ F.cocones :=
 { app := λ X f, c.ι ≫ ((const J).map f),
   naturality' := by intros X Y f; ext g j; dsimp; rw ←assoc; refl }
 
diff --git a/src/category_theory/limits/limits.lean b/src/category_theory/limits/limits.lean
@@ -90,7 +90,7 @@ def hom_iso (h : is_limit t) (W : C) : (W ⟶ t.X) ≅ ((const J).obj W ⟹ F) :
 /-- The limit of `F` represents the functor taking `W` to
   the set of cones on `F` with vertex `W`. -/
 def nat_iso (h : is_limit t) : yoneda.obj t.X ≅ F.cones :=
-nat_iso.of_components (is_limit.hom_iso h) (by tidy)
+nat_iso.of_components (λ W, is_limit.hom_iso h (unop W)) (by tidy)
 
 def hom_iso' (h : is_limit t) (W : C) :
   (W ⟶ t.X) ≅ { p : Π j, W ⟶ F.obj j // ∀ {j j'} (f : j ⟶ j'), p j ≫ F.map f = p j' } :=
@@ -191,7 +191,7 @@ def hom_iso (h : is_colimit t) (W : C) : (t.X ⟶ W) ≅ (F ⟹ (const J).obj W)
 
 /-- The colimit of `F` represents the functor taking `W` to
   the set of cocones on `F` with vertex `W`. -/
-def nat_iso (h : is_colimit t) : coyoneda.obj t.X ≅ F.cocones :=
+def nat_iso (h : is_colimit t) : coyoneda.obj (op t.X) ≅ F.cocones :=
 nat_iso.of_components (is_colimit.hom_iso h) (by intros; ext; dsimp; rw ←assoc; refl)
 
 def hom_iso' (h : is_colimit t) (W : C) :
@@ -290,7 +290,7 @@ by erw is_limit.fac
   (w : ∀ j, f ≫ limit.π F j = f' ≫ limit.π F j) : f = f' :=
 (limit.is_limit F).hom_ext w
 
-def limit.hom_iso (F : J ⥤ C) [has_limit F] (W : C) : (W ⟶ limit F) ≅ (F.cones.obj W) :=
+def limit.hom_iso (F : J ⥤ C) [has_limit F] (W : C) : (W ⟶ limit F) ≅ (F.cones.obj (op W)) :=
 (limit.is_limit F).hom_iso W
 
 @[simp] lemma limit.hom_iso_hom (F : J ⥤ C) [has_limit F] {W : C} (f : W ⟶ limit F):
@@ -416,7 +416,8 @@ begin
 end
 
 def lim_yoneda : lim ⋙ yoneda ≅ category_theory.cones J C :=
-nat_iso.of_components (λ F, nat_iso.of_components (limit.hom_iso F) (by tidy)) (by tidy)
+nat_iso.of_components (λ F, nat_iso.of_components (λ W, limit.hom_iso F (unop W)) (by tidy))
+  (by tidy)
 
 end lim_functor
 
@@ -634,7 +635,7 @@ begin
 end
 
 def colim_coyoneda : colim.op ⋙ coyoneda ≅ category_theory.cocones J C :=
-nat_iso.of_components (λ F, nat_iso.of_components (colimit.hom_iso F)
+nat_iso.of_components (λ F, nat_iso.of_components (colimit.hom_iso (unop F))
   (by {tidy, dsimp [functor.cocones], rw category.assoc }))
   (by {tidy, rw [← category.assoc,← category.assoc], tidy })
 
diff --git a/src/category_theory/opposites.lean b/src/category_theory/opposites.lean
@@ -9,23 +9,66 @@ namespace category_theory
 
 universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
 
-def op (C : Type u₁) : Type u₁ := C
+def opposite (C : Type u₁) : Type u₁ := C
 
 -- Use a high right binding power (like that of postfix ⁻¹) so that, for example,
 -- `presheaf Cᵒᵖ` parses as `presheaf (Cᵒᵖ)` and not `(presheaf C)ᵒᵖ`.
-notation C `ᵒᵖ`:std.prec.max_plus := op C
+notation C `ᵒᵖ`:std.prec.max_plus := opposite C
 
-variables {C : Type u₁} [𝒞 : category.{v₁} C]
+variables {C : Type u₁}
+
+def op (X : C) : Cᵒᵖ := X
+def unop (X : Cᵒᵖ) : C := X
+
+attribute [irreducible] opposite
+
+@[simp] lemma unop_op (X : C) : unop (op X) = X := rfl
+@[simp] lemma op_unop (X : Cᵒᵖ) : op (unop X) = X := rfl
+
+section has_hom
+
+variables [𝒞 : has_hom.{v₁} C]
+include 𝒞
+
+instance has_hom.opposite : has_hom Cᵒᵖ :=
+{ hom := λ X Y, unop Y ⟶ unop X }
+
+def has_hom.hom.op {X Y : C} (f : X ⟶ Y) : op Y ⟶ op X := f
+def has_hom.hom.unop {X Y : Cᵒᵖ} (f : X ⟶ Y) : unop Y ⟶ unop X := f
+
+attribute [irreducible] has_hom.opposite
+
+lemma has_hom.hom.op_inj {X Y : C} :
+  function.injective (has_hom.hom.op : (X ⟶ Y) → (op Y ⟶ op X)) :=
+λ _ _ H, congr_arg has_hom.hom.unop H
+
+lemma has_hom.hom.unop_inj {X Y : Cᵒᵖ} :
+  function.injective (has_hom.hom.unop : (X ⟶ Y) → (unop Y ⟶ unop X)) :=
+λ _ _ H, congr_arg has_hom.hom.op H
+
+@[simp] lemma has_hom.hom.unop_op {X Y : C} {f : X ⟶ Y} : f.op.unop = f := rfl
+@[simp] lemma has_hom.hom.op_unop {X Y : Cᵒᵖ} {f : X ⟶ Y} : f.unop.op = f := rfl
+
+end has_hom
+
+variables [𝒞 : category.{v₁} C]
 include 𝒞
 
-instance opposite : category.{v₁} Cᵒᵖ :=
-{ hom  := λ X Y : C, Y ⟶ X,
-  comp := λ _ _ _ f g, g ≫ f,
-  id   := λ X, 𝟙 X }
+instance category.opposite : category.{v₁} Cᵒᵖ :=
+{ comp := λ _ _ _ f g, (g.unop ≫ f.unop).op,
+  id   := λ X, (𝟙 (unop X)).op }
+
+@[simp] lemma op_comp {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} :
+  (f ≫ g).op = g.op ≫ f.op := rfl
+@[simp] lemma op_id {X : C} : (𝟙 X).op = 𝟙 (op X) := rfl
+
+@[simp] lemma unop_comp {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} :
+  (f ≫ g).unop = g.unop ≫ f.unop := rfl
+@[simp] lemma unop_id {X : Cᵒᵖ} : (𝟙 X).unop = 𝟙 (unop X) := rfl
 
 def op_op : (Cᵒᵖ)ᵒᵖ ⥤ C :=
-{ obj := λ X, X,
-  map := λ X Y f, f }
+{ obj := λ X, unop (unop X),
+  map := λ X Y f, f.unop.unop }
 
 -- TODO this is an equivalence
 
@@ -39,78 +82,64 @@ include 𝒟
 variables {C D}
 
 protected definition op (F : C ⥤ D) : Cᵒᵖ ⥤ Dᵒᵖ :=
-{ obj       := λ X, F.obj X,
-  map       := λ X Y f, F.map f,
-  map_id'   := begin /- `obviously'` says: -/ intros, erw [map_id], refl, end,
-  map_comp' := begin /- `obviously'` says: -/ intros, erw [map_comp], refl end }
+{ obj := λ X, op (F.obj (unop X)),
+  map := λ X Y f, (F.map f.unop).op }
 
-@[simp] lemma op_obj (F : C ⥤ D) (X : C) : (F.op).obj X = F.obj X := rfl
-@[simp] lemma op_map (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) : (F.op).map f = F.map f := rfl
+@[simp] lemma op_obj (F : C ⥤ D) (X : Cᵒᵖ) : (F.op).obj X = op (F.obj (unop X)) := rfl
+@[simp] lemma op_map (F : C ⥤ D) {X Y : Cᵒᵖ} (f : X ⟶ Y) : (F.op).map f = (F.map f.unop).op := rfl
 
 protected definition unop (F : Cᵒᵖ ⥤ Dᵒᵖ) : C ⥤ D :=
-{ obj       := λ X, F.obj X,
-  map       := λ X Y f, F.map f,
-  map_id'   := F.map_id,
-  map_comp' := by intros; apply F.map_comp }
+{ obj := λ X, unop (F.obj (op X)),
+  map := λ X Y f, (F.map f.op).unop }
 
-@[simp] lemma unop_obj (F : Cᵒᵖ ⥤ Dᵒᵖ) (X : C) : (F.unop).obj X = F.obj X := rfl
-@[simp] lemma unop_map (F : Cᵒᵖ ⥤ Dᵒᵖ) {X Y : C} (f : X ⟶ Y) : (F.unop).map f = F.map f := rfl
+@[simp] lemma unop_obj (F : Cᵒᵖ ⥤ Dᵒᵖ) (X : C) : (F.unop).obj X = unop (F.obj (op X)) := rfl
+@[simp] lemma unop_map (F : Cᵒᵖ ⥤ Dᵒᵖ) {X Y : C} (f : X ⟶ Y) : (F.unop).map f = (F.map f.op).unop := rfl
 
 variables (C D)
 
 definition op_hom : (C ⥤ D)ᵒᵖ ⥤ (Cᵒᵖ ⥤ Dᵒᵖ) :=
-{ obj := λ F, F.op,
+{ obj := λ F, (unop F).op,
   map := λ F G α,
-  { app := λ X, α.app X,
-    naturality' := λ X Y f, eq.symm (α.naturality f) } }
+  { app := λ X, (α.unop.app (unop X)).op,
+    naturality' := λ X Y f, has_hom.hom.unop_inj $ eq.symm (α.unop.naturality f.unop) } }
 
-@[simp] lemma op_hom.obj (F : (C ⥤ D)ᵒᵖ) : (op_hom C D).obj F = F.op := rfl
-@[simp] lemma op_hom.map_app {F G : (C ⥤ D)ᵒᵖ} (α : F ⟶ G) (X : C) :
-  ((op_hom C D).map α).app X = α.app X := rfl
+@[simp] lemma op_hom.obj (F : (C ⥤ D)ᵒᵖ) : (op_hom C D).obj F = (unop F).op := rfl
+@[simp] lemma op_hom.map_app {F G : (C ⥤ D)ᵒᵖ} (α : F ⟶ G) (X : Cᵒᵖ) :
+  ((op_hom C D).map α).app X = (α.unop.app (unop X)).op := rfl
 
 definition op_inv : (Cᵒᵖ ⥤ Dᵒᵖ) ⥤ (C ⥤ D)ᵒᵖ :=
-{ obj := λ F : Cᵒᵖ ⥤ Dᵒᵖ, F.unop,
-  map := λ F G α,
-  { app := λ X : C, α.app X,
-    naturality' := λ X Y f, eq.symm (α.naturality f) } }
+{ obj := λ F, op F.unop,
+  map := λ F G α, has_hom.hom.op
+  { app := λ X, (α.app (op X)).unop,
+    naturality' := λ X Y f, has_hom.hom.op_inj $ eq.symm (α.naturality f.op) } }
 
-@[simp] lemma op_inv.obj (F : Cᵒᵖ ⥤ Dᵒᵖ) : (op_inv C D).obj F = F.unop := rfl
+@[simp] lemma op_inv.obj (F : Cᵒᵖ ⥤ Dᵒᵖ) : (op_inv C D).obj F = op F.unop := rfl
 @[simp] lemma op_inv.map_app {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ⟶ G) (X : C) :
-  ((op_inv C D).map α).app X = α.app X := rfl
+  (((op_inv C D).map α).unop).app X = (α.app (op X)).unop := rfl
 
 -- TODO show these form an equivalence
 
 instance {F : C ⥤ D} [full F] : full F.op :=
-{ preimage := λ X Y f, F.preimage f }
+{ preimage := λ X Y f, (F.preimage f.unop).op }
 
 instance {F : C ⥤ D} [faithful F] : faithful F.op :=
-{ injectivity' := λ X Y f g h, by simpa using injectivity F h }
+{ injectivity' := λ X Y f g h,
+    has_hom.hom.unop_inj $ by simpa using injectivity F (has_hom.hom.op_inj h) }
 
 end
 
-namespace category
-variables {C} {D : Type u₂} [𝒟 : category.{v₂} D]
-include 𝒟
-
-@[simp] lemma op_id_app (F : (C ⥤ D)ᵒᵖ) (X : C) : (𝟙 F : F ⟹ F).app X = 𝟙 (F.obj X) := rfl
-@[simp] lemma op_comp_app {F G H : (C ⥤ D)ᵒᵖ} (α : F ⟶ G) (β : G ⟶ H) (X : C) :
-  ((α ≫ β) : H ⟹ F).app X = (β : H ⟹ G).app X ≫ (α : G ⟹ F).app X := rfl
-end category
-
 section
 
 variable (C)
 
 /-- `functor.hom` is the hom-pairing, sending (X,Y) to X → Y, contravariant in X and covariant in Y. -/
 definition hom : Cᵒᵖ × C ⥤ Type v₁ :=
-{ obj       := λ p, @has_hom.hom C _ p.1 p.2,
-  map       := λ X Y f, λ h, f.1 ≫ h ≫ f.2,
-  map_id'   := by intros; ext; dsimp [category_theory.opposite]; simp,
-  map_comp' := by intros; ext; dsimp [category_theory.opposite]; simp }
+{ obj       := λ p, unop p.1 ⟶ p.2,
+  map       := λ X Y f, λ h, f.1.unop ≫ h ≫ f.2 }
 
-@[simp] lemma hom_obj (X : Cᵒᵖ × C) : (functor.hom C).obj X = @has_hom.hom C _ X.1 X.2 := rfl
+@[simp] lemma hom_obj (X : Cᵒᵖ × C) : (functor.hom C).obj X = (unop X.1 ⟶ X.2) := rfl
 @[simp] lemma hom_pairing_map {X Y : Cᵒᵖ × C} (f : X ⟶ Y) :
-  (functor.hom C).map f = λ h, f.1 ≫ h ≫ f.2 := rfl
+  (functor.hom C).map f = λ h, f.1.unop ≫ h ≫ f.2 := rfl
 
 end
 
diff --git a/src/category_theory/yoneda.lean b/src/category_theory/yoneda.lean
