Commit 2023-06-12 15:16 9d9686a1

View on Github →

feat: port CategoryTheory.Groupoid.Subgroupoid (#4975)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean

added inductive CategoryTheory.Subgroupoid.Discrete.Arrows

added theorem CategoryTheory.Subgroupoid.IsNormal.conj'

added theorem CategoryTheory.Subgroupoid.IsNormal.conjugation_bij

added theorem CategoryTheory.Subgroupoid.IsNormal.generatedNormal_le

added theorem CategoryTheory.Subgroupoid.IsNormal.vertexSubgroup

added structure CategoryTheory.Subgroupoid.IsNormal

added theorem CategoryTheory.Subgroupoid.IsWide.eqToHom_mem

added theorem CategoryTheory.Subgroupoid.IsWide.id_mem

added structure CategoryTheory.Subgroupoid.IsWide

added inductive CategoryTheory.Subgroupoid.Map.Arrows

added theorem CategoryTheory.Subgroupoid.Map.arrows_iff

added def CategoryTheory.Subgroupoid.asWideQuiver

added theorem CategoryTheory.Subgroupoid.coe_inv_coe'

added def CategoryTheory.Subgroupoid.comap

added theorem CategoryTheory.Subgroupoid.comap_comp

added theorem CategoryTheory.Subgroupoid.comap_mono

added def CategoryTheory.Subgroupoid.disconnect

added theorem CategoryTheory.Subgroupoid.disconnect_isTotallyDisconnected

added theorem CategoryTheory.Subgroupoid.disconnect_le

added theorem CategoryTheory.Subgroupoid.disconnect_normal

added theorem CategoryTheory.Subgroupoid.disconnect_objs

added def CategoryTheory.Subgroupoid.discrete

added theorem CategoryTheory.Subgroupoid.discrete_isNormal

added def CategoryTheory.Subgroupoid.full

added theorem CategoryTheory.Subgroupoid.full_arrow_eq_iff

added theorem CategoryTheory.Subgroupoid.full_empty

added theorem CategoryTheory.Subgroupoid.full_mono

added theorem CategoryTheory.Subgroupoid.full_objs

added theorem CategoryTheory.Subgroupoid.full_univ

added theorem CategoryTheory.Subgroupoid.galoisConnection_map_comap

added def CategoryTheory.Subgroupoid.generated

added def CategoryTheory.Subgroupoid.generatedNormal

added theorem CategoryTheory.Subgroupoid.generatedNormal_isNormal

added theorem CategoryTheory.Subgroupoid.generated_le_generatedNormal

added theorem CategoryTheory.Subgroupoid.hom.faithful

added theorem CategoryTheory.Subgroupoid.hom.inj_on_objects

added def CategoryTheory.Subgroupoid.hom

added theorem CategoryTheory.Subgroupoid.id_mem_of_nonempty_isotropy

added theorem CategoryTheory.Subgroupoid.id_mem_of_src

added theorem CategoryTheory.Subgroupoid.id_mem_of_tgt

added def CategoryTheory.Subgroupoid.im

added def CategoryTheory.Subgroupoid.inclusion

added theorem CategoryTheory.Subgroupoid.inclusion_comp_embedding

added theorem CategoryTheory.Subgroupoid.inclusion_faithful

added theorem CategoryTheory.Subgroupoid.inclusion_inj_on_objects

added theorem CategoryTheory.Subgroupoid.inclusion_refl

added theorem CategoryTheory.Subgroupoid.inclusion_trans

added theorem CategoryTheory.Subgroupoid.inv_mem_iff

added theorem CategoryTheory.Subgroupoid.isNormal_comap

added theorem CategoryTheory.Subgroupoid.isNormal_map

added theorem CategoryTheory.Subgroupoid.isTotallyDisconnected_iff

added theorem CategoryTheory.Subgroupoid.isWide_iff_objs_eq_univ

added def CategoryTheory.Subgroupoid.ker

added theorem CategoryTheory.Subgroupoid.ker_comp

added theorem CategoryTheory.Subgroupoid.ker_isNormal

added theorem CategoryTheory.Subgroupoid.le_comap_map

added theorem CategoryTheory.Subgroupoid.le_iff

added theorem CategoryTheory.Subgroupoid.le_objs

added def CategoryTheory.Subgroupoid.map

added theorem CategoryTheory.Subgroupoid.map_comap_le

added theorem CategoryTheory.Subgroupoid.map_le_iff_le_comap

added theorem CategoryTheory.Subgroupoid.map_mono

added theorem CategoryTheory.Subgroupoid.map_objs_eq

added theorem CategoryTheory.Subgroupoid.mem_disconnect_objs_iff

added theorem CategoryTheory.Subgroupoid.mem_discrete_iff

added theorem CategoryTheory.Subgroupoid.mem_full_iff

added theorem CategoryTheory.Subgroupoid.mem_full_objs_iff

added theorem CategoryTheory.Subgroupoid.mem_iff

added theorem CategoryTheory.Subgroupoid.mem_im_iff

added theorem CategoryTheory.Subgroupoid.mem_im_objs_iff

added theorem CategoryTheory.Subgroupoid.mem_ker_iff

added theorem CategoryTheory.Subgroupoid.mem_map_iff

added theorem CategoryTheory.Subgroupoid.mem_map_objs_iff

added theorem CategoryTheory.Subgroupoid.mem_objs_of_src

added theorem CategoryTheory.Subgroupoid.mem_objs_of_tgt

added theorem CategoryTheory.Subgroupoid.mem_sInf

added theorem CategoryTheory.Subgroupoid.mem_sInf_arrows

added theorem CategoryTheory.Subgroupoid.mem_top

added theorem CategoryTheory.Subgroupoid.mem_top_objs

added theorem CategoryTheory.Subgroupoid.mul_mem_cancel_left

added theorem CategoryTheory.Subgroupoid.mul_mem_cancel_right

added theorem CategoryTheory.Subgroupoid.obj_surjective_of_im_eq_top

added def CategoryTheory.Subgroupoid.objs

added theorem CategoryTheory.Subgroupoid.sInf_isNormal

added theorem CategoryTheory.Subgroupoid.subset_generated

added def CategoryTheory.Subgroupoid.toSet

added theorem CategoryTheory.Subgroupoid.top_isNormal

added def CategoryTheory.Subgroupoid.vertexSubgroup

added structure CategoryTheory.Subgroupoid