Commit 2022-11-05 17:02 f187f107

View on Github →

feat(category_theory/groupoid/*): is_thin and is_totally_disconnected (#17122) Define is_thin for quivers and subgroupoids and is_totally_disconnected for groupoids and subgroupoids.

Estimated changes

Modified src/category_theory/bicategory/coherence.lean

Modified src/category_theory/essentially_small.lean

Modified src/category_theory/generator.lean

modified theorem category_theory.is_coseparating_empty_of_thin

modified theorem category_theory.is_separating_empty_of_thin

modified theorem category_theory.thin_of_is_coseparating_empty

modified theorem category_theory.thin_of_is_separating_empty

Created src/category_theory/groupoid/basic.lean

added theorem category_theory.groupoid.is_thin_iff

added def category_theory.groupoid.is_totally_disconnected

Modified src/category_theory/groupoid/subgroupoid.lean

added def category_theory.subgroupoid.disconnect

added theorem category_theory.subgroupoid.disconnect_is_totally_disconnected

added theorem category_theory.subgroupoid.disconnect_le

added theorem category_theory.subgroupoid.disconnect_normal

added theorem category_theory.subgroupoid.disconnect_objs

added def category_theory.subgroupoid.full

added theorem category_theory.subgroupoid.full_arrow_eq_iff

added theorem category_theory.subgroupoid.full_empty

added theorem category_theory.subgroupoid.full_mono

added theorem category_theory.subgroupoid.full_objs

added theorem category_theory.subgroupoid.full_univ

modified theorem category_theory.subgroupoid.inclusion_faithful

added def category_theory.subgroupoid.is_thin

added theorem category_theory.subgroupoid.is_thin_iff

added def category_theory.subgroupoid.is_totally_disconnected

added theorem category_theory.subgroupoid.is_totally_disconnected_iff

modified theorem category_theory.subgroupoid.map_objs_eq

added theorem category_theory.subgroupoid.mem_disconnect_objs_iff

modified theorem category_theory.subgroupoid.mem_discrete_iff

added theorem category_theory.subgroupoid.mem_full_iff

added theorem category_theory.subgroupoid.mem_full_objs_iff

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

Modified src/category_theory/limits/small_complete.lean

Modified src/category_theory/monoidal/free/coherence.lean

Modified src/category_theory/skeletal.lean

modified theorem category_theory.functor.eq_of_iso

modified theorem category_theory.functor_skeletal

Modified src/category_theory/subobject/mono_over.lean

Modified src/category_theory/thin.lean

Modified src/combinatorics/quiver/basic.lean

added def quiver.is_thin