bump to nightly-2023-08-13-09

mathlib commit leanprover-community/mathlib@32a7e53

Mathbin/Combinatorics/Quiver/Covering.lean

@@ -49,119 +49,156 @@ universe u v w
 variable {U : Type _} [Quiver.{u + 1} U] {V : Type _} [Quiver.{v + 1} V] (φ : U ⥤q V) {W : Type _}
   [Quiver.{w + 1} W] (ψ : V ⥤q W)
 
+#print Quiver.Star /-
 /-- The `quiver.star` at a vertex is the collection of arrows whose source is the vertex.
 The type `quiver.star u` is defined to be `Σ (v : U), (u ⟶ v)`. -/
 @[reducible]
 def Quiver.Star (u : U) :=
   Σ v : U, u ⟶ v
 #align quiver.star Quiver.Star
+-/
 
+#print Quiver.Star.mk /-
 /-- Constructor for `quiver.star`. Defined to be `sigma.mk`. -/
 @[reducible]
 protected def Quiver.Star.mk {u v : U} (f : u ⟶ v) : Quiver.Star u :=
   ⟨_, f⟩
 #align quiver.star.mk Quiver.Star.mk
+-/
 
+#print Quiver.Costar /-
 /-- The `quiver.costar` at a vertex is the collection of arrows whose target is the vertex.
 The type `quiver.costar v` is defined to be `Σ (u : U), (u ⟶ v)`. -/
 @[reducible]
 def Quiver.Costar (v : U) :=
   Σ u : U, u ⟶ v
 #align quiver.costar Quiver.Costar
+-/
 
+#print Quiver.Costar.mk /-
 /-- Constructor for `quiver.costar`. Defined to be `sigma.mk`. -/
 @[reducible]
 protected def Quiver.Costar.mk {u v : U} (f : u ⟶ v) : Quiver.Costar v :=
   ⟨_, f⟩
 #align quiver.costar.mk Quiver.Costar.mk
+-/
 
+#print Prefunctor.star /-
 /-- A prefunctor induces a map of `quiver.star` at every vertex. -/
 @[simps]
 def Prefunctor.star (u : U) : Quiver.Star u → Quiver.Star (φ.obj u) := fun F =>
   Quiver.Star.mk (φ.map F.2)
 #align prefunctor.star Prefunctor.star
+-/
 
+#print Prefunctor.costar /-
 /-- A prefunctor induces a map of `quiver.costar` at every vertex. -/
 @[simps]
 def Prefunctor.costar (u : U) : Quiver.Costar u → Quiver.Costar (φ.obj u) := fun F =>
   Quiver.Costar.mk (φ.map F.2)
 #align prefunctor.costar Prefunctor.costar
+-/
 
+#print Prefunctor.star_apply /-
 @[simp]
 theorem Prefunctor.star_apply {u v : U} (e : u ⟶ v) :
     φ.unit u (Quiver.Star.mk e) = Quiver.Star.mk (φ.map e) :=
   rfl
 #align prefunctor.star_apply Prefunctor.star_apply
+-/
 
+#print Prefunctor.costar_apply /-
 @[simp]
 theorem Prefunctor.costar_apply {u v : U} (e : u ⟶ v) :
     φ.Costar v (Quiver.Costar.mk e) = Quiver.Costar.mk (φ.map e) :=
   rfl
 #align prefunctor.costar_apply Prefunctor.costar_apply
+-/
 
+#print Prefunctor.star_comp /-
 theorem Prefunctor.star_comp (u : U) : (φ ⋙q ψ).unit u = ψ.unit (φ.obj u) ∘ φ.unit u :=
   rfl
 #align prefunctor.star_comp Prefunctor.star_comp
+-/
 
+#print Prefunctor.costar_comp /-
 theorem Prefunctor.costar_comp (u : U) : (φ ⋙q ψ).Costar u = ψ.Costar (φ.obj u) ∘ φ.Costar u :=
   rfl
 #align prefunctor.costar_comp Prefunctor.costar_comp
+-/
 
+#print Prefunctor.IsCovering /-
 /-- A prefunctor is a covering of quivers if it defines bijections on all stars and costars. -/
 protected structure Prefunctor.IsCovering : Prop where
   star_bijective : ∀ u, Bijective (φ.unit u)
   costar_bijective : ∀ u, Bijective (φ.Costar u)
 #align prefunctor.is_covering Prefunctor.IsCovering
+-/
 
+#print Prefunctor.IsCovering.map_injective /-
 @[simp]
 theorem Prefunctor.IsCovering.map_injective (hφ : φ.IsCovering) {u v : U} :
     Injective fun f : u ⟶ v => φ.map f := by
   rintro f g he
   have : φ.star u (Quiver.Star.mk f) = φ.star u (Quiver.Star.mk g) := by simpa using he
   simpa using (hφ.star_bijective u).left this
 #align prefunctor.is_covering.map_injective Prefunctor.IsCovering.map_injective
