Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-10 12:46 5680428f

View on Github →

chore(category_theory/limits): minor changes in equalizers and products (#3603)

Estimated changes

Modified src/algebra/category/Group/abelian.lean

Modified src/algebra/category/Module/abelian.lean

Modified src/category_theory/abelian/non_preadditive.lean

Modified src/category_theory/limits/lattice.lean

Modified src/category_theory/limits/opposites.lean

added def category_theory.limits.has_colimit_of_has_limit_left_op

added def category_theory.limits.has_colimits_of_shape_op_of_has_limits_of_shape

added def category_theory.limits.has_colimits_op_of_has_limits

added def category_theory.limits.has_coproducts_opposite

added def category_theory.limits.has_limit_of_has_colimit_left_op

added def category_theory.limits.has_limits_of_shape_op_of_has_colimits_of_shape

added def category_theory.limits.has_limits_op_of_has_colimits

added def category_theory.limits.has_products_opposite

Modified src/category_theory/limits/shapes/binary_products.lean

added def category_theory.limits.has_binary_coproducts

added def category_theory.limits.has_binary_products

Modified src/category_theory/limits/shapes/biproducts.lean

Modified src/category_theory/limits/shapes/constructions/binary_products.lean

Modified src/category_theory/limits/shapes/constructions/equalizers.lean

Modified src/category_theory/limits/shapes/constructions/limits_of_products_and_equalizers.lean

Modified src/category_theory/limits/shapes/constructions/over/default.lean

Modified src/category_theory/limits/shapes/constructions/over/products.lean

Modified src/category_theory/limits/shapes/constructions/pullbacks.lean

Modified src/category_theory/limits/shapes/equalizers.lean

added def category_theory.limits.coequalizer.cofork

added theorem category_theory.limits.coequalizer.cofork_ι_app_one

added theorem category_theory.limits.coequalizer.cofork_π

modified def category_theory.limits.coequalizer.iso_target_of_self

modified theorem category_theory.limits.coequalizer.iso_target_of_self_hom

modified theorem category_theory.limits.coequalizer.iso_target_of_self_inv

deleted theorem category_theory.limits.coequalizer.π.cofork

deleted theorem category_theory.limits.coequalizer.π.eq_app_one

modified def category_theory.limits.coequalizer.π_of_eq

modified def category_theory.limits.coequalizer

added def category_theory.limits.cofork.mk_hom

added def category_theory.limits.equalizer.fork

added theorem category_theory.limits.equalizer.fork_ι

added theorem category_theory.limits.equalizer.fork_π_app_zero

modified def category_theory.limits.equalizer.iso_source_of_self

modified theorem category_theory.limits.equalizer.iso_source_of_self_hom

modified theorem category_theory.limits.equalizer.iso_source_of_self_inv

deleted theorem category_theory.limits.equalizer.ι.eq_app_zero

deleted theorem category_theory.limits.equalizer.ι.fork

modified def category_theory.limits.equalizer.ι_of_eq

modified def category_theory.limits.equalizer

added def category_theory.limits.fork.mk_hom

added def category_theory.limits.has_coequalizer

added def category_theory.limits.has_coequalizers

added def category_theory.limits.has_equalizer

added def category_theory.limits.has_equalizers

Modified src/category_theory/limits/shapes/finite_limits.lean

deleted def category_theory.limits.has_coequalizers_of_has_finite_colimits

deleted def category_theory.limits.has_equalizers_of_has_finite_limits

added def category_theory.limits.has_finite_colimits

added def category_theory.limits.has_finite_limits

added def category_theory.limits.has_finite_wide_pullbacks

added def category_theory.limits.has_finite_wide_pushouts

deleted def category_theory.limits.has_pullbacks_of_has_finite_limits

deleted def category_theory.limits.has_pushouts_of_has_finite_colimits

Modified src/category_theory/limits/shapes/finite_products.lean

added def category_theory.limits.has_finite_coproducts

added def category_theory.limits.has_finite_coproducts_of_has_coproducts

added def category_theory.limits.has_finite_products

added def category_theory.limits.has_finite_products_of_has_products

Modified src/category_theory/limits/shapes/products.lean

added def category_theory.limits.has_coproducts

added def category_theory.limits.has_products

Modified src/category_theory/limits/shapes/pullbacks.lean

added def category_theory.limits.has_pullback

added def category_theory.limits.has_pullbacks

added def category_theory.limits.has_pushout

added def category_theory.limits.has_pushouts

modified theorem category_theory.limits.pullback.condition

modified def category_theory.limits.pullback.desc'

modified def category_theory.limits.pullback.fst

modified theorem category_theory.limits.pullback.hom_ext

modified def category_theory.limits.pullback.lift'

modified def category_theory.limits.pullback.lift

modified theorem category_theory.limits.pullback.lift_fst

modified theorem category_theory.limits.pullback.lift_snd

modified def category_theory.limits.pullback.snd

modified def category_theory.limits.pullback

modified theorem category_theory.limits.pushout.condition

modified def category_theory.limits.pushout.desc

modified theorem category_theory.limits.pushout.hom_ext

modified def category_theory.limits.pushout.inl

modified theorem category_theory.limits.pushout.inl_desc

modified def category_theory.limits.pushout.inr

modified theorem category_theory.limits.pushout.inr_desc

modified def category_theory.limits.pushout

Modified src/category_theory/limits/shapes/terminal.lean

added def category_theory.limits.has_initial

added def category_theory.limits.has_terminal

Modified src/category_theory/limits/shapes/types.lean

added theorem category_theory.limits.types.pi

added theorem category_theory.limits.types.pi_lift

added theorem category_theory.limits.types.pi_map

added theorem category_theory.limits.types.pi_π

modified def category_theory.limits.types.types_has_products

Modified src/category_theory/limits/shapes/wide_pullbacks.lean

added def category_theory.limits.has_wide_pullbacks

added def category_theory.limits.has_wide_pushouts