Commit 2022-10-14 06:45 7a52b9ce

View on Github →

feat(category_theory/groupoid/subgroupoid): subgroupoids and basic properties (#16742) Add a definition of (bundled) subgroupoid and prove some of their basic properties.

Estimated changes

Modified src/category_theory/endomorphism.lean

added theorem category_theory.Aut.Aut_inv_def

Created src/category_theory/groupoid/subgroupoid.lean

added theorem category_theory.subgroupoid.Inf_is_normal

added def category_theory.subgroupoid.as_wide_quiver

added def category_theory.subgroupoid.comap

added theorem category_theory.subgroupoid.comap_mono

added inductive category_theory.subgroupoid.discrete.arrows

added def category_theory.subgroupoid.discrete

added def category_theory.subgroupoid.generated

added def category_theory.subgroupoid.generated_normal

added theorem category_theory.subgroupoid.generated_normal_is_normal

added theorem category_theory.subgroupoid.hom.faithful

added theorem category_theory.subgroupoid.hom.inj_on_objects

added def category_theory.subgroupoid.hom

added theorem category_theory.subgroupoid.id_mem_of_nonempty_isotropy

added def category_theory.subgroupoid.im

added def category_theory.subgroupoid.inclusion

added theorem category_theory.subgroupoid.inclusion_comp_embedding

added theorem category_theory.subgroupoid.inclusion_faithful

added theorem category_theory.subgroupoid.inclusion_inj_on_objects

added theorem category_theory.subgroupoid.inclusion_refl

added theorem category_theory.subgroupoid.inclusion_trans

added theorem category_theory.subgroupoid.is_normal.conj'

added theorem category_theory.subgroupoid.is_normal.conjugation_bij

added theorem category_theory.subgroupoid.is_normal.vertex_subgroup

added structure category_theory.subgroupoid.is_normal

added theorem category_theory.subgroupoid.is_normal_comap

added def category_theory.subgroupoid.ker

added theorem category_theory.subgroupoid.le_iff

added theorem category_theory.subgroupoid.le_objs

added inductive category_theory.subgroupoid.map.arrows

added theorem category_theory.subgroupoid.map.mem_arrows_iff

added def category_theory.subgroupoid.map

added theorem category_theory.subgroupoid.map_mono

added theorem category_theory.subgroupoid.mem_discrete_iff

added theorem category_theory.subgroupoid.mem_iff

added theorem category_theory.subgroupoid.mem_im_iff

added theorem category_theory.subgroupoid.mem_ker_iff

added def category_theory.subgroupoid.objs

added theorem category_theory.subgroupoid.top_is_normal

added def category_theory.subgroupoid.vertex_subgroup

added structure category_theory.subgroupoid

Created src/category_theory/groupoid/vertex_group.lean

added def category_theory.functor.map_vertex_group

added theorem category_theory.groupoid.vertex_group.inv_eq_inv

added def category_theory.groupoid.vertex_group_isom_of_map

added def category_theory.groupoid.vertex_group_isom_of_path