Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-09 03:23 a6d9c65a

View on Github →

feat(category_theory/extensive): Define extensive categories (#17318)

Estimated changes

Modified docs/references.bib

Created src/category_theory/extensive.lean

added theorem category_theory.binary_cofan.is_pullback_initial_to_of_is_van_kampen

added theorem category_theory.binary_cofan.is_van_kampen_iff

added theorem category_theory.binary_cofan.is_van_kampen_mk

added theorem category_theory.binary_cofan.mono_inr_of_is_van_kampen

added theorem category_theory.finitary_extensive.is_pullback_initial_to_binary_cofan

added theorem category_theory.finitary_extensive.mono_inl_of_is_colimit

added theorem category_theory.finitary_extensive.mono_inr_of_is_colimit

added theorem category_theory.finitary_extensive.van_kampen

added theorem category_theory.finitary_extensive_iff_of_is_terminal

added theorem category_theory.has_strict_initial_of_is_universal

added theorem category_theory.is_initial.is_van_kampen_colimit

added def category_theory.is_universal_colimit

added def category_theory.is_van_kampen_colimit.is_colimit

added theorem category_theory.is_van_kampen_colimit.is_universal

added def category_theory.is_van_kampen_colimit

added theorem category_theory.map_pair_equifibered

added theorem category_theory.nat_trans.equifibered.comp

added def category_theory.nat_trans.equifibered

added theorem category_theory.nat_trans.equifibered_of_is_iso