Skip to content

Commit

Permalink
chore(category_theory/limits): move product isomorphisms (#5057)
Browse files Browse the repository at this point in the history 
This PR moves some constructions and lemmas from `monoidal/of_has_finite_products` (back) to `limits/shapes/binary_products`. 

This reverts some changes made in 18246ac#diff-95871ea16bec862dfc4359f812b624a7a98e87b8c31c034e8a6e792332edb646. In particular, the purpose of that PR was to minimise imports in particular relating to `finite_limits`, but moving these particular definitions back doesn't make the imports any worse in that sense - other than that `binary_products` now imports `terminal` which I think doesn't make the import graph much worse.  On the other hand, these definitions are useful outside of the context of monoidal categories so I think they do genuinely belong in `limits/`.

I also changed some proofs from `tidy` to `simp` or a term-mode proof, and removed a `simp` attribute from a lemma which was already provable by `simp`.
  • Loading branch information
@b-mehta
b-mehta committed Nov 23, 2020
1 parent a71901f commit e8c8ce9
Show file tree
Hide file tree
Showing 2 changed files with 167 additions and 166 deletions.
158 changes: 158 additions & 0 deletions src/category_theory/limits/shapes/binary_products.lean
View file
Expand Up @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Bhavik Mehta
-/
import category_theory.limits.limits
import category_theory.limits.shapes.terminal
import category_theory.discrete_category
import category_theory.epi_mono

Expand Down Expand Up @@ -531,6 +532,158 @@ lemma has_binary_coproducts_of_has_colimit_pair [Π {X Y : C}, has_colimit (pair
has_binary_coproducts C :=
{ has_colimit := λ F, has_colimit_of_iso (diagram_iso_pair F) }

section
variables {C}

/-- The braiding isomorphism which swaps a binary product. -/
@[simps] def prod.braiding (P Q : C) [has_binary_product P Q] [has_binary_product Q P] :
P ⨯ Q ≅ Q ⨯ P :=
{ hom := prod.lift prod.snd prod.fst,
inv := prod.lift prod.snd prod.fst }

/-- The braiding isomorphism can be passed through a map by swapping the order. -/
@[reassoc] lemma braid_natural [has_binary_products C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) :
prod.map f g ≫ (prod.braiding _ _).hom = (prod.braiding _ _).hom ≫ prod.map g f :=
by simp

@[reassoc] lemma prod.symmetry' (P Q : C) [has_binary_product P Q] [has_binary_product Q P] :
prod.lift prod.snd prod.fst ≫ prod.lift prod.snd prod.fst = 𝟙 (P ⨯ Q) :=
(prod.braiding _ _).hom_inv_id

/-- The braiding isomorphism is symmetric. -/
@[reassoc] lemma prod.symmetry (P Q : C) [has_binary_product P Q] [has_binary_product Q P] :
(prod.braiding P Q).hom ≫ (prod.braiding Q P).hom = 𝟙 _ :=
(prod.braiding _ _).hom_inv_id

/-- The associator isomorphism for binary products. -/
@[simps] def prod.associator [has_binary_products C] (P Q R : C) :
(P ⨯ Q) ⨯ R ≅ P ⨯ (Q ⨯ R) :=
{ hom :=
prod.lift
(prod.fst ≫ prod.fst)
(prod.lift (prod.fst ≫ prod.snd) prod.snd),
inv :=
prod.lift
(prod.lift prod.fst (prod.snd ≫ prod.fst))
(prod.snd ≫ prod.snd) }

@[reassoc]
lemma prod.pentagon [has_binary_products C] (W X Y Z : C) :
prod.map ((prod.associator W X Y).hom) (𝟙 Z) ≫
(prod.associator W (X ⨯ Y) Z).hom ≫ prod.map (𝟙 W) ((prod.associator X Y Z).hom) =
(prod.associator (W ⨯ X) Y Z).hom ≫ (prod.associator W X (Y ⨯ Z)).hom :=
by simp

@[reassoc]
lemma prod.associator_naturality [has_binary_products C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C}
(f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
prod.map (prod.map f₁ f₂) f₃ ≫ (prod.associator Y₁ Y₂ Y₃).hom =
(prod.associator X₁ X₂ X₃).hom ≫ prod.map f₁ (prod.map f₂ f₃) :=
by simp

variables [has_terminal C]

/-- The left unitor isomorphism for binary products with the terminal object. -/
@[simps] def prod.left_unitor (P : C) [has_binary_product (⊤_ C) P] :
⊤_ C ⨯ P ≅ P :=
{ hom := prod.snd,
inv := prod.lift (terminal.from P) (𝟙 _) }

/-- The right unitor isomorphism for binary products with the terminal object. -/
@[simps] def prod.right_unitor (P : C) [has_binary_product P (⊤_ C)] :
P ⨯ ⊤_ C ≅ P :=
{ hom := prod.fst,
inv := prod.lift (𝟙 _) (terminal.from P) }

@[reassoc]
lemma prod.left_unitor_hom_naturality [has_binary_products C] (f : X ⟶ Y) :
prod.map (𝟙 _) f ≫ (prod.left_unitor Y).hom = (prod.left_unitor X).hom ≫ f :=
prod.map_snd _ _

@[reassoc]
lemma prod.left_unitor_inv_naturality [has_binary_products C] (f : X ⟶ Y) :
(prod.left_unitor X).inv ≫ prod.map (𝟙 _) f = f ≫ (prod.left_unitor Y).inv :=
by rw [iso.inv_comp_eq, ← category.assoc, iso.eq_comp_inv, prod.left_unitor_hom_naturality]

@[reassoc]
lemma prod.right_unitor_hom_naturality [has_binary_products C] (f : X ⟶ Y) :
prod.map f (𝟙 _) ≫ (prod.right_unitor Y).hom = (prod.right_unitor X).hom ≫ f :=
prod.map_fst _ _

@[reassoc]
lemma prod_right_unitor_inv_naturality [has_binary_products C] (f : X ⟶ Y) :
(prod.right_unitor X).inv ≫ prod.map f (𝟙 _) = f ≫ (prod.right_unitor Y).inv :=
by rw [iso.inv_comp_eq, ← category.assoc, iso.eq_comp_inv, prod.right_unitor_hom_naturality]

lemma prod.triangle [has_binary_products C] (X Y : C) :
(prod.associator X (⊤_ C) Y).hom ≫ prod.map (𝟙 X) ((prod.left_unitor Y).hom) =
prod.map ((prod.right_unitor X).hom) (𝟙 Y) :=
by tidy

end

section

variables {C} [has_binary_coproducts C]

/-- The braiding isomorphism which swaps a binary coproduct. -/
@[simps] def coprod.braiding (P Q : C) : P ⨿ Q ≅ Q ⨿ P :=
{ hom := coprod.desc coprod.inr coprod.inl,
inv := coprod.desc coprod.inr coprod.inl }

@[reassoc] lemma coprod.symmetry' (P Q : C) :
coprod.desc coprod.inr coprod.inl ≫ coprod.desc coprod.inr coprod.inl = 𝟙 (P ⨿ Q) :=
(coprod.braiding _ _).hom_inv_id

/-- The braiding isomorphism is symmetric. -/
lemma coprod.symmetry (P Q : C) :
(coprod.braiding P Q).hom ≫ (coprod.braiding Q P).hom = 𝟙 _ :=
coprod.symmetry' _ _

/-- The associator isomorphism for binary coproducts. -/
@[simps] def coprod.associator
(P Q R : C) : (P ⨿ Q) ⨿ R ≅ P ⨿ (Q ⨿ R) :=
{ hom :=
coprod.desc
(coprod.desc coprod.inl (coprod.inl ≫ coprod.inr))
(coprod.inr ≫ coprod.inr),
inv :=
coprod.desc
(coprod.inl ≫ coprod.inl)
(coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) }

lemma coprod.pentagon (W X Y Z : C) :
coprod.map ((coprod.associator W X Y).hom) (𝟙 Z) ≫
(coprod.associator W (X ⨿ Y) Z).hom ≫ coprod.map (𝟙 W) ((coprod.associator X Y Z).hom) =
(coprod.associator (W ⨿ X) Y Z).hom ≫ (coprod.associator W X (Y ⨿ Z)).hom :=
by simp

lemma coprod.associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
coprod.map (coprod.map f₁ f₂) f₃ ≫ (coprod.associator Y₁ Y₂ Y₃).hom =
(coprod.associator X₁ X₂ X₃).hom ≫ coprod.map f₁ (coprod.map f₂ f₃) :=
by simp

variables [has_initial C]

/-- The left unitor isomorphism for binary coproducts with the initial object. -/
@[simps] def coprod.left_unitor
(P : C) : ⊥_ C ⨿ P ≅ P :=
{ hom := coprod.desc (initial.to P) (𝟙 _),
inv := coprod.inr }

/-- The right unitor isomorphism for binary coproducts with the initial object. -/
@[simps] def coprod.right_unitor
(P : C) : P ⨿ ⊥_ C ≅ P :=
{ hom := coprod.desc (𝟙 _) (initial.to P),
inv := coprod.inl }

lemma coprod.triangle (X Y : C) :
(coprod.associator X (⊥_ C) Y).hom ≫ coprod.map (𝟙 X) ((coprod.left_unitor Y).hom) =
coprod.map ((coprod.right_unitor X).hom) (𝟙 Y) :=
by tidy

end

section prod_functor
variables {C} [has_binary_products C]

Expand All @@ -541,6 +694,11 @@ def prod.functor : C ⥤ C ⥤ C :=
{ obj := λ X, { obj := λ Y, X ⨯ Y, map := λ Y Z, prod.map (𝟙 X) },
map := λ Y Z f, { app := λ T, prod.map f (𝟙 T) }}

/-- The product functor can be decomposed. -/
def prod.functor_left_comp (X Y : C) :
prod.functor.obj (X ⨯ Y) ≅ prod.functor.obj Y ⋙ prod.functor.obj X :=
nat_iso.of_components (prod.associator _ _) (by tidy)

end prod_functor

section prod_comparison
Expand Down
175 changes: 9 additions & 166 deletions src/category_theory/monoidal/of_has_finite_products.lean
View file
Expand Up @@ -36,163 +36,6 @@ namespace category_theory

variables (C : Type u) [category.{v} C] {X Y : C}

namespace limits

section
variables {C} [has_binary_products C]

/-- The braiding isomorphism which swaps a binary product. -/
@[simps] def prod.braiding (P Q : C) : P ⨯ Q ≅ Q ⨯ P :=
{ hom := prod.lift prod.snd prod.fst,
inv := prod.lift prod.snd prod.fst }

/-- The braiding isomorphism can be passed through a map by swapping the order. -/
@[reassoc] lemma braid_natural {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) :
prod.map f g ≫ (prod.braiding _ _).hom = (prod.braiding _ _).hom ≫ prod.map g f :=
by tidy

@[simp, reassoc] lemma prod.symmetry' (P Q : C) :
prod.lift prod.snd prod.fst ≫ prod.lift prod.snd prod.fst = 𝟙 (P ⨯ Q) :=
by tidy

/-- The braiding isomorphism is symmetric. -/
@[reassoc] lemma prod.symmetry (P Q : C) :
(prod.braiding P Q).hom ≫ (prod.braiding Q P).hom = 𝟙 _ :=
by simp

/-- The associator isomorphism for binary products. -/
@[simps] def prod.associator
(P Q R : C) : (P ⨯ Q) ⨯ R ≅ P ⨯ (Q ⨯ R) :=
{ hom :=
prod.lift
(prod.fst ≫ prod.fst)
(prod.lift (prod.fst ≫ prod.snd) prod.snd),
inv :=
prod.lift
(prod.lift prod.fst (prod.snd ≫ prod.fst))
(prod.snd ≫ prod.snd) }

/-- The product functor can be decomposed. -/
def prod.functor_left_comp (X Y : C) :
prod.functor.obj (X ⨯ Y) ≅ prod.functor.obj Y ⋙ prod.functor.obj X :=
nat_iso.of_components (prod.associator _ _) (by tidy)

@[reassoc]
lemma prod.pentagon (W X Y Z : C) :
prod.map ((prod.associator W X Y).hom) (𝟙 Z) ≫
(prod.associator W (X ⨯ Y) Z).hom ≫ prod.map (𝟙 W) ((prod.associator X Y Z).hom) =
(prod.associator (W ⨯ X) Y Z).hom ≫ (prod.associator W X (Y ⨯ Z)).hom :=
by tidy

@[reassoc]
lemma prod.associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
prod.map (prod.map f₁ f₂) f₃ ≫ (prod.associator Y₁ Y₂ Y₃).hom =
(prod.associator X₁ X₂ X₃).hom ≫ prod.map f₁ (prod.map f₂ f₃) :=
by tidy

variables [has_terminal C]

/-- The left unitor isomorphism for binary products with the terminal object. -/
@[simps] def prod.left_unitor
(P : C) : ⊤_ C ⨯ P ≅ P :=
{ hom := prod.snd,
inv := prod.lift (terminal.from P) (𝟙 _) }

/-- The right unitor isomorphism for binary products with the terminal object. -/
@[simps] def prod.right_unitor
(P : C) : P ⨯ ⊤_ C ≅ P :=
{ hom := prod.fst,
inv := prod.lift (𝟙 _) (terminal.from P) }

@[reassoc]
lemma prod.left_unitor_hom_naturality (f : X ⟶ Y):
prod.map (𝟙 _) f ≫ (prod.left_unitor Y).hom = (prod.left_unitor X).hom ≫ f :=
prod.map_snd _ _

@[reassoc]
lemma prod.left_unitor_inv_naturality (f : X ⟶ Y):
(prod.left_unitor X).inv ≫ prod.map (𝟙 _) f = f ≫ (prod.left_unitor Y).inv :=
by rw [iso.inv_comp_eq, ← category.assoc, iso.eq_comp_inv, prod.left_unitor_hom_naturality]

@[reassoc]
lemma prod.right_unitor_hom_naturality (f : X ⟶ Y):
prod.map f (𝟙 _) ≫ (prod.right_unitor Y).hom = (prod.right_unitor X).hom ≫ f :=
prod.map_fst _ _

@[reassoc]
lemma prod_right_unitor_inv_naturality (f : X ⟶ Y):
(prod.right_unitor X).inv ≫ prod.map f (𝟙 _) = f ≫ (prod.right_unitor Y).inv :=
by rw [iso.inv_comp_eq, ← category.assoc, iso.eq_comp_inv, prod.right_unitor_hom_naturality]

lemma prod.triangle (X Y : C) :
(prod.associator X (⊤_ C) Y).hom ≫ prod.map (𝟙 X) ((prod.left_unitor Y).hom) =
prod.map ((prod.right_unitor X).hom) (𝟙 Y) :=
by tidy

end

section
variables {C} [has_binary_coproducts C]

/-- The braiding isomorphism which swaps a binary coproduct. -/
@[simps] def coprod.braiding (P Q : C) : P ⨿ Q ≅ Q ⨿ P :=
{ hom := coprod.desc coprod.inr coprod.inl,
inv := coprod.desc coprod.inr coprod.inl }

@[simp] lemma coprod.symmetry' (P Q : C) :
coprod.desc coprod.inr coprod.inl ≫ coprod.desc coprod.inr coprod.inl = 𝟙 (P ⨿ Q) :=
by tidy

/-- The braiding isomorphism is symmetric. -/
lemma coprod.symmetry (P Q : C) :
(coprod.braiding P Q).hom ≫ (coprod.braiding Q P).hom = 𝟙 _ :=
by simp

/-- The associator isomorphism for binary coproducts. -/
@[simps] def coprod.associator
(P Q R : C) : (P ⨿ Q) ⨿ R ≅ P ⨿ (Q ⨿ R) :=
{ hom :=
coprod.desc
(coprod.desc coprod.inl (coprod.inl ≫ coprod.inr))
(coprod.inr ≫ coprod.inr),
inv :=
coprod.desc
(coprod.inl ≫ coprod.inl)
(coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) }

lemma coprod.pentagon (W X Y Z : C) :
coprod.map ((coprod.associator W X Y).hom) (𝟙 Z) ≫
(coprod.associator W (X ⨿ Y) Z).hom ≫ coprod.map (𝟙 W) ((coprod.associator X Y Z).hom) =
(coprod.associator (W ⨿ X) Y Z).hom ≫ (coprod.associator W X (Y ⨿ Z)).hom :=
by tidy

lemma coprod.associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
coprod.map (coprod.map f₁ f₂) f₃ ≫ (coprod.associator Y₁ Y₂ Y₃).hom =
(coprod.associator X₁ X₂ X₃).hom ≫ coprod.map f₁ (coprod.map f₂ f₃) :=
by tidy

variables [has_initial C]

/-- The left unitor isomorphism for binary coproducts with the initial object. -/
@[simps] def coprod.left_unitor
(P : C) : ⊥_ C ⨿ P ≅ P :=
{ hom := coprod.desc (initial.to P) (𝟙 _),
inv := coprod.inr }

/-- The right unitor isomorphism for binary coproducts with the initial object. -/
@[simps] def coprod.right_unitor
(P : C) : P ⨿ ⊥_ C ≅ P :=
{ hom := coprod.desc (𝟙 _) (initial.to P),
inv := coprod.inl }

lemma coprod.triangle (X Y : C) :
(coprod.associator X (⊥_ C) Y).hom ≫ coprod.map (𝟙 X) ((coprod.left_unitor Y).hom) =
coprod.map ((coprod.right_unitor X).hom) (𝟙 Y) :=
by tidy

end
end limits

open category_theory.limits

section
Expand All @@ -204,8 +47,8 @@ def monoidal_of_has_finite_products [has_terminal C] [has_binary_products C] : m
tensor_obj := λ X Y, X ⨯ Y,
tensor_hom := λ _ _ _ _ f g, limits.prod.map f g,
associator := prod.associator,
left_unitor := prod.left_unitor,
right_unitor := prod.right_unitor,
left_unitor := λ P, prod.left_unitor P,
right_unitor := λ P, prod.right_unitor P,
pentagon' := prod.pentagon,
triangle' := prod.triangle,
associator_naturality' := @prod.associator_naturality _ _ _, }
Expand All @@ -222,13 +65,13 @@ The monoidal structure coming from finite products is symmetric.
@[simps]
def symmetric_of_has_finite_products [has_terminal C] [has_binary_products C] :
symmetric_category C :=
{ braiding := limits.prod.braiding,
{ braiding := λ X Y, limits.prod.braiding X Y,
braiding_naturality' := λ X X' Y Y' f g,
by { dsimp [tensor_hom], ext; simp, },
by { dsimp [tensor_hom], simp, },
hexagon_forward' := λ X Y Z,
by ext; { dsimp [monoidal_of_has_finite_products], simp; dsimp; simp, },
by { dsimp [monoidal_of_has_finite_products], simp },
hexagon_reverse' := λ X Y Z,
by ext; { dsimp [monoidal_of_has_finite_products], simp; dsimp; simp, },
by { dsimp [monoidal_of_has_finite_products], simp },
symmetry' := λ X Y, by { dsimp, simp, refl, }, }

end
Expand Down Expand Up @@ -292,11 +135,11 @@ def symmetric_of_has_finite_coproducts [has_initial C] [has_binary_coproducts C]
symmetric_category C :=
{ braiding := limits.coprod.braiding,
braiding_naturality' := λ X X' Y Y' f g,
by { dsimp [tensor_hom], ext; simp, },
by { dsimp [tensor_hom], simp, },
hexagon_forward' := λ X Y Z,
by ext; { dsimp [monoidal_of_has_finite_coproducts], simp; dsimp; simp, },
by { dsimp [monoidal_of_has_finite_coproducts], simp },
hexagon_reverse' := λ X Y Z,
by ext; { dsimp [monoidal_of_has_finite_coproducts], simp; dsimp; simp, },
by { dsimp [monoidal_of_has_finite_coproducts], simp },
symmetry' := λ X Y, by { dsimp, simp, refl, }, }

end
Expand Down

0 comments on commit e8c8ce9

Please sign in to comment.