feat(category_theory): basic definitions

category_theory/category.lean

@@ -14,7 +14,7 @@ local notation f ` ⊚ `:80 g:80 := category.comp g f    -- type as \oo
 ```
 -/
 
-import tactic.make_lemma
+import tactic.restate_axiom
 import tactic.interactive
 
 namespace category_theory
@@ -43,9 +43,9 @@ infixr ` ≫ `:80 := category.comp -- type as \gg
 infixr ` ⟶ `:10 := category.Hom -- type as \h
 
 -- make_lemma is a command that creates a lemma from a structure field, discarding all auto_param wrappers from the type.
-make_lemma category.id_comp
-make_lemma category.comp_id
-make_lemma category.assoc
+restate_axiom category.id_comp
+restate_axiom category.comp_id
+restate_axiom category.assoc
 -- We tag some lemmas with the attribute `@[ematch]`, for later automation. (I'd be happy to change this to e.g. `@[search]`.)
 attribute [simp,ematch] category.id_comp_lemma category.comp_id_lemma category.assoc_lemma 
 

category_theory/functor.lean

@@ -25,8 +25,8 @@ structure functor (C : Type u₁) [category.{u₁ v₁} C] (D : Type u₂) [cate
 (map_id   : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously)
 (map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = (map f) ≫ (map g) . obviously)
 
-make_lemma functor.map_id
-make_lemma functor.map_comp
+restate_axiom functor.map_id
+restate_axiom functor.map_comp
 attribute [simp,ematch] functor.map_id_lemma functor.map_comp_lemma
 
 infixr ` ↝ `:70 := functor       -- type as \lea -- 
@@ -60,8 +60,8 @@ instance has_one : has_one (C ↝ C) :=
 
 variable {C}
 
-@[simp] lemma identity.on_objects (X : C) : (identity C) X = X := rfl
-@[simp] lemma identity.on_morphisms {X Y : C} (f : X ⟶ Y) : (identity C).map f = f := rfl
+@[simp] lemma identity_to_has_one : (identity C) = 1 := rfl
+
 @[simp] lemma has_one.on_objects (X : C) : (1 : C ↝ C) X = X := rfl
 @[simp] lemma has_one.on_morphisms {X Y : C} (f : X ⟶ Y) : (1 : C ↝ C).map f = f := rfl
 

category_theory/natural_transformation.lean

@@ -21,39 +21,40 @@ universes u₁ v₁ u₂ v₂ u₃ v₃
 variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
 include 𝒞 𝒟
 
-structure natural_transformation (F G : C ↝ D) : Type (max u₁ v₂) :=
-(components : Π X : C, (F X) ⟶ (G X))
-(naturality : ∀ {X Y : C} (f : X ⟶ Y), (F.map f) ≫ (components Y) = (components X) ≫ (G.map f) . obviously)
+structure nat_trans (F G : C ↝ D) : Type (max u₁ v₂) :=
+(app : Π X : C, (F X) ⟶ (G X))
+(naturality : ∀ {X Y : C} (f : X ⟶ Y), (F.map f) ≫ (app Y) = (app X) ≫ (G.map f) . obviously)
 
-make_lemma natural_transformation.naturality
-attribute [ematch] natural_transformation.naturality_lemma
+restate_axiom nat_trans.naturality
+attribute [ematch] nat_trans.naturality_lemma
 
-infixr ` ⟹ `:50  := natural_transformation             -- type as \==> or ⟹
+infixr ` ⟹ `:50  := nat_trans             -- type as \==> or ⟹
 
-namespace natural_transformation
+namespace nat_trans
 
 instance {F G : C ↝ D} : has_coe_to_fun (F ⟹ G) :=
 { F   := λ α, Π X : C, (F X) ⟶ (G X),
-  coe := λ α, α.components }
+  coe := λ α, α.app }
 
-@[simp] lemma coe_def {F G : C ↝ D} (α : F ⟹ G) (X : C) : α X = α.components X := rfl
+@[simp] lemma coe_def {F G : C ↝ D} (α : F ⟹ G) (X : C) : α X = α.app X := rfl
 
-end natural_transformation
+end nat_trans
 
 namespace functor
 definition identity (F : C ↝ D) : F ⟹ F := 
-{ components := λ X, 𝟙 (F X),
+{ app        := λ X, 𝟙 (F X),
   naturality := begin /- `obviously'` says: -/ intros, dsimp, simp end }
 
 instance has_one (F : C ↝ D) : has_one (F ⟹ F) := 
 { one := identity F }
 
