feat(combinatorics/quiver/*): More edge reversal constructions (#17665)

bottine · bottine · commit 706d88f2b8fd · 2022-12-17T06:45:00.000Z
Move 

* `quiver.symmetrify`,
* `quiver.has_reverse`,
* `quiver.has_involutive_reverse`,
* `quiver.reverse`,
* `quiver.path.reverse`,
* `quiver.symmetrify.of`,
* `quiver.lift`,
* associated lemmas,

from `combinatorics/quiver/connected_component.lean` to `combinatorics/quiver/symmetrify.lean`. 

Add

* the class `prefunctor.map_reverse` witnessing that a prefunctor maps reverses to reverses, and change the lemmas taking this property as an explicit argument.
* `prefunctor.symmetrify` mapping a prefunctor to the prefunctor between symmetrifications,
* associated lemmas,

to `combinatorics/quiver/symmetrify.lean`.

Move `quiver.hom.to_pos` and `quiver.hom.to_neg` from `category_theory/groupoid/free_groupoid.lean` to `combinatorics/quiver/symmetrify.lean`.

Add `map_reverse` instance for functors between groupoids.



Co-authored-by: Rémi Bottinelli &lt;bottine@users.noreply.github.com&gt;
diff --git a/src/category_theory/groupoid.lean b/src/category_theory/groupoid.lean
@@ -75,6 +75,12 @@ instance groupoid_has_involutive_reverse : quiver.has_involutive_reverse C :=
 
 @[simp] lemma groupoid.reverse_eq_inv (f : X ⟶ Y) : quiver.reverse f = groupoid.inv f := rfl
 
+instance functor_map_reverse {D : Type*} [groupoid D] (F : C ⥤ D) :
+  F.to_prefunctor.map_reverse :=
+{ map_reverse' := λ X Y f, by
+  simp only [quiver.reverse, quiver.has_reverse.reverse', groupoid.inv_eq_inv,
+               functor.to_prefunctor_map, functor.map_inv], }
+
 variables (X Y)
 
 /-- In a groupoid, isomorphisms are equivalent to morphisms. -/
diff --git a/src/category_theory/groupoid/free_groupoid.lean b/src/category_theory/groupoid/free_groupoid.lean
@@ -9,6 +9,7 @@ import category_theory.groupoid
 import tactic.nth_rewrite
 import category_theory.path_category
 import category_theory.quotient
+import combinatorics.quiver.symmetric
 
 /-!
 # Free groupoid on a quiver
@@ -45,14 +46,6 @@ universes u v u' v' u'' v''
 
 variables {V : Type u} [quiver.{v+1} V]
 
-/-- Shorthand for the "forward" arrow corresponding to `f` in `symmetrify V` -/
-abbreviation quiver.hom.to_pos {X Y : V} (f : X ⟶ Y) :
-  (quiver.symmetrify_quiver V).hom X Y := sum.inl f
-
-/-- Shorthand for the "backward" arrow corresponding to `f` in `symmetrify V` -/
-abbreviation quiver.hom.to_neg {X Y : V} (f : X ⟶ Y) :
-  (quiver.symmetrify_quiver V).hom Y X := sum.inr f
-
 /-- Shorthand for the "forward" arrow corresponding to `f` in `paths $ symmetrify V` -/
 abbreviation quiver.hom.to_pos_path {X Y : V} (f : X ⟶ Y) :
   ((category_theory.paths.category_paths $ quiver.symmetrify V).hom X Y) := f.to_pos.to_path
@@ -168,9 +161,9 @@ lemma lift_unique (φ : V ⥤q V') (Φ : free_groupoid V ⥤ V')
 begin
   apply quotient.lift_unique,
   apply paths.lift_unique,
-  apply quiver.symmetrify.lift_unique,
+  fapply @quiver.symmetrify.lift_unique _ _ _ _ _ _ _ _ _,
   { rw ←functor.to_prefunctor_comp, exact hΦ, },
-  { rintros X Y f,
+  { constructor, rintros X Y f,
     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)),
diff --git a/src/combinatorics/quiver/connected_component.lean b/src/combinatorics/quiver/connected_component.lean
@@ -5,129 +5,26 @@ Authors: David Wärn
 -/
 import combinatorics.quiver.subquiver
 import combinatorics.quiver.path
-import data.sum.basic
-
+import combinatorics.quiver.symmetric
 /-!
 ## Weakly connected components
 
 > THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
 > https://github.com/leanprover-community/mathlib4/pull/836
 > Any changes to this file require a corresponding PR to mathlib4.
 
-For a quiver `V`, we build a quiver `symmetrify V` by adding a reversal of every edge.
-Informally, a path in `symmetrify V` corresponds to a 'zigzag' in `V`. This lets us
-define the type `weakly_connected_component V` as the quotient of `V` by the relation which
-identifies `a` with `b` if there is a path from `a` to `b` in `symmetrify V`. (These
-zigzags can be seen as a proof-relevant analogue of `eqv_gen`.)
+
+For a quiver `V`, we define the type `weakly_connected_component V` as the quotient of `V`
+by the relation which identifies `a` with `b` if there is a path from `a` to `b` in `symmetrify V`.
+(These zigzags can be seen as a proof-relevant analogue of `eqv_gen`.)
 
 Strongly connected components have not yet been defined.
 -/
-universes v u
+universes u
 
 namespace quiver
 
-/-- A type synonym for the symmetrized quiver (with an arrow both ways for each original arrow).
-    NB: this does not work for `Prop`-valued quivers. It requires `[quiver.{v+1} V]`. -/
-@[nolint has_nonempty_instance]
-def symmetrify (V) : Type u := V
-
-instance symmetrify_quiver (V : Type u) [quiver V] : quiver (symmetrify V) :=
-⟨λ a b : V, (a ⟶ b) ⊕ (b ⟶ a)⟩
-
-variables (V : Type u) [quiver.{v+1} V]
-
-/-- A quiver `has_reverse` if we can reverse an arrow `p` from `a` to `b` to get an arrow
-    `p.reverse` from `b` to `a`.-/
-class has_reverse :=
-(reverse' : Π {a b : V}, (a ⟶ b) → (b ⟶ a))
-
-/-- Reverse the direction of an arrow. -/
-def reverse {V} [quiver.{v+1} V] [has_reverse V] {a b : V} : (a ⟶ b) → (b ⟶ a) :=
-  has_reverse.reverse'
-
-/-- A quiver `has_involutive_reverse` if reversing twice is the identity.`-/
-class has_involutive_reverse extends has_reverse V :=
-(inv' : Π {a b : V} (f : a ⟶ b), reverse (reverse f) = f)
-
-@[simp] lemma reverse_reverse {V} [quiver.{v+1} V] [h : has_involutive_reverse V]
-  {a b : V} (f : a ⟶ b) : reverse (reverse f) = f := by apply h.inv'
-
-variables {V}
-
-instance : has_reverse (symmetrify V) := ⟨λ a b e, e.swap⟩
-instance : has_involutive_reverse (symmetrify V) :=
-{ to_has_reverse := ⟨λ a b e, e.swap⟩,
-  inv' := λ a b e, congr_fun sum.swap_swap_eq e }
-
-
-/-- Reverse the direction of a path. -/
-@[simp] def path.reverse [has_reverse V] {a : V} : Π {b}, path a b → path b a
-| a path.nil := path.nil
-| b (path.cons p e) := (reverse e).to_path.comp p.reverse
-
-@[simp] lemma path.reverse_to_path [has_reverse V] {a b : V} (f : a ⟶ b) :
-  f.to_path.reverse = (reverse f).to_path := rfl
-
-@[simp] lemma path.reverse_comp [has_reverse V] {a b c : V} (p : path a b) (q : path b c) :
-  (p.comp q).reverse = q.reverse.comp p.reverse := by
-{ induction q, { simp, }, { simp [q_ih], }, }
-
-@[simp] lemma path.reverse_reverse [h : has_involutive_reverse V] {a b : V} (p : path a b) :
-  p.reverse.reverse = p := by
-{ induction p,
-  { simp, },
-  { simp only [path.reverse, path.reverse_comp, path.reverse_to_path, reverse_reverse, p_ih],
-    refl, }, }
-
-/-- The inclusion of a quiver in its symmetrification -/
-def symmetrify.of : prefunctor V (symmetrify V) :=
-{ obj := id,
-  map := λ X Y f, sum.inl f }
-
-/-- Given a quiver `V'` with reversible arrows, a prefunctor to `V'` can be lifted to one from
-    `symmetrify V` to `V'` -/
-def symmetrify.lift {V' : Type*} [quiver V'] [has_reverse V'] (φ : prefunctor V V') :
-  prefunctor (symmetrify V) V' :=
-{ obj := φ.obj,
-  map := λ X Y f, sum.rec (λ fwd, φ.map fwd) (λ bwd, reverse (φ.map bwd)) f }
-
-lemma symmetrify.lift_spec  (V' : Type*) [quiver V'] [has_reverse V'] (φ : prefunctor V V') :
-  symmetrify.of.comp (symmetrify.lift φ) = φ :=
-begin
-  fapply prefunctor.ext,
-  { rintro X, refl, },
-  { rintros X Y f, refl, },
-end
-
-lemma symmetrify.lift_reverse  (V' : Type*) [quiver V'] [h : has_involutive_reverse V']
-  (φ : prefunctor V V')
-  {X Y : symmetrify V} (f : X ⟶ Y) :
-  (symmetrify.lift φ).map (quiver.reverse f) = quiver.reverse ((symmetrify.lift φ).map f) :=
-begin
-  dsimp [symmetrify.lift], cases f,
-  { simp only, refl, },
-  { simp only, rw h.inv', refl, }
-end
-
-/-- `lift φ` is the only prefunctor extending `φ` and preserving reverses. -/
-lemma symmetrify.lift_unique (V' : Type*) [quiver V'] [has_reverse V']
-  (φ : prefunctor V V')
-  (Φ : prefunctor (symmetrify V) V')
-  (hΦ : symmetrify.of.comp Φ = φ)
-  (hΦinv : ∀ {X Y : V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)) :
-  Φ = symmetrify.lift φ :=
-begin
-  subst_vars,
-  fapply prefunctor.ext,
-  { rintro X, refl, },
-  { rintros X Y f,
-    cases f,
-    { refl, },
-    { dsimp [symmetrify.lift,symmetrify.of],
-      convert hΦinv (sum.inl f), }, },
-end
-
-variables (V)
+variables (V : Type*) [quiver.{u+1} V]
 
 /-- Two vertices are related in the zigzag setoid if there is a
     zigzag of arrows from one to the other. -/
diff --git a/src/combinatorics/quiver/push.lean b/src/combinatorics/quiver/push.lean
@@ -21,6 +21,8 @@ universes v v₁ v₂ u u₁ u₂
 
 variables {V : Type*} [quiver V] {W : Type*} (σ : V → W)
 
+namespace quiver
+
 /-- The `quiver` instance obtained by pushing arrows of `V` along the map `σ : V → W` -/
 @[nolint unused_arguments]
 def push (σ : V → W) := W
@@ -80,3 +82,5 @@ begin
 end
 
 end push
+
+end quiver
diff --git a/src/combinatorics/quiver/symmetric.lean b/src/combinatorics/quiver/symmetric.lean
