Skip to content

Commit

Permalink
chore(category_theory): put biproduct results on preadditive categori…
Browse files Browse the repository at this point in the history 
…es into the correct file (#16924)
  • Loading branch information
@javra
javra committed Oct 13, 2022
1 parent b68e4a8 commit 234ddfe
Show file tree
Hide file tree
Showing 7 changed files with 818 additions and 832 deletions.
2 changes: 1 addition & 1 deletion src/algebra/category/Group/biproducts.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Scott Morrison
-/
import algebra.group.pi
import algebra.category.Group.preadditive
import category_theory.limits.shapes.biproducts
import category_theory.preadditive.biproducts
import algebra.category.Group.limits

/-!
Expand Down
2 changes: 1 addition & 1 deletion src/category_theory/abelian/basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Markus Himmel, Johan Commelin, Scott Morrison
-/

import category_theory.limits.constructions.pullbacks
import category_theory.limits.shapes.biproducts
import category_theory.preadditive.biproducts
import category_theory.limits.shapes.images
import category_theory.limits.constructions.limits_of_products_and_equalizers
import category_theory.limits.constructions.epi_mono
Expand Down
216 changes: 1 addition & 215 deletions src/category_theory/limits/preserves/shapes/biproducts.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,7 @@ classes `preserves_biproduct` and `preserves_binary_biproduct`. We then
* construct the comparison morphisms between the image of a biproduct and the biproduct of the
images and show that the biproduct is preserved if one of them is an isomorphism,
* give the canonical isomorphism between the image of a biproduct and the biproduct of the images
in case that the biproduct is preserved,
* show that in a preadditive category, a functor preserves a biproduct if and only if it preserves
the corresponding product if and only if it preserves the corresponding coproduct.
in case that the biproduct is preserved.
-/

Expand Down Expand Up @@ -380,216 +378,4 @@ end limits

end has_zero_morphisms

open category_theory.functor

section preadditive
variables [preadditive C] [preadditive D] (F : C ⥤ D) [preserves_zero_morphisms F]

namespace limits

section fintype
variables {J : Type} [fintype J]

local attribute [tidy] tactic.discrete_cases

/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
preserves finite products. -/
def preserves_product_of_preserves_biproduct {f : J → C} [preserves_biproduct f F] :
preserves_limit (discrete.functor f) F :=
{ preserves := λ c hc, is_limit.of_iso_limit
((is_limit.postcompose_inv_equiv (discrete.comp_nat_iso_discrete _ _) _).symm
(is_bilimit_of_preserves F (bicone_is_bilimit_of_limit_cone_of_is_limit hc)).is_limit) $
cones.ext (iso.refl _) (by tidy) }

section
local attribute [instance] preserves_product_of_preserves_biproduct

/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
preserves finite products. -/
def preserves_products_of_shape_of_preserves_biproducts_of_shape
[preserves_biproducts_of_shape J F] : preserves_limits_of_shape (discrete J) F :=
{ preserves_limit := λ f, preserves_limit_of_iso_diagram _ discrete.nat_iso_functor.symm }

end

/-- A functor between preadditive categories that preserves (zero morphisms and) finite products
preserves finite biproducts. -/
def preserves_biproduct_of_preserves_product {f : J → C} [preserves_limit (discrete.functor f) F] :
preserves_biproduct f F :=
{ preserves := λ b hb, is_bilimit_of_is_limit _ $
is_limit.of_iso_limit ((is_limit.postcompose_hom_equiv (discrete.comp_nat_iso_discrete _ _)
(F.map_cone b.to_cone)).symm (is_limit_of_preserves F hb.is_limit)) $
cones.ext (iso.refl _) (by tidy) }

/-- If the (product-like) biproduct comparison for `F` and `f` is a monomorphism, then `F`
preserves the biproduct of `f`. For the converse, see `map_biproduct`. -/
def preserves_biproduct_of_mono_biproduct_comparison {f : J → C} [has_biproduct f]
[has_biproduct (F.obj ∘ f)] [mono (biproduct_comparison F f)] : preserves_biproduct f F :=
begin
have : pi_comparison F f = (F.map_iso (biproduct.iso_product f)).inv ≫
biproduct_comparison F f ≫ (biproduct.iso_product _).hom,
{ ext, convert pi_comparison_comp_π F f j.as; simp [← functor.map_comp] },
haveI : is_iso (biproduct_comparison F f) := is_iso_of_mono_of_is_split_epi _,
haveI : is_iso (pi_comparison F f) := by { rw this, apply_instance },
haveI := preserves_product.of_iso_comparison F f,
apply preserves_biproduct_of_preserves_product
end

/-- If the (coproduct-like) biproduct comparison for `F` and `f` is an epimorphism, then `F`
preserves the biproduct of `F` and `f`. For the converse, see `map_biproduct`. -/
def preserves_biproduct_of_epi_biproduct_comparison' {f : J → C} [has_biproduct f]
[has_biproduct (F.obj ∘ f)] [epi (biproduct_comparison' F f)] : preserves_biproduct f F :=
begin
haveI : epi ((split_epi_biproduct_comparison F f).section_) := by simpa,
haveI : is_iso (biproduct_comparison F f) := is_iso.of_epi_section'
(split_epi_biproduct_comparison F f),
apply preserves_biproduct_of_mono_biproduct_comparison
end

/-- A functor between preadditive categories that preserves (zero morphisms and) finite products
preserves finite biproducts. -/
def preserves_biproducts_of_shape_of_preserves_products_of_shape
[preserves_limits_of_shape (discrete J) F] : preserves_biproducts_of_shape J F :=
{ preserves := λ f, preserves_biproduct_of_preserves_product F }

/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
preserves finite coproducts. -/
def preserves_coproduct_of_preserves_biproduct {f : J → C} [preserves_biproduct f F] :
preserves_colimit (discrete.functor f) F :=
{ preserves := λ c hc, is_colimit.of_iso_colimit
((is_colimit.precompose_hom_equiv (discrete.comp_nat_iso_discrete _ _) _).symm
(is_bilimit_of_preserves F
(bicone_is_bilimit_of_colimit_cocone_of_is_colimit hc)).is_colimit) $
cocones.ext (iso.refl _) (by tidy) }

section
local attribute [instance] preserves_coproduct_of_preserves_biproduct

/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
preserves finite coproducts. -/
def preserves_coproducts_of_shape_of_preserves_biproducts_of_shape
[preserves_biproducts_of_shape J F] : preserves_colimits_of_shape (discrete J) F :=
{ preserves_colimit := λ f, preserves_colimit_of_iso_diagram _ discrete.nat_iso_functor.symm }

end

/-- A functor between preadditive categories that preserves (zero morphisms and) finite coproducts
preserves finite biproducts. -/
def preserves_biproduct_of_preserves_coproduct {f : J → C}
[preserves_colimit (discrete.functor f) F] : preserves_biproduct f F :=
{ preserves := λ b hb, is_bilimit_of_is_colimit _ $
is_colimit.of_iso_colimit ((is_colimit.precompose_inv_equiv (discrete.comp_nat_iso_discrete _ _)
(F.map_cocone b.to_cocone)).symm (is_colimit_of_preserves F hb.is_colimit)) $
cocones.ext (iso.refl _) (by tidy) }

/-- A functor between preadditive categories that preserves (zero morphisms and) finite coproducts
preserves finite biproducts. -/
def preserves_biproducts_of_shape_of_preserves_coproducts_of_shape
[preserves_colimits_of_shape (discrete J) F] : preserves_biproducts_of_shape J F :=
{ preserves := λ f, preserves_biproduct_of_preserves_coproduct F }

end fintype

/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
preserves binary products. -/
def preserves_binary_product_of_preserves_binary_biproduct {X Y : C}
[preserves_binary_biproduct X Y F] : preserves_limit (pair X Y) F :=
{ preserves := λ c hc, is_limit.of_iso_limit
((is_limit.postcompose_inv_equiv (by exact diagram_iso_pair _) _).symm
(is_binary_bilimit_of_preserves F
(binary_bicone_is_bilimit_of_limit_cone_of_is_limit hc)).is_limit) $
cones.ext (iso.refl _) (λ j, by { rcases j with ⟨⟨⟩⟩, tidy }) }

section
local attribute [instance] preserves_binary_product_of_preserves_binary_biproduct

/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
preserves binary products. -/
def preserves_binary_products_of_preserves_binary_biproducts
[preserves_binary_biproducts F] : preserves_limits_of_shape (discrete walking_pair) F :=
{ preserves_limit := λ K, preserves_limit_of_iso_diagram _ (diagram_iso_pair _).symm }

end

/-- A functor between preadditive categories that preserves (zero morphisms and) binary products
preserves binary biproducts. -/
def preserves_binary_biproduct_of_preserves_binary_product {X Y : C}
[preserves_limit (pair X Y) F] : preserves_binary_biproduct X Y F :=
{ preserves := λ b hb, is_binary_bilimit_of_is_limit _ $
is_limit.of_iso_limit ((is_limit.postcompose_hom_equiv (by exact diagram_iso_pair _)
(F.map_cone b.to_cone)).symm (is_limit_of_preserves F hb.is_limit)) $
cones.ext (iso.refl _) (λ j, by { rcases j with ⟨⟨⟩⟩, tidy }) }

/-- If the (product-like) biproduct comparison for `F`, `X` and `Y` is a monomorphism, then
`F` preserves the biproduct of `X` and `Y`. For the converse, see `map_biprod`. -/
def preserves_binary_biproduct_of_mono_biprod_comparison {X Y : C} [has_binary_biproduct X Y]
[has_binary_biproduct (F.obj X) (F.obj Y)] [mono (biprod_comparison F X Y)] :
preserves_binary_biproduct X Y F :=
begin
have : prod_comparison F X Y = (F.map_iso (biprod.iso_prod X Y)).inv ≫
biprod_comparison F X Y ≫ (biprod.iso_prod _ _).hom := by { ext; simp [← functor.map_comp] },
haveI : is_iso (biprod_comparison F X Y) := is_iso_of_mono_of_is_split_epi _,
haveI : is_iso (prod_comparison F X Y) := by { rw this, apply_instance },
haveI := preserves_limit_pair.of_iso_prod_comparison F X Y,
apply preserves_binary_biproduct_of_preserves_binary_product
end

/-- If the (coproduct-like) biproduct comparison for `F`, `X` and `Y` is an epimorphism, then
`F` preserves the biproduct of `X` and `Y`. For the converse, see `map_biprod`. -/
def preserves_binary_biproduct_of_epi_biprod_comparison' {X Y : C} [has_binary_biproduct X Y]
[has_binary_biproduct (F.obj X) (F.obj Y)] [epi (biprod_comparison' F X Y)] :
preserves_binary_biproduct X Y F :=
begin
haveI : epi ((split_epi_biprod_comparison F X Y).section_) := by simpa,
haveI : is_iso (biprod_comparison F X Y) := is_iso.of_epi_section'
(split_epi_biprod_comparison F X Y),
apply preserves_binary_biproduct_of_mono_biprod_comparison
end

/-- A functor between preadditive categories that preserves (zero morphisms and) binary products
preserves binary biproducts. -/
def preserves_binary_biproducts_of_preserves_binary_products
[preserves_limits_of_shape (discrete walking_pair) F] : preserves_binary_biproducts F :=
{ preserves := λ X Y, preserves_binary_biproduct_of_preserves_binary_product F }

/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
preserves binary coproducts. -/
def preserves_binary_coproduct_of_preserves_binary_biproduct {X Y : C}
[preserves_binary_biproduct X Y F] : preserves_colimit (pair X Y) F :=
{ preserves := λ c hc, is_colimit.of_iso_colimit
((is_colimit.precompose_hom_equiv (by exact diagram_iso_pair _) _).symm
(is_binary_bilimit_of_preserves F
(binary_bicone_is_bilimit_of_colimit_cocone_of_is_colimit hc)).is_colimit) $
cocones.ext (iso.refl _) (λ j, by { rcases j with ⟨⟨⟩⟩, tidy }) }

section
local attribute [instance] preserves_binary_coproduct_of_preserves_binary_biproduct

/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
preserves binary coproducts. -/
def preserves_binary_coproducts_of_preserves_binary_biproducts
[preserves_binary_biproducts F] : preserves_colimits_of_shape (discrete walking_pair) F :=
{ preserves_colimit := λ K, preserves_colimit_of_iso_diagram _ (diagram_iso_pair _).symm }

end

/-- A functor between preadditive categories that preserves (zero morphisms and) binary coproducts
preserves binary biproducts. -/
def preserves_binary_biproduct_of_preserves_binary_coproduct {X Y : C}
[preserves_colimit (pair X Y) F] : preserves_binary_biproduct X Y F :=
{ preserves := λ b hb, is_binary_bilimit_of_is_colimit _ $
is_colimit.of_iso_colimit ((is_colimit.precompose_inv_equiv (by exact diagram_iso_pair _)
(F.map_cocone b.to_cocone)).symm (is_colimit_of_preserves F hb.is_colimit)) $
cocones.ext (iso.refl _) (λ j, by { rcases j with ⟨⟨⟩⟩, tidy }) }

/-- A functor between preadditive categories that preserves (zero morphisms and) binary coproducts
preserves binary biproducts. -/
def preserves_binary_biproducts_of_preserves_binary_coproducts
[preserves_colimits_of_shape (discrete walking_pair) F] : preserves_binary_biproducts F :=
{ preserves := λ X Y, preserves_binary_biproduct_of_preserves_binary_coproduct F }

end limits

end preadditive

end category_theory
Loading

0 comments on commit 234ddfe

Please sign in to comment.