chore(category_theory/groupoid/*) More subgroupoid lemmas (#17147)

More subgroupoid lemmas and a few minor general cleanups.



Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

src/category_theory/groupoid.lean

@@ -71,8 +71,10 @@ is_iso.eq_inv_of_hom_inv_id $ groupoid.comp_inv f
 
 @[priority 100]
 instance groupoid_has_involutive_reverse : quiver.has_involutive_reverse C :=
-{ reverse' := λ X Y f, groupoid.inv f
-, inv' := λ X Y f, by { dsimp [quiver.reverse], simp, } }
+{ reverse' := λ X Y f, groupoid.inv f,
+  inv' := λ X Y f, by { dsimp [quiver.reverse], simp, } }
+
+@[simp] lemma groupoid.reverse_eq_inv (f : X ⟶ Y) : quiver.reverse f = groupoid.inv f := rfl
 
 variables (X Y)
 

src/category_theory/groupoid/free_groupoid.lean

@@ -6,8 +6,6 @@ Authors: Rémi Bottinelli
 import category_theory.category.basic
 import category_theory.functor.basic
 import category_theory.groupoid
-import combinatorics.quiver.basic
-import combinatorics.quiver.connected_component
 import logic.relation
 import tactic.nth_rewrite
 import category_theory.path_category
@@ -70,9 +68,9 @@ inductive red_step : hom_rel (paths (quiver.symmetrify V))
     red_step (𝟙 X) (f.to_path ≫ (quiver.reverse f).to_path)
 
 /-- The underlying vertices of the free groupoid -/
-def _root_.category_theory.free_groupoid (V) [Q : quiver.{v+1} V] := quotient (@red_step V Q)
+def _root_.category_theory.free_groupoid (V) [Q : quiver V] := quotient (@red_step V Q)
 
-instance {V} [Q : quiver.{v+1} V] [h : nonempty V] : nonempty (free_groupoid V) := ⟨⟨h.some⟩⟩
+instance {V} [Q : quiver V] [h : nonempty V] : nonempty (free_groupoid V) := ⟨⟨h.some⟩⟩
 
 lemma congr_reverse {X Y : paths $ quiver.symmetrify V} (p q : X ⟶ Y) :
   quotient.comp_closure red_step p q →
@@ -132,7 +130,7 @@ instance : groupoid (free_groupoid V) :=
   comp_inv' := λ X Y p, quot.induction_on p $ λ pp, congr_comp_reverse pp }
 
 /-- The inclusion of the quiver on `V` to the underlying quiver on `free_groupoid V`-/
-def of (V) [quiver.{v+1} V] : prefunctor V (free_groupoid V) :=
+def of (V) [quiver V] : prefunctor V (free_groupoid V) :=
 { obj := λ X, ⟨X⟩,
   map := λ X Y f, quot.mk _ f.to_pos_path }
 
@@ -175,7 +173,7 @@ begin
   apply quiver.symmetrify.lift_unique,
   { rw ←functor.to_prefunctor_comp, exact hΦ, },
   { rintros X Y f,
-    simp [←functor.to_prefunctor_comp,prefunctor.comp_map, paths.of_map, inv_eq_inv],
+    simp only [←functor.to_prefunctor_comp,prefunctor.comp_map, paths.of_map, inv_eq_inv],
     change Φ.map (inv ((quotient.functor red_step).to_prefunctor.map f.to_path)) =
            inv (Φ.map ((quotient.functor red_step).to_prefunctor.map f.to_path)),
     have := functor.map_inv Φ ((quotient.functor red_step).to_prefunctor.map f.to_path),

src/category_theory/groupoid/subgroupoid.lean

@@ -11,6 +11,7 @@ import algebra.hom.equiv
 import data.set.lattice
 import combinatorics.quiver.connected_component
 import group_theory.subgroup.basic
+import order.galois_connection
 /-!
 # Subgroupoid
 
@@ -80,9 +81,47 @@ namespace subgroupoid
 
 variable (S : subgroupoid C)
 
+lemma inv_mem_iff {c d : C} (f : c ⟶ d) : inv f ∈ S.arrows d c ↔ f ∈ S.arrows c d :=
+begin
+  split,
+  { rintro h,
+    suffices : inv (inv f) ∈ S.arrows c d,
+    { simpa only [inv_eq_inv, is_iso.inv_inv] using this, },
+    { apply S.inv h, }, },
+  { apply S.inv, },
+end
+
+lemma mul_mem_cancel_left {c d e : C} {f : c ⟶ d} {g : d ⟶ e} (hf : f ∈ S.arrows c d) :
+  f ≫ g ∈ S.arrows c e ↔ g ∈ S.arrows d e :=
+begin
+  split,
+  { rintro h,
+    suffices : (inv f) ≫ f ≫ g ∈ S.arrows d e,
+    { simpa only [inv_eq_inv, is_iso.inv_hom_id_assoc] using this, },
+    { apply S.mul (S.inv hf) h, }, },
+  { apply S.mul hf, },
+end
+
+lemma mul_mem_cancel_right {c d e : C} {f : c ⟶ d} {g : d ⟶ e} (hg : g ∈ S.arrows d e) :
+  f ≫ g ∈ S.arrows c e ↔ f ∈ S.arrows c d :=
+begin
+  split,
+  { rintro h,
+    suffices : (f ≫ g) ≫ (inv g) ∈ S.arrows c d,
+    { simpa only [inv_eq_inv, is_iso.hom_inv_id, category.comp_id, category.assoc] using this, },
+    { apply S.mul h (S.inv hg), }, },
+  { exact λ hf, S.mul hf hg, },
+end
+
 /-- The vertices of `C` on which `S` has non-trivial isotropy -/
 def objs : set C := {c : C | (S.arrows c c).nonempty}
 
+lemma mem_objs_of_src {c d : C} {f : c ⟶ d} (h : f ∈ S.arrows c d) : c ∈ S.objs :=
+⟨f ≫ inv f, S.mul h (S.inv h)⟩
+
+lemma mem_objs_of_tgt {c d : C} {f : c ⟶ d} (h : f ∈ S.arrows c d) : d ∈ S.objs :=
+⟨(inv f) ≫ f, S.mul (S.inv h) h⟩
+
 lemma id_mem_of_nonempty_isotropy (c : C) :
   c ∈ objs S → 𝟙 c ∈ S.arrows c c :=
 begin
@@ -91,10 +130,17 @@ begin
   simp only [inv_eq_inv, is_iso.hom_inv_id],
 end
 
+lemma id_mem_of_src {c d : C} {f : c ⟶ d} (h : f ∈ S.arrows c d) : (𝟙 c) ∈ S.arrows c c :=
+id_mem_of_nonempty_isotropy S c (mem_objs_of_src S h)
+
+lemma id_mem_of_tgt {c d : C} {f : c ⟶ d} (h : f ∈ S.arrows c d) : (𝟙 d) ∈ S.arrows d d :=
+id_mem_of_nonempty_isotropy S d (mem_objs_of_tgt S h)
+
 /-- A subgroupoid seen as a quiver on vertex set `C` -/
 def as_wide_quiver : quiver C := ⟨λ c d, subtype $ S.arrows c d⟩
 
 /-- The coercion of a subgroupoid as a groupoid -/
+@[simps to_category_comp_coe, simps inv_coe (lemmas_only)]
 instance coe : groupoid S.objs :=
 { hom := λ a b, S.arrows a.val b.val,
   id := λ a, ⟨𝟙 a.val, id_mem_of_nonempty_isotropy S a.val a.prop⟩,
@@ -106,6 +152,10 @@ instance coe : groupoid S.objs :=
   inv_comp' := λ a b ⟨p,hp⟩, by simp only [inv_comp],
   comp_inv' := λ a b ⟨p,hp⟩, by simp only [comp_inv] }
 
+@[simp] lemma coe_inv_coe' {c d : S.objs} (p : c ⟶ d) :
+  (category_theory.inv p).val = category_theory.inv p.val := by
+{ simp only [subtype.val_eq_coe, ←inv_eq_inv, coe_inv_coe], }
+
 /-- The embedding of the coerced subgroupoid to its parent-/
 def hom : S.objs ⥤ C :=
 { obj := λ c, c.val,
@@ -142,6 +192,11 @@ instance : has_top (subgroupoid C) :=
     mul    := by { rintros, trivial, },
     inv    := by { rintros, trivial, } } ⟩
 
+lemma mem_top {c d : C} (f : c ⟶ d) : f ∈ (⊤ : subgroupoid C).arrows c d := trivial
+
+lemma mem_top_objs (c : C) : c ∈ (⊤ : subgroupoid C).objs :=
+by { dsimp [has_top.top,objs], simp only [univ_nonempty], }
+
 instance : has_bot (subgroupoid C) :=
 ⟨ { arrows := (λ _ _, ∅),
     mul    := λ _ _ _ _, false.elim,
@@ -218,10 +273,31 @@ lemma mem_discrete_iff {c d : C} (f : c ⟶ d):
   (f ∈ (discrete).arrows c d) ↔ (∃ (h : c = d), f = eq_to_hom h) :=
 ⟨by { rintro ⟨⟩, exact ⟨rfl, rfl⟩ }, by { rintro ⟨rfl, rfl⟩, split }⟩
 
-/-- A subgroupoid is normal if it is “wide” (meaning that its carrier set is all of `C`)
-    and satisfies the expected stability under conjugacy. -/
-structure is_normal : Prop :=
+/-- A subgroupoid is wide if its carrier set is all of `C`-/
+structure is_wide : Prop :=
 (wide : ∀ c, (𝟙 c) ∈ (S.arrows c c))
+
+lemma is_wide_iff_objs_eq_univ : S.is_wide ↔ S.objs = set.univ :=
+begin
+  split,
+  { rintro h,
+    ext, split; simp only [top_eq_univ, mem_univ, implies_true_iff, forall_true_left],
+    apply mem_objs_of_src S (h.wide x), },
+  { rintro h,
+    refine ⟨λ c, _⟩,
+    obtain ⟨γ,γS⟩ := (le_of_eq h.symm : ⊤ ⊆ S.objs) (set.mem_univ c),
+    exact id_mem_of_src S γS, },
+end
+
+lemma is_wide.id_mem {S : subgroupoid C} (Sw : S.is_wide) (c : C) :
+  (𝟙 c) ∈ S.arrows c c := Sw.wide c
+
+lemma is_wide.eq_to_hom_mem {S : subgroupoid C} (Sw : S.is_wide) {c d : C} (h : c = d) :
+  (eq_to_hom h) ∈ S.arrows c d := by
+{ cases h, simp only [eq_to_hom_refl], apply Sw.id_mem c, }
+
+/-- A subgroupoid is normal if it is wide and satisfies the expected stability under conjugacy. -/
+structure is_normal extends (is_wide S) : Prop :=
 (conj : ∀ {c d} (p : c ⟶ d) {γ : c ⟶ c} (hs : γ ∈ S.arrows c c),
               ((inv p) ≫ γ ≫ p) ∈ (S.arrows d d))
 
@@ -247,6 +323,11 @@ lemma Inf_is_normal (s : set $ subgroupoid C) (sn : ∀ S ∈ s, is_normal S) :
 { wide := by { simp_rw [Inf, mem_Inter₂], exact λ c S Ss, (sn S Ss).wide c },
   conj := by { simp_rw [Inf, mem_Inter₂], exact λ c d p γ hγ S Ss, (sn S Ss).conj p (hγ S Ss) } }
 
+lemma discrete_is_normal : (@discrete C _).is_normal :=
+{ wide := λ c, by { constructor, },
+  conj := λ c d f γ hγ, by
+  { cases hγ, simp only [inv_eq_inv, category.id_comp, is_iso.inv_hom_id], constructor, } }
+
 lemma is_normal.vertex_subgroup (Sn : is_normal S) (c : C) (cS : c ∈ S.objs) :
   (S.vertex_subgroup cS).normal :=
 { conj_mem := λ x hx y, by { rw mul_assoc, exact Sn.conj' y hx } }
@@ -260,13 +341,39 @@ variable (X : ∀ c d : C, set (c ⟶ d))
 def generated : subgroupoid C :=
 Inf {S : subgroupoid C | ∀ c d, X c d ⊆ S.arrows c d}
 
+lemma subset_generated (c d : C) : X c d ⊆ (generated X).arrows c d :=
+begin
+  dsimp only [generated, Inf],
+  simp only [subset_Inter₂_iff],
+  exact λ S hS f fS, hS _ _ fS,
+end
+
 /-- The normal sugroupoid generated by the set of arrows `X` -/
 def generated_normal : subgroupoid C :=
 Inf {S : subgroupoid C | (∀ c d, X c d ⊆ S.arrows c d) ∧ S.is_normal}
 
+lemma generated_le_generated_normal : generated X ≤ generated_normal X :=
+begin
+  apply @Inf_le_Inf (subgroupoid C) _,
+  exact λ S ⟨h,_⟩, h,
+end
+
 lemma generated_normal_is_normal : (generated_normal X).is_normal :=
 Inf_is_normal _ (λ S h, h.right)
 
+lemma is_normal.generated_normal_le {S : subgroupoid C} (Sn : S.is_normal) :
+  generated_normal X ≤ S ↔ ∀ c d, X c d ⊆ S.arrows c d :=
+begin
+  split,
+  { rintro h c d,
+    let h' := generated_le_generated_normal X,
+    rw le_iff at h h',
+    exact ((subset_generated X c d).trans (@h' c d)).trans (@h c d), },
+  { rintro h,
+    apply @Inf_le (subgroupoid C) _,
+    exact ⟨h,Sn⟩, },
+end
+
 end generated_subgroupoid
 
 section hom
@@ -291,11 +398,12 @@ lemma comap_mono (S T : subgroupoid D) :
 
 lemma is_normal_comap {S : subgroupoid D} (Sn : is_normal S) : is_normal (comap φ S) :=
 { wide := λ c, by { rw [comap, mem_set_of, functor.map_id], apply Sn.wide, },
-  conj := λ c d f γ hγ, begin
-    simp only [comap, mem_set_of, functor.map_comp, functor.map_inv, inv_eq_inv],
-    rw [←inv_eq_inv],
-    exact Sn.conj _ hγ,
-  end }
+  conj := λ c d f γ hγ, by
+  { simp_rw [inv_eq_inv f, comap, mem_set_of, functor.map_comp, functor.map_inv, ←inv_eq_inv],
+    exact Sn.conj _ hγ, } }
+
+@[simp] lemma comap_comp {E : Type*} [groupoid E] (ψ : D ⥤ E) :
+  comap (φ ⋙ ψ) = (comap φ) ∘ (comap ψ) := rfl
 
 /-- The kernel of a functor between subgroupoid is the preimage. -/
 def ker : subgroupoid C := comap φ discrete
@@ -304,12 +412,17 @@ lemma mem_ker_iff {c d : C} (f : c ⟶ d) :
   f ∈ (ker φ).arrows c d ↔ ∃ (h : φ.obj c = φ.obj d), φ.map f = eq_to_hom h :=
 mem_discrete_iff (φ.map f)
 
+lemma ker_is_normal : (ker φ).is_normal := is_normal_comap φ (discrete_is_normal)
+
+@[simp]
+lemma ker_comp {E : Type*} [groupoid E] (ψ : D ⥤ E) : ker (φ ⋙ ψ) = comap φ (ker ψ) := rfl
+
 /-- The family of arrows of the image of a subgroupoid under a functor injective on objects -/
 inductive map.arrows (hφ : function.injective φ.obj) (S : subgroupoid C) :
   Π (c d : D), (c ⟶ d) → Prop
 | im {c d : C} (f : c ⟶ d) (hf : f ∈ S.arrows c d) : map.arrows (φ.obj c) (φ.obj d) (φ.map f)
 
-lemma map.mem_arrows_iff (hφ : function.injective φ.obj) (S : subgroupoid C) {c d : D} (f : c ⟶ d):
+lemma map.arrows_iff (hφ : function.injective φ.obj) (S : subgroupoid C) {c d : D} (f : c ⟶ d) :
   map.arrows φ hφ S c d f ↔
   ∃ (a b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d) (hg : g ∈ S.arrows a b),
     f = (eq_to_hom ha.symm) ≫ φ.map g ≫ (eq_to_hom hb) :=
@@ -329,14 +442,55 @@ def map (hφ : function.injective φ.obj) (S : subgroupoid C) : subgroupoid D :=
   end,
   mul := begin
     rintro _ _ _ _ ⟨f,hf⟩ q hq,
-    obtain ⟨c₃,c₄,g,he,rfl,hg,gq⟩ := (map.mem_arrows_iff φ hφ S q).mp hq,
+    obtain ⟨c₃,c₄,g,he,rfl,hg,gq⟩ := (map.arrows_iff φ hφ S q).mp hq,
     cases hφ he, rw [gq, ← eq_conj_eq_to_hom, ← φ.map_comp],
     split, exact S.mul hf hg,
   end }
 
+lemma mem_map_iff (hφ : function.injective φ.obj) (S : subgroupoid C) {c d : D} (f : c ⟶ d) :
+  f ∈ (map φ hφ S).arrows c d ↔
+  ∃ (a b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d) (hg : g ∈ S.arrows a b),
+    f = (eq_to_hom ha.symm) ≫ φ.map g ≫ (eq_to_hom hb) := map.arrows_iff φ hφ S f
+
+lemma galois_connection_map_comap (hφ : function.injective φ.obj) :
+  galois_connection (map φ hφ) (comap φ) :=
+begin
+  rintro S T, simp_rw [le_iff], split,
+  { exact λ h c d f fS, h (map.arrows.im f fS), },
+  { rintros h _ _ g ⟨a,gφS⟩,
+    exact h gφS, },
+end
+
 lemma map_mono (hφ : function.injective φ.obj) (S T : subgroupoid C) :
   S ≤ T → map φ hφ S ≤ map φ hφ T :=
-by { rintro ST ⟨c,d,f⟩ ⟨_,h⟩, split, exact @ST ⟨_,_,_⟩ h }
+λ h, (galois_connection_map_comap φ hφ).monotone_l h
+
+lemma le_comap_map (hφ : function.injective φ.obj) (S : subgroupoid C) :
+  S ≤ comap φ (map φ hφ S) := (galois_connection_map_comap φ hφ).le_u_l S
+
+lemma map_comap_le (hφ : function.injective φ.obj) (T : subgroupoid D) :
+  map φ hφ (comap φ T) ≤ T := (galois_connection_map_comap φ hφ).l_u_le T
+
+lemma map_le_iff_le_comap (hφ : function.injective φ.obj)
+  (S : subgroupoid C) (T : subgroupoid D) :
+  map φ hφ S ≤ T ↔ S ≤ comap φ T := (galois_connection_map_comap φ hφ).le_iff_le
+
+lemma mem_map_objs_iff (hφ : function.injective φ.obj) (d : D) :
+  d ∈ (map φ hφ S).objs ↔ ∃ c ∈ S.objs, φ.obj c = d :=
+begin
+  dsimp [objs, map],
+  split,
+  { rintro ⟨f,hf⟩,
+    change map.arrows φ hφ S d d f at hf, rw map.arrows_iff at hf,
+    obtain ⟨c,d,g,ec,ed,eg,gS,eg⟩ := hf,
+    exact ⟨c, ⟨mem_objs_of_src S eg, ec⟩⟩, },
+  { rintros ⟨c,⟨γ,γS⟩,rfl⟩,
+    exact ⟨φ.map γ,⟨γ,γS⟩⟩, }
+end
+
+@[simp]
+lemma map_objs_eq (hφ : function.injective φ.obj) : (map φ hφ S).objs = φ.obj '' S.objs := by
+{ ext, convert mem_map_objs_iff S φ hφ x, simp only [mem_image, exists_prop], }
 
 /-- The image of a functor injective on objects -/
 def im (hφ : function.injective φ.obj) := map φ hφ (⊤)
@@ -345,7 +499,41 @@ lemma mem_im_iff (hφ : function.injective φ.obj) {c d : D} (f : c ⟶ d) :
   f ∈ (im φ hφ).arrows c d ↔
   ∃ (a b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d),
     f = (eq_to_hom ha.symm) ≫ φ.map g ≫ (eq_to_hom hb) :=
-by { convert map.mem_arrows_iff φ hφ ⊤ f, simp only [has_top.top, mem_univ, exists_true_left] }
+by { convert map.arrows_iff φ hφ ⊤ f, simp only [has_top.top, mem_univ, exists_true_left] }
+
+lemma mem_im_objs_iff (hφ : function.injective φ.obj) (d : D) :
+  d ∈ (im φ hφ).objs ↔ ∃ c : C, φ.obj c = d := by
+{ simp only [im, mem_map_objs_iff, mem_top_objs, exists_true_left], }
+
+lemma obj_surjective_of_im_eq_top (hφ : function.injective φ.obj) (hφ' : im φ hφ = ⊤) :
+  function.surjective φ.obj :=
+begin
+  rintro d,
+  rw [←mem_im_objs_iff, hφ'],
+  apply mem_top_objs,
+end
+
+lemma is_normal_map (hφ : function.injective φ.obj) (hφ' : im φ hφ = ⊤) (Sn : S.is_normal) :
+  (map φ hφ S).is_normal :=
+{ wide := λ d, by
+  { obtain ⟨c,rfl⟩ := obj_surjective_of_im_eq_top φ hφ hφ' d,
+    change map.arrows φ hφ S _ _ (𝟙 _), rw ←functor.map_id,
+    constructor, exact Sn.wide c, },
+  conj := λ d d' g δ hδ, by
+  { rw mem_map_iff at hδ,
+    obtain ⟨c,c',γ,cd,cd',γS,hγ⟩ := hδ, subst_vars, cases hφ cd',
+    have : d' ∈ (im φ hφ).objs, by { rw hφ', apply mem_top_objs, },
+    rw mem_im_objs_iff at this,
+    obtain ⟨c',rfl⟩ := this,
+    have : g ∈ (im φ hφ).arrows (φ.obj c) (φ.obj c'), by
+    { rw hφ', trivial, },
+    rw mem_im_iff at this,
+    obtain ⟨b,b',f,hb,hb',_,hf⟩ := this, subst_vars, cases hφ hb, cases hφ hb',
+    change map.arrows φ hφ S (φ.obj c') (φ.obj c') _,
+    simp only [eq_to_hom_refl, category.comp_id, category.id_comp, inv_eq_inv],
+    suffices : map.arrows φ hφ S (φ.obj c') (φ.obj c') (φ.map $ inv f ≫ γ ≫ f),
+    { simp only [inv_eq_inv, functor.map_comp, functor.map_inv] at this, exact this, },
+    { constructor, apply Sn.conj f γS, } } }
 
 end hom