-@[simp] lemma identity.components (F : C ↝ D) (X : C) : (identity F) X = 𝟙 (F X) := rfl
-@[simp] lemma has_one.components (F : C ↝ D) (X : C) : (1 : F ⟹ F) X = 𝟙 (F X) := rfl
+@[simp] lemma identity_to_has_one (F : C ↝ D) : identity F = 1 := rfl
+
+@[simp] lemma has_one.app (F : C ↝ D) (X : C) : (1 : F ⟹ F) X = 𝟙 (F X) := rfl
 
 end functor
 
-namespace natural_transformation
+namespace nat_trans
 
 open category
 open category_theory.functor
@@ -62,7 +63,7 @@ section
 variables {F G H : C ↝ D}
 
 -- We'll want to be able to prove that two natural transformations are equal if they are componentwise equal.
-@[extensionality] lemma componentwise_equal (α β : F ⟹ G) (w : ∀ X : C, α X = β X) : α = β :=
+@[extensionality] lemma ext (α β : F ⟹ G) (w : ∀ X : C, α X = β X) : α = β :=
 begin
   induction α with α_components α_naturality,
   induction β with β_components β_naturality,
@@ -71,7 +72,7 @@ begin
 end
 
 definition vcomp (α : F ⟹ G) (β : G ⟹ H) : F ⟹ H := 
-{ components := λ X, (α X) ≫ (β X),
+{ app        := λ X, (α X) ≫ (β X),
   naturality := begin /- `obviously'` says: -/ intros, simp, rw [←assoc_lemma, naturality_lemma, assoc_lemma, ←naturality_lemma], end }
 
 notation α `⊟` β:80 := vcomp α β    
@@ -84,7 +85,7 @@ variable [ℰ : category.{u₃ v₃} E]
 include ℰ
 
 definition hcomp {F G : C ↝ D} {H I : D ↝ E} (α : F ⟹ G) (β : H ⟹ I) : (F ⋙ H) ⟹ (G ⋙ I) :=
-{ components := λ X : C, (β (F X)) ≫ (I.map (α X)), 
+{ app        := λ X : C, (β (F X)) ≫ (I.map (α X)), 
   naturality := begin 
                   /- `obviously'` says: -/
                   intros,
@@ -102,13 +103,13 @@ notation α `◫` β:80 := hcomp α β
 @[ematch] lemma exchange {F G H : C ↝ D} {I J K : D ↝ E} (α : F ⟹ G) (β : G ⟹ H) (γ : I ⟹ J) (δ : J ⟹ K) : ((α ⊟ β) ◫ (γ ⊟ δ)) = ((α ◫ γ) ⊟ (β ◫ δ)) := 
 begin
   -- `obviously'` says:
-  apply componentwise_equal,
+  ext,
   intros,
   dsimp,
   simp,
   -- again, this isn't actually what obviously says, but it achieves the same effect.
   conv { to_lhs, congr, skip, rw [←assoc_lemma, ←naturality_lemma, assoc_lemma] }
 end
 
-end natural_transformation
+end nat_trans
 end category_theory

tactic/make_lemma.lean → tactic/restate_axiom.lean

@@ -9,12 +9,11 @@ import data.buffer.parser
 open lean.parser tactic interactive parser
 
 @[user_attribute] meta def field_lemma_attr : user_attribute :=
-{ name := `field_lemma, descr := "This definition was automatically generated from a structure field by `make_lemma`." }
-
+{ name := `field_lemma, descr := "This definition was automatically generated from a structure field by `restate_axiom`." }
 
 /- Make lemma takes a structure field, and makes a new, definitionally simplified copy of it, appending `_lemma` to the name.
    The main application is to provide clean versions of structure fields that have been tagged with an auto_param. -/
-meta def make_lemma (d : declaration) (new_name : name) : tactic unit :=
+meta def restate_axiom (d : declaration) (new_name : name) : tactic unit :=
 do (levels, type, value, reducibility, trusted) ← pure (match d.to_definition with
   | declaration.defn name levels type value reducibility trusted :=
     (levels, type, value, reducibility, trusted)
@@ -31,13 +30,13 @@ match n.components.reverse with
 | nil          := undefined
 end
 
-@[user_command] meta def make_lemma_cmd (meta_info : decl_meta_info)
-  (_ : parse $ tk "make_lemma") : lean.parser unit :=
+@[user_command] meta def restate_axiom_cmd (meta_info : decl_meta_info)
+  (_ : parse $ tk "restate_axiom") : lean.parser unit :=
 do from_lemma ← ident,
    from_lemma_fully_qualified ← resolve_constant from_lemma,
   d ← get_decl from_lemma_fully_qualified <|>
     fail ("declaration " ++ to_string from_lemma ++ " not found"),
   do {
-    make_lemma d (name_lemma from_lemma_fully_qualified)
+    restate_axiom d (name_lemma from_lemma_fully_qualified)
   }.