refactor(category_theory/products): tweak PR after merge

Author: digama0

analysis/nnreal.lean

@@ -11,7 +11,7 @@ noncomputable theory
 open lattice filter
 variables {α : Type*}
 
-definition nnreal := {r : ℝ // 0 ≤ r}
+def nnreal := {r : ℝ // 0 ≤ r}
 local notation ` ℝ≥0 ` := nnreal
 
 namespace nnreal

category_theory/functor.lean

@@ -5,7 +5,7 @@ Authors: Tim Baumann, Stephen Morgan, Scott Morrison
 
 Defines a functor between categories.
 
-(As it is a 'bundled' object rather than the `is_functorial` typeclass parametrised 
+(As it is a 'bundled' object rather than the `is_functorial` typeclass parametrised
 by the underlying function on objects, the name is capitalised.)
 
 Introduces notations
@@ -16,14 +16,14 @@ Introduces notations
 import .category
 
 namespace category_theory
- 
+
 universes u₁ v₁ u₂ v₂ u₃ v₃
 
 /--
-`functor C D` represents a functor between categories `C` and `D`. 
+`functor C D` represents a functor between categories `C` and `D`.
 
 To apply a functor `F` to an object use `F X`, and to a morphism use `F.map f`.
- 
+
 The axiom `map_id_lemma` expresses preservation of identities, and
 `map_comp_lemma` expresses functoriality.
 -/
@@ -37,7 +37,7 @@ 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 -- 
+infixr ` ↝ `:70 := functor       -- type as \lea --
 
 namespace functor
 
@@ -57,7 +57,7 @@ variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C]
 include 𝒞
 
 /-- `functor.id C` is the identity functor on a category `C`. -/
-protected definition id : C ↝ C := 
+protected def id : C ↝ C :=
 { obj      := λ X, X,
   map      := λ _ _ f, f,
   map_id   := begin /- `obviously'` says: -/ intros, refl end,
@@ -76,7 +76,7 @@ include 𝒞 𝒟 ℰ
 /--
 `F ⋙ G` is the composition of a functor `F` and a functor `G` (`F` first, then `G`).
 -/
-definition comp (F : C ↝ D) (G : D ↝ E) : C ↝ E := 
+def comp (F : C ↝ D) (G : D ↝ E) : C ↝ E :=
 { obj      := λ X, G.obj (F.obj X),
   map      := λ _ _ f, G.map (F.map f),
   map_id   := begin /- `obviously'` says: -/ intros, simp end,

category_theory/functor_category.lean

@@ -11,41 +11,41 @@ universes u₁ v₁ u₂ v₂ u₃ v₃
 open nat_trans
 
 /--
-`functor_category C D` gives the category structure on functor and natural transformations between categories `C` and `D`.
+`functor.category C D` gives the category structure on functor and natural transformations between categories `C` and `D`.
 
 Notice that if `C` and `D` are both small categories at the same universe level, this is another small category at that level.
 However if `C` and `D` are both large categories at the same universe level, this is a small category at the next higher level.
 -/
-instance functor_category (C : Type u₁) [category.{u₁ v₁} C] (D : Type u₂) [category.{u₂ v₂} D] : category.{(max u₁ v₁ u₂ v₂) (max u₁ v₂)} (C ↝ D) := 
+instance functor.category (C : Type u₁) [category.{u₁ v₁} C] (D : Type u₂) [category.{u₂ v₂} D] : category.{(max u₁ v₁ u₂ v₂) (max u₁ v₂)} (C ↝ D) :=
 { Hom     := λ F G, F ⟹ G,
   id      := λ F, nat_trans.id F,
   comp    := λ _ _ _ α β, α ⊟ β,
   id_comp := begin /- `obviously'` says: -/ intros, ext, intros, dsimp, simp end,
   comp_id := begin /- `obviously'` says: -/ intros, ext, intros, dsimp, simp end,
   assoc   := begin /- `obviously'` says: -/ intros, ext, intros, simp end }
 
-namespace functor_category
+namespace functor.category
 
 section
 variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
 include 𝒞 𝒟
 
-@[simp,ematch] lemma id_app (F : C ↝ D) (X : C) : (𝟙 F : F ⟹ F) X = 𝟙 (F X) := rfl
-@[simp,ematch] lemma comp_app {F G H : C ↝ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) : ((α ≫ β) : F ⟹ H) X = (α : F ⟹ G) X ≫ (β : G ⟹ H) X := rfl
+@[simp, ematch] lemma id_app (F : C ↝ D) (X : C) : (𝟙 F : F ⟹ F) X = 𝟙 (F X) := rfl
+@[simp, ematch] lemma comp_app {F G H : C ↝ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) : ((α ≫ β) : F ⟹ H) X = (α : F ⟹ G) X ≫ (β : G ⟹ H) X := rfl
 end
 
 namespace nat_trans
 -- This section gives two lemmas about natural transformations between functors into functor categories, spelling them out in components.
 
 variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] {D : Type u₂} [𝒟 : category.{u₂ v₂} D] {E : Type u₃} [ℰ : category.{u₃ v₃} E]
-include 𝒞 𝒟 ℰ 
+include 𝒞 𝒟 ℰ
 
 @[ematch] lemma app_naturality {F G : C ↝ (D ↝ E)} (T : F ⟹ G) (X : C) {Y Z : D} (f : Y ⟶ Z) : ((F X).map f) ≫ ((T X) Z) = ((T X) Y) ≫ ((G X).map f) := (T X).naturality f
 
 @[ematch] lemma naturality_app {F G : C ↝ (D ↝ E)} (T : F ⟹ G) (Z : D) {X Y : C} (f : X ⟶ Y) : ((F.map f) Z) ≫ ((T Y) Z) = ((T X) Z) ≫ ((G.map f) Z) := congr_fun (congr_arg app (T.naturality f)) Z
 
 end nat_trans
 
-end functor_category
+end functor.category
 
 end category_theory

category_theory/natural_transformation.lean

@@ -47,7 +47,7 @@ instance {F G : C ↝ D} : has_coe_to_fun (F ⟹ G) :=
 @[simp] lemma coe_def {F G : C ↝ D} (α : F ⟹ G) (X : C) : α X = α.app X := rfl
 
 /-- `nat_trans.id F` is the identity natural transformation on a functor `F`. -/
-protected definition id (F : C ↝ D) : F ⟹ F := 
+protected def id (F : C ↝ D) : F ⟹ F :=
 { app        := λ X, 𝟙 (F X),
   naturality := begin /- `obviously'` says: -/ intros, dsimp, simp end }
 
@@ -69,11 +69,11 @@ begin
 end
 
 /-- `vcomp α β` is the vertical compositions of natural transformations. -/
-definition vcomp (α : F ⟹ G) (β : G ⟹ H) : F ⟹ H := 
+def vcomp (α : F ⟹ G) (β : G ⟹ H) : F ⟹ H :=
 { app        := λ X, (α X) ≫ (β X),
   naturality := begin /- `obviously'` says: -/ intros, simp, rw [←assoc_lemma, naturality_lemma, assoc_lemma, ←naturality_lemma], end }
 
-notation α `⊟` β:80 := vcomp α β    
+notation α `⊟` β:80 := vcomp α β
 
 @[simp] lemma vcomp_app (α : F ⟹ G) (β : G ⟹ H) (X : C) : (α ⊟ β) X = (α X) ≫ (β X) := rfl
 @[ematch] lemma vcomp_assoc (α : F ⟹ G) (β : G ⟹ H) (γ : H ⟹ I) : (α ⊟ β) ⊟ γ = (α ⊟ (β ⊟ γ)) := begin ext, intros, dsimp, rw [assoc] end
@@ -83,9 +83,9 @@ variables {E : Type u₃} [ℰ : category.{u₃ v₃} E]
 include ℰ
 
 /-- `hcomp α β` is the horizontal composition of natural transformations. -/
-definition hcomp {F G : C ↝ D} {H I : D ↝ E} (α : F ⟹ G) (β : H ⟹ I) : (F ⋙ H) ⟹ (G ⋙ I) :=
-{ app        := λ X : C, (β (F X)) ≫ (I.map (α X)), 
-  naturality := begin 
+def hcomp {F G : C ↝ D} {H I : D ↝ E} (α : F ⟹ G) (β : H ⟹ I) : (F ⋙ H) ⟹ (G ⋙ I) :=
+{ app        := λ X : C, (β (F X)) ≫ (I.map (α X)),
+  naturality := begin
                   /- `obviously'` says: -/
                   intros,
                   dsimp,
@@ -101,7 +101,7 @@ notation α `◫` β:80 := hcomp α β
 
 -- Note that we don't yet prove a `hcomp_assoc` lemma here: even stating it is painful, because we need to use associativity of functor composition
 
-@[ematch] lemma exchange {F G H : C ↝ D} {I J K : D ↝ E} (α : F ⟹ G) (β : G ⟹ H) (γ : I ⟹ J) (δ : J ⟹ K) : ((α ⊟ β) ◫ (γ ⊟ δ)) = ((α ◫ γ) ⊟ (β ◫ δ)) := 
+@[ematch] lemma exchange {F G H : C ↝ D} {I J K : D ↝ E} (α : F ⟹ G) (β : G ⟹ H) (γ : I ⟹ J) (δ : J ⟹ K) : ((α ⊟ β) ◫ (γ ⊟ δ)) = ((α ◫ γ) ⊟ (β ◫ δ)) :=
 begin
   -- `obviously'` says:
   ext,

category_theory/products.lean

@@ -11,96 +11,92 @@ section
 variables (C : Type u₁) [category.{u₁ v₁} C] (D : Type u₂) [category.{u₂ v₂} D]
 
 /--
-`product_category C D` gives the cartesian product of two categories.
+`prod.category C D` gives the cartesian product of two categories.
 -/
-instance product_category : category.{(max u₁ u₂) (max v₁ v₂)} (C × D) := 
+instance prod.category : category.{(max u₁ u₂) (max v₁ v₂)} (C × D) :=
 { Hom     := λ X Y, ((X.1) ⟶ (Y.1)) × ((X.2) ⟶ (Y.2)),
   id      := λ X, ⟨ 𝟙 (X.1), 𝟙 (X.2) ⟩,
   comp    := λ _ _ _ f g, (f.1 ≫ g.1, f.2 ≫ g.2),
   id_comp := begin  /- `obviously'` says: -/ intros, cases X, cases Y, cases f, dsimp at *, simp end,
   comp_id := begin /- `obviously'` says: -/ intros, cases X, cases Y, cases f, dsimp at *, simp end,
-  assoc   := begin /- `obviously'` says: -/ intros, cases W, cases X, cases Y, cases Z, cases f, cases g, cases h, dsimp at *, simp end }     
-end 
+  assoc   := begin /- `obviously'` says: -/ intros, cases W, cases X, cases Y, cases Z, cases f, cases g, cases h, dsimp at *, simp end }
+end
 
-namespace product_category
+namespace prod.category
 
-section -- rfl lemmas for product_category
+section -- rfl lemmas for prod.category
 variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
 include 𝒞 𝒟
 
-@[simp,ematch] lemma id (X : C) (Y : D) : 𝟙 (X, Y) = (𝟙 X, 𝟙 Y) := rfl
-@[simp,ematch] lemma comp {P Q R : C} {S T U : D} (f : (P, S) ⟶ (Q, T)) (g : (Q, T) ⟶ (R, U)) : f ≫ g = (f.1 ≫ g.1, f.2 ≫ g.2) := rfl
+@[simp, ematch] lemma id (X : C) (Y : D) : 𝟙 (X, Y) = (𝟙 X, 𝟙 Y) := rfl
+@[simp, ematch] lemma comp {P Q R : C} {S T U : D} (f : (P, S) ⟶ (Q, T)) (g : (Q, T) ⟶ (R, U)) : f ≫ g = (f.1 ≫ g.1, f.2 ≫ g.2) := rfl
 end
 
-section 
+section
 variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C] (D : Type u₁) [𝒟 : category.{u₁ v₁} D]
 include 𝒞 𝒟
 
-/-- 
-`product_category.uniform C D` is an additional instance specialised so both factors have the same universe levels. This helps typeclass resolution.
+/--
+`prod.category.uniform C D` is an additional instance specialised so both factors have the same universe levels. This helps typeclass resolution.
 -/
-instance uniform : category.{u₁ v₁} (C × D) := category_theory.product_category C D
+instance uniform : category (C × D) := prod.category C D
 end
 
 -- Next we define the natural functors into and out of product categories. For now this doesn't address the universal properties.
 
-/-- `right_injection_at C Z` is the functor `X ↦ (X, Z)`. -/
-definition right_injection_at (C : Type u₁) [category.{u₁ v₁} C] {D : Type u₁} [category.{u₁ v₁} D] (Z : D) : C ↝ (C × D) := 
+/-- `inl C Z` is the functor `X ↦ (X, Z)`. -/
+def inl (C : Type u₁) [category.{u₁ v₁} C] {D : Type u₁} [category.{u₁ v₁} D] (Z : D) : C ↝ (C × D) :=
 { obj      := λ X, (X, Z),
   map      := λ X Y f, (f, 𝟙 Z),
   map_id   := begin /- `obviously'` says: -/ intros, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, dsimp, simp end }
 
-/-- `left_injection_at Z D` is the functor `X ↦ (Z, X)`. -/
-definition left_injection_at {C : Type u₁} [category.{u₁ v₁} C] (Z : C) (D : Type u₁) [category.{u₁ v₁} D] : D ↝ (C × D) := 
+/-- `inr D Z` is the functor `X ↦ (Z, X)`. -/
+def inr {C : Type u₁} [category.{u₁ v₁} C] (D : Type u₁) [category.{u₁ v₁} D] (Z : C) : D ↝ (C × D) :=
 { obj      := λ X, (Z, X),
   map      := λ X Y f, (𝟙 Z, f),
   map_id   := begin /- `obviously'` says: -/ intros, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, dsimp, simp end }
 
-/-- `left_projection` is the functor `(X, Y) ↦ X`. -/
-definition left_projection (C : Type u₁) [category.{u₁ v₁} C] (Z : C) (D : Type u₁) [category.{u₁ v₁} D] : (C × D) ↝ C := 
+/-- `fst` is the functor `(X, Y) ↦ X`. -/
+def fst (C : Type u₁) [category.{u₁ v₁} C] (Z : C) (D : Type u₁) [category.{u₁ v₁} D] : (C × D) ↝ C :=
 { obj      := λ X, X.1,
   map      := λ X Y f, f.1,
   map_id   := begin /- `obviously'` says: -/ intros, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, refl end }
 
-/-- `right_projection` is the functor `(X, Y) ↦ Y`. -/
-definition right_projection (C : Type u₁) [category.{u₁ v₁} C] (Z : C) (D : Type u₁) [category.{u₁ v₁} D] : (C × D) ↝ D := 
+/-- `snd` is the functor `(X, Y) ↦ Y`. -/
+def snd (C : Type u₁) [category.{u₁ v₁} C] (Z : C) (D : Type u₁) [category.{u₁ v₁} D] : (C × D) ↝ D :=
 { obj      := λ X, X.2,
   map      := λ X Y f, f.2,
   map_id   := begin /- `obviously'` says: -/ intros, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, refl end }
 
-end product_category
+end prod.category
 
 variables {A : Type u₁} [𝒜 : category.{u₁ v₁} A] {B : Type u₂} [ℬ : category.{u₂ v₂} B] {C : Type u₃} [𝒞 : category.{u₃ v₃} C] {D : Type u₄} [𝒟 : category.{u₄ v₄} D]
 include 𝒜 ℬ 𝒞 𝒟
 
 namespace functor
 /-- The cartesion product of two functors. -/
-definition product (F : A ↝ B) (G : C ↝ D) : (A × C) ↝ (B × D) :=
+def prod (F : A ↝ B) (G : C ↝ D) : (A × C) ↝ (B × D) :=
 { obj := λ X, (F X.1, G X.2),
   map := λ _ _ f, (F.map f.1, G.map f.2),
   map_id   := begin /- `obviously'` says: -/ intros, cases X, dsimp, rw map_id_lemma, rw map_id_lemma end,
   map_comp := begin /- `obviously'` says: -/ intros, cases Z, cases Y, cases X, cases f, cases g, dsimp at *, rw map_comp_lemma, rw map_comp_lemma end }
 
-notation F `×` G := product F G
-
-@[simp,ematch] lemma product_obj   (F : A ↝ B) (G : C ↝ D) (a : A) (c : C) : (F × G) (a, c) = (F a, G c) := rfl
-@[simp,ematch] lemma product_map (F : A ↝ B) (G : C ↝ D) {a a' : A} {c c' : C} (f : (a, c) ⟶ (a', c')) : (F × G).map f = (F.map f.1, G.map f.2) := rfl
+@[simp, ematch] lemma prod_obj (F : A ↝ B) (G : C ↝ D) (a : A) (c : C) : F.prod G (a, c) = (F a, G c) := rfl
+@[simp, ematch] lemma prod_map (F : A ↝ B) (G : C ↝ D) {a a' : A} {c c' : C} (f : (a, c) ⟶ (a', c')) : (F.prod G).map f = (F.map f.1, G.map f.2) := rfl
 end functor
 
 namespace nat_trans
 
 /-- The cartesian product of two natural transformations. -/
-definition product {F G : A ↝ B} {H I : C ↝ D} (α : F ⟹ G) (β : H ⟹ I) : (F × H) ⟹ (G × I) :=
+def prod {F G : A ↝ B} {H I : C ↝ D} (α : F ⟹ G) (β : H ⟹ I) : F.prod H ⟹ G.prod I :=
 { app        := λ X, (α X.1, β X.2),
   naturality := begin /- `obviously'` says: -/ intros, cases f, cases Y, cases X, dsimp at *, simp, split, rw naturality_lemma, rw naturality_lemma end }
 
-notation α `×` β := product α β
-
-@[simp,ematch] lemma product_app {F G : A ↝ B} {H I : C ↝ D} (α : F ⟹ G) (β : H ⟹ I) (a : A) (c : C) : (α × β) (a, c) = (α a, β c) := rfl
+@[simp, ematch] lemma prod_app {F G : A ↝ B} {H I : C ↝ D} (α : F ⟹ G) (β : H ⟹ I) (a : A) (c : C) : α.prod β (a, c) = (α a, β c) := rfl
 end nat_trans
 
 end category_theory

order/bounds.lean

@@ -15,12 +15,12 @@ section preorder
 
 variables [preorder α] [preorder β] {f : α → β}
 
-definition upper_bounds (s : set α) : set α := { x | ∀a ∈ s, a ≤ x }
-definition lower_bounds (s : set α) : set α := { x | ∀a ∈ s, x ≤ a }
-definition is_least (s : set α) (a : α) : Prop := a ∈ s ∧ a ∈ lower_bounds s
-definition is_greatest (s : set α) (a : α) : Prop := a ∈ s ∧ a ∈ upper_bounds s
-definition is_lub (s : set α) : α → Prop := is_least (upper_bounds s)
-definition is_glb (s : set α) : α → Prop := is_greatest (lower_bounds s)
+def upper_bounds (s : set α) : set α := { x | ∀a ∈ s, a ≤ x }
+def lower_bounds (s : set α) : set α := { x | ∀a ∈ s, x ≤ a }
+def is_least (s : set α) (a : α) : Prop := a ∈ s ∧ a ∈ lower_bounds s
+def is_greatest (s : set α) (a : α) : Prop := a ∈ s ∧ a ∈ upper_bounds s
+def is_lub (s : set α) : α → Prop := is_least (upper_bounds s)
+def is_glb (s : set α) : α → Prop := is_greatest (lower_bounds s)
 
 lemma mem_upper_bounds_image (Hf : monotone f) (Ha : a ∈ upper_bounds s) :
   f a ∈ upper_bounds (f '' s) :=

tactic/basic.lean

@@ -46,7 +46,7 @@ end environment
 
 namespace tactic
 
-meta definition mk_local (n : name) : expr :=
+meta def mk_local (n : name) : expr :=
 expr.local_const n n binder_info.default (expr.const n [])
 
 meta def exact_dec_trivial : tactic unit := `[exact dec_trivial]