+-/
 
+#print Prefunctor.IsCovering.comp /-
 theorem Prefunctor.IsCovering.comp (hφ : φ.IsCovering) (hψ : ψ.IsCovering) : (φ ⋙q ψ).IsCovering :=
   ⟨fun u => (hψ.star_bijective _).comp (hφ.star_bijective _), fun u =>
     (hψ.costar_bijective _).comp (hφ.costar_bijective _)⟩
 #align prefunctor.is_covering.comp Prefunctor.IsCovering.comp
+-/
 
+#print Prefunctor.IsCovering.of_comp_right /-
 theorem Prefunctor.IsCovering.of_comp_right (hψ : ψ.IsCovering) (hφψ : (φ ⋙q ψ).IsCovering) :
     φ.IsCovering :=
   ⟨fun u => (Bijective.of_comp_iff' (hψ.star_bijective _) _).mp (hφψ.star_bijective _), fun u =>
     (Bijective.of_comp_iff' (hψ.costar_bijective _) _).mp (hφψ.costar_bijective _)⟩
 #align prefunctor.is_covering.of_comp_right Prefunctor.IsCovering.of_comp_right
+-/
 
+#print Prefunctor.IsCovering.of_comp_left /-
 theorem Prefunctor.IsCovering.of_comp_left (hφ : φ.IsCovering) (hφψ : (φ ⋙q ψ).IsCovering)
     (φsur : Surjective φ.obj) : ψ.IsCovering :=
   by
   refine' ⟨fun v => _, fun v => _⟩ <;> obtain ⟨u, rfl⟩ := φsur v
   exacts [(bijective.of_comp_iff _ (hφ.star_bijective u)).mp (hφψ.star_bijective u),
     (bijective.of_comp_iff _ (hφ.costar_bijective u)).mp (hφψ.costar_bijective u)]
 #align prefunctor.is_covering.of_comp_left Prefunctor.IsCovering.of_comp_left
+-/
 
+#print Quiver.symmetrifyStar /-
 /-- The star of the symmetrification of a quiver at a vertex `u` is equivalent to the sum of the
 star and the costar at `u` in the original quiver. -/
 def Quiver.symmetrifyStar (u : U) :
     Quiver.Star (Symmetrify.of.obj u) ≃ Sum (Quiver.Star u) (Quiver.Costar u) :=
   Equiv.sigmaSumDistrib _ _
 #align quiver.symmetrify_star Quiver.symmetrifyStar
+-/
 
+#print Quiver.symmetrifyCostar /-
 /-- The costar of the symmetrification of a quiver at a vertex `u` is equivalent to the sum of the
 costar and the star at `u` in the original quiver. -/
 def Quiver.symmetrifyCostar (u : U) :
     Quiver.Costar (Symmetrify.of.obj u) ≃ Sum (Quiver.Costar u) (Quiver.Star u) :=
   Equiv.sigmaSumDistrib _ _
 #align quiver.symmetrify_costar Quiver.symmetrifyCostar
+-/
 
+#print Prefunctor.symmetrifyStar /-
 theorem Prefunctor.symmetrifyStar (u : U) :
     φ.Symmetrify.unit u =
       (Quiver.symmetrifyStar _).symm ∘ Sum.map (φ.unit u) (φ.Costar u) ∘ Quiver.symmetrifyStar u :=
   by
   rw [Equiv.eq_symm_comp]
   ext ⟨v, f | g⟩ <;> simp [Quiver.symmetrifyStar]
 #align prefunctor.symmetrify_star Prefunctor.symmetrifyStar
+-/
 
+#print Prefunctor.symmetrifyCostar /-
 protected theorem Prefunctor.symmetrifyCostar (u : U) :
     φ.Symmetrify.Costar u =
       (Quiver.symmetrifyCostar _).symm ∘
@@ -170,37 +207,49 @@ protected theorem Prefunctor.symmetrifyCostar (u : U) :
   rw [Equiv.eq_symm_comp]
   ext ⟨v, f | g⟩ <;> simp [Quiver.symmetrifyCostar]
 #align prefunctor.symmetrify_costar Prefunctor.symmetrifyCostar
+-/
 
+#print Prefunctor.IsCovering.symmetrify /-
 protected theorem Prefunctor.IsCovering.symmetrify (hφ : φ.IsCovering) : φ.Symmetrify.IsCovering :=
   by
   refine' ⟨fun u => _, fun u => _⟩ <;>
     simp [φ.symmetrify_star, φ.symmetrify_costar, hφ.star_bijective u, hφ.costar_bijective u]
 #align prefunctor.is_covering.symmetrify Prefunctor.IsCovering.symmetrify
+-/
 
+#print Quiver.PathStar /-
 /-- The path star at a vertex `u` is the type of all paths starting at `u`.
 The type `quiver.path_star u` is defined to be `Σ v : U, path u v`. -/
 @[reducible]
 def Quiver.PathStar (u : U) :=
   Σ v : U, Path u v
 #align quiver.path_star Quiver.PathStar
+-/
 
+#print Quiver.PathStar.mk /-
 /-- Constructor for `quiver.path_star`. Defined to be `sigma.mk`. -/
 @[reducible]
 protected def Quiver.PathStar.mk {u v : U} (p : Path u v) : Quiver.PathStar u :=
   ⟨_, p⟩
 #align quiver.path_star.mk Quiver.PathStar.mk
+-/
 
+#print Prefunctor.pathStar /-
 /-- A prefunctor induces a map of path stars. -/
 def Prefunctor.pathStar (u : U) : Quiver.PathStar u → Quiver.PathStar (φ.obj u) := fun p =>
   Quiver.PathStar.mk (φ.mapPath p.2)
 #align prefunctor.path_star Prefunctor.pathStar
+-/
 
+#print Prefunctor.pathStar_apply /-
 @[simp]
 theorem Prefunctor.pathStar_apply {u v : U} (p : Path u v) :
     φ.PathStar u (Quiver.PathStar.mk p) = Quiver.PathStar.mk (φ.mapPath p) :=
   rfl
 #align prefunctor.path_star_apply Prefunctor.pathStar_apply
+-/
 
+#print Prefunctor.pathStar_injective /-
 theorem Prefunctor.pathStar_injective (hφ : ∀ u, Injective (φ.unit u)) (u : U) :
     Injective (φ.PathStar u) :=
   by
@@ -230,7 +279,9 @@ theorem Prefunctor.pathStar_injective (hφ : ∀ u, Injective (φ.unit u)) (u :
     cases hφ x₁ h_star
     rfl
 #align prefunctor.path_star_injective Prefunctor.pathStar_injective
+-/
 
+#print Prefunctor.pathStar_surjective /-
 theorem Prefunctor.pathStar_surjective (hφ : ∀ u, Surjective (φ.unit u)) (u : U) :
     Surjective (φ.PathStar u) :=
   by
@@ -248,26 +299,32 @@ theorem Prefunctor.pathStar_surjective (hφ : ∀ u, Surjective (φ.unit u)) (u
     use⟨_, q'.cons eu⟩
     simp only [Prefunctor.mapPath_cons, eq_self_iff_true, heq_iff_eq, and_self_iff]
 #align prefunctor.path_star_surjective Prefunctor.pathStar_surjective
+-/
 
+#print Prefunctor.pathStar_bijective /-
 theorem Prefunctor.pathStar_bijective (hφ : ∀ u, Bijective (φ.unit u)) (u : U) :
     Bijective (φ.PathStar u) :=
   ⟨φ.pathStar_injective (fun u => (hφ u).1) _, φ.pathStar_surjective (fun u => (hφ u).2) _⟩
 #align prefunctor.path_star_bijective Prefunctor.pathStar_bijective
+-/
 
 namespace Prefunctor.IsCovering
 
 variable {φ}
 
+#print Prefunctor.IsCovering.pathStar_bijective /-
 protected theorem pathStar_bijective (hφ : φ.IsCovering) (u : U) : Bijective (φ.PathStar u) :=
   φ.pathStar_bijective hφ.1 u
 #align prefunctor.is_covering.path_star_bijective Prefunctor.IsCovering.pathStar_bijective
+-/
 
 end Prefunctor.IsCovering
 
 section HasInvolutiveReverse
 
 variable [HasInvolutiveReverse U] [HasInvolutiveReverse V] [Prefunctor.MapReverse φ]
 
+#print Quiver.starEquivCostar /-
 /-- In a quiver with involutive inverses, the star and costar at every vertex are equivalent.
 This map is induced by `quiver.reverse`. -/
 @[simps]
@@ -278,38 +335,51 @@ def Quiver.starEquivCostar (u : U) : Quiver.Star u ≃ Quiver.Costar u
   left_inv e := by simp [Sigma.ext_iff]
   right_inv e := by simp [Sigma.ext_iff]
 #align quiver.star_equiv_costar Quiver.starEquivCostar
+-/
 
+#print Quiver.starEquivCostar_apply /-
 @[simp]
 theorem Quiver.starEquivCostar_apply {u v : U} (e : u ⟶ v) :
     Quiver.starEquivCostar u (Quiver.Star.mk e) = Quiver.Costar.mk (reverse e) :=
   rfl
 #align quiver.star_equiv_costar_apply Quiver.starEquivCostar_apply
+-/
 
+#print Quiver.starEquivCostar_symm_apply /-
 @[simp]
 theorem Quiver.starEquivCostar_symm_apply {u v : U} (e : u ⟶ v) :
     (Quiver.starEquivCostar v).symm (Quiver.Costar.mk e) = Quiver.Star.mk (reverse e) :=
   rfl
 #align quiver.star_equiv_costar_symm_apply Quiver.starEquivCostar_symm_apply
+-/
 
+#print Prefunctor.costar_conj_star /-
 theorem Prefunctor.costar_conj_star (u : U) :
     φ.Costar u = Quiver.starEquivCostar (φ.obj u) ∘ φ.unit u ∘ (Quiver.starEquivCostar u).symm := by
   ext ⟨v, f⟩ <;> simp
 #align prefunctor.costar_conj_star Prefunctor.costar_conj_star
+-/
 
+#print Prefunctor.bijective_costar_iff_bijective_star /-
 theorem Prefunctor.bijective_costar_iff_bijective_star (u : U) :
     Bijective (φ.Costar u) ↔ Bijective (φ.unit u) := by
   rw [Prefunctor.costar_conj_star, bijective.of_comp_iff', bijective.of_comp_iff] <;>
     exact Equiv.bijective _
 #align prefunctor.bijective_costar_iff_bijective_star Prefunctor.bijective_costar_iff_bijective_star
+-/
 
+#print Prefunctor.isCovering_of_bijective_star /-
 theorem Prefunctor.isCovering_of_bijective_star (h : ∀ u, Bijective (φ.unit u)) : φ.IsCovering :=
   ⟨h, fun u => (φ.bijective_costar_iff_bijective_star u).2 (h u)⟩
 #align prefunctor.is_covering_of_bijective_star Prefunctor.isCovering_of_bijective_star
+-/
 
+#print Prefunctor.isCovering_of_bijective_costar /-
 theorem Prefunctor.isCovering_of_bijective_costar (h : ∀ u, Bijective (φ.Costar u)) :
     φ.IsCovering :=
   ⟨fun u => (φ.bijective_costar_iff_bijective_star u).1 (h u), h⟩
 #align prefunctor.is_covering_of_bijective_costar Prefunctor.isCovering_of_bijective_costar
+-/
 
 end HasInvolutiveReverse
 

Mathbin/Combinatorics/Quiver/Symmetric.lean

@@ -251,17 +251,21 @@ theorem lift_unique [HasReverse V'] (φ : V ⥤q V') (Φ : Symmetrify V ⥤q V')
 #align quiver.symmetrify.lift_unique Quiver.Symmetrify.lift_unique
 -/
 
+#print Prefunctor.symmetrify /-
 /-- A prefunctor canonically defines a prefunctor of the symmetrifications. -/
 @[simps]
 def Prefunctor.symmetrify (φ : U ⥤q V) : Symmetrify U ⥤q Symmetrify V
     where
   obj := φ.obj
   map X Y := Sum.map φ.map φ.map
 #align prefunctor.symmetrify Prefunctor.symmetrify
+-/
 
+#print Prefunctor.symmetrify_mapReverse /-
 instance Prefunctor.symmetrify_mapReverse (φ : U ⥤q V) : Prefunctor.MapReverse φ.Symmetrify :=
   ⟨fun u v e => by cases e <;> rfl⟩
 #align prefunctor.symmetrify_map_reverse Prefunctor.symmetrify_mapReverse
+-/
 
 end Symmetrify
 

lake-manifest.json

@@ -10,9 +10,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "474b14315d7a22e60920bd1f4392e59966a69135",
+    "rev": "62499a26e3ce45dc590cb2e9dbe81725d0ebece5",
     "name": "lean3port",
-    "inputRev?": "474b14315d7a22e60920bd1f4392e59966a69135"}},
+    "inputRev?": "62499a26e3ce45dc590cb2e9dbe81725d0ebece5"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
@@ -22,9 +22,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "3d6112b5c7d095d3088b359c611a5a2704c5dbdc",
+    "rev": "a28c6c6ce79d0b1160e83639f511b5bebbe93cac",
     "name": "mathlib",
-    "inputRev?": "3d6112b5c7d095d3088b359c611a5a2704c5dbdc"}},
+    "inputRev?": "a28c6c6ce79d0b1160e83639f511b5bebbe93cac"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-08-13-07"
+def tag : String := "nightly-2023-08-13-09"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"474b14315d7a22e60920bd1f4392e59966a69135"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"62499a26e3ce45dc590cb2e9dbe81725d0ebece5"
 
 @[default_target]
 lean_lib Mathbin where