Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-05-20 00:16
c9c9fa15
View on Github →
refactor(category_theory/discrete): make discrete irreducible (
#13762
)
Estimated changes
Modified
src/algebra/category/Group/biproducts.lean
added
theorem
AddCommGroup.biprod_iso_prod_inv_comp_fst
added
theorem
AddCommGroup.biprod_iso_prod_inv_comp_snd
modified
def
AddCommGroup.has_limit.lift
deleted
theorem
AddCommGroup.has_limit.lift_apply
modified
def
AddCommGroup.has_limit.product_limit_cone
Modified
src/algebra/category/Module/biproducts.lean
modified
def
Module.has_limit.lift
deleted
theorem
Module.has_limit.lift_apply
modified
def
Module.has_limit.product_limit_cone
Modified
src/algebra/category/Module/products.lean
Modified
src/algebra/category/Ring/constructions.lean
Modified
src/algebraic_geometry/locally_ringed_space/has_colimits.lean
Modified
src/algebraic_geometry/open_immersion.lean
modified
theorem
algebraic_geometry.SheafedSpace.is_open_immersion.image_preimage_is_empty
Modified
src/algebraic_geometry/sheafed_space.lean
Modified
src/algebraic_topology/fundamental_groupoid/product.lean
Modified
src/category_theory/adjunction/comma.lean
Modified
src/category_theory/adjunction/evaluation.lean
Modified
src/category_theory/adjunction/over.lean
Modified
src/category_theory/bicategory/coherence.lean
added
theorem
category_theory.free_bicategory.preinclusion_map₂
Modified
src/category_theory/bicategory/locally_discrete.lean
added
theorem
category_theory.locally_discrete.eq_of_hom
modified
def
category_theory.locally_discrete
Modified
src/category_theory/category/Cat.lean
Modified
src/category_theory/category/Groupoid.lean
deleted
def
category_theory.Groupoid.pi_limit_cone
modified
def
category_theory.Groupoid.pi_limit_fan
added
def
category_theory.Groupoid.pi_limit_fan_is_limit
Modified
src/category_theory/discrete_category.lean
modified
theorem
category_theory.discrete.eq_of_hom
added
def
category_theory.discrete.eq_to_hom'
added
def
category_theory.discrete.eq_to_hom
added
def
category_theory.discrete.eq_to_iso'
added
def
category_theory.discrete.eq_to_iso
modified
theorem
category_theory.discrete.id_def
added
theorem
category_theory.discrete.mk_as
modified
def
category_theory.discrete.nat_iso_functor
deleted
theorem
category_theory.discrete.nat_iso_hom_app
deleted
theorem
category_theory.discrete.nat_iso_inv_app
deleted
theorem
category_theory.discrete.nat_trans_app
added
structure
category_theory.discrete
deleted
def
category_theory.discrete
added
def
category_theory.discrete_equiv
Modified
src/category_theory/elements.lean
Modified
src/category_theory/fin_category.lean
Modified
src/category_theory/functor/flat.lean
Modified
src/category_theory/graded_object.lean
Modified
src/category_theory/grothendieck.lean
Modified
src/category_theory/is_connected.lean
Modified
src/category_theory/limits/cones.lean
Modified
src/category_theory/limits/constructions/binary_products.lean
Modified
src/category_theory/limits/constructions/finite_products_of_binary_products.lean
Modified
src/category_theory/limits/constructions/limits_of_products_and_equalizers.lean
Modified
src/category_theory/limits/constructions/over/products.lean
Modified
src/category_theory/limits/final.lean
Modified
src/category_theory/limits/kan_extension.lean
Modified
src/category_theory/limits/lattice.lean
Modified
src/category_theory/limits/preserves/shapes/biproducts.lean
Modified
src/category_theory/limits/preserves/shapes/products.lean
Modified
src/category_theory/limits/presheaf.lean
Modified
src/category_theory/limits/punit.lean
Modified
src/category_theory/limits/shapes/binary_products.lean
modified
def
category_theory.limits.binary_cofan.inl
modified
def
category_theory.limits.binary_cofan.inr
modified
def
category_theory.limits.binary_fan.fst
modified
def
category_theory.limits.binary_fan.snd
modified
def
category_theory.limits.map_pair
modified
def
category_theory.limits.map_pair_iso
modified
theorem
category_theory.limits.map_pair_left
modified
theorem
category_theory.limits.map_pair_right
added
def
category_theory.limits.pair_function
added
theorem
category_theory.limits.pair_function_left
added
theorem
category_theory.limits.pair_function_right
modified
theorem
category_theory.limits.pair_obj_left
modified
theorem
category_theory.limits.pair_obj_right
Modified
src/category_theory/limits/shapes/biproducts.lean
modified
def
category_theory.limits.bicone.to_binary_bicone
modified
def
category_theory.limits.bicone.to_binary_bicone_is_bilimit
modified
def
category_theory.limits.bicone.to_binary_bicone_is_colimit
modified
def
category_theory.limits.bicone.to_binary_bicone_is_limit
added
theorem
category_theory.limits.bicone.to_cocone_X
added
theorem
category_theory.limits.bicone.to_cocone_ι_app
added
theorem
category_theory.limits.bicone.to_cone_X
added
theorem
category_theory.limits.bicone.to_cone_π_app
modified
def
category_theory.limits.binary_bicone.to_bicone
Modified
src/category_theory/limits/shapes/disjoint_coproduct.lean
Modified
src/category_theory/limits/shapes/multiequalizer.lean
Modified
src/category_theory/limits/shapes/products.lean
added
def
category_theory.limits.fan.proj
added
theorem
category_theory.limits.fan_mk_proj
added
theorem
category_theory.limits.has_products_of_limit_fans
added
def
category_theory.limits.mk_fan_limit
Modified
src/category_theory/limits/shapes/terminal.lean
Modified
src/category_theory/limits/shapes/types.lean
Modified
src/category_theory/limits/shapes/zero_objects.lean
Modified
src/category_theory/limits/small_complete.lean
Modified
src/category_theory/monoidal/CommMon_.lean
Modified
src/category_theory/monoidal/Mon_.lean
Modified
src/category_theory/monoidal/braided.lean
Modified
src/category_theory/monoidal/discrete.lean
Modified
src/category_theory/monoidal/free/coherence.lean
added
theorem
category_theory.free_monoidal_category.discrete_functor_map_eq_id
added
theorem
category_theory.free_monoidal_category.discrete_functor_obj_eq_as
modified
def
category_theory.free_monoidal_category.normalize_obj
modified
theorem
category_theory.free_monoidal_category.normalize_obj_tensor
modified
theorem
category_theory.free_monoidal_category.normalize_obj_unitor
Modified
src/category_theory/monoidal/of_chosen_finite_products.lean
Modified
src/category_theory/opposites.lean
added
def
category_theory.iso_op_equiv
Modified
src/category_theory/over.lean
modified
theorem
category_theory.over.over_right
modified
theorem
category_theory.under.under_left
Modified
src/category_theory/pempty.lean
Modified
src/category_theory/preadditive/additive_functor.lean
Modified
src/category_theory/preadditive/injective.lean
Modified
src/category_theory/preadditive/projective.lean
Modified
src/category_theory/punit.lean
Modified
src/category_theory/shift.lean
modified
theorem
category_theory.has_shift.shift_obj_obj
modified
def
category_theory.opaque_eq_to_iso
modified
def
category_theory.shift_functor
Modified
src/category_theory/simple.lean
Modified
src/category_theory/sites/sheaf_of_types.lean
Modified
src/category_theory/structured_arrow.lean
modified
def
category_theory.costructured_arrow.mk
modified
theorem
category_theory.costructured_arrow.mk_right
modified
def
category_theory.structured_arrow.mk
modified
theorem
category_theory.structured_arrow.mk_left
Modified
src/category_theory/subterminal.lean
Modified
src/order/category/omega_complete_partial_order.lean
Modified
src/topology/category/Top/limits.lean
Modified
src/topology/gluing.lean
Modified
src/topology/sheaves/sheaf_condition/equalizer_products.lean
modified
theorem
Top.presheaf.sheaf_condition_equalizer_products.res_π
Modified
src/topology/sheaves/sheaf_condition/opens_le_cover.lean
Modified
src/topology/sheaves/sheaf_condition/pairwise_intersections.lean
Modified
src/topology/sheaves/sheaf_condition/sites.lean
Modified
src/topology/sheaves/sheaf_condition/unique_gluing.lean
Modified
src/topology/sheaves/stalks.lean