bump to nightly-2023-02-22-06

mathlib commit leanprover-community/mathlib@bd9851c

Mathbin/CategoryTheory/IsomorphismClasses.lean

@@ -28,32 +28,40 @@ section Category
 
 variable {C : Type u} [Category.{v} C]
 
+#print CategoryTheory.IsIsomorphic /-
 /-- An object `X` is isomorphic to an object `Y`, if `X ≅ Y` is not empty. -/
 def IsIsomorphic : C → C → Prop := fun X Y => Nonempty (X ≅ Y)
 #align category_theory.is_isomorphic CategoryTheory.IsIsomorphic
+-/
 
 variable (C)
 
+#print CategoryTheory.isIsomorphicSetoid /-
 /-- `is_isomorphic` defines a setoid. -/
 def isIsomorphicSetoid : Setoid C where
   R := IsIsomorphic
   iseqv := ⟨fun X => ⟨Iso.refl X⟩, fun X Y ⟨α⟩ => ⟨α.symm⟩, fun X Y Z ⟨α⟩ ⟨β⟩ => ⟨α.trans β⟩⟩
 #align category_theory.is_isomorphic_setoid CategoryTheory.isIsomorphicSetoid
+-/
 
 end Category
 
+#print CategoryTheory.isomorphismClasses /-
 /-- The functor that sends each category to the quotient space of its objects up to an isomorphism.
 -/
 def isomorphismClasses : Cat.{v, u} ⥤ Type u
     where
   obj C := Quotient (isIsomorphicSetoid C.α)
   map C D F := Quot.map F.obj fun X Y ⟨f⟩ => ⟨F.mapIso f⟩
 #align category_theory.isomorphism_classes CategoryTheory.isomorphismClasses
+-/
 
+#print CategoryTheory.Groupoid.isIsomorphic_iff_nonempty_hom /-
 theorem Groupoid.isIsomorphic_iff_nonempty_hom {C : Type u} [Groupoid.{v} C] {X Y : C} :
     IsIsomorphic X Y ↔ Nonempty (X ⟶ Y) :=
   (Groupoid.isoEquivHom X Y).nonempty_congr
 #align category_theory.groupoid.is_isomorphic_iff_nonempty_hom CategoryTheory.Groupoid.isIsomorphic_iff_nonempty_hom
+-/
 
 -- PROJECT: define `skeletal`, and show every category is equivalent to a skeletal category,
 -- using the axiom of choice to pick a representative of every isomorphism class.

Mathbin/CategoryTheory/Limits/Shapes/StrongEpi.lean

@@ -47,13 +47,16 @@ variable {C : Type u} [Category.{v} C]
 
 variable {P Q : C}
 
+#print CategoryTheory.StrongEpi /-
 /-- A strong epimorphism `f` is an epimorphism which has the left lifting property
 with respect to monomorphisms. -/
 class StrongEpi (f : P ⟶ Q) : Prop where
   Epi : Epi f
   llp : ∀ ⦃X Y : C⦄ (z : X ⟶ Y) [Mono z], HasLiftingProperty f z
 #align category_theory.strong_epi CategoryTheory.StrongEpi
+-/
 
+#print CategoryTheory.StrongEpi.mk' /-
 theorem StrongEpi.mk' {f : P ⟶ Q} [Epi f]
     (hf :
       ∀ (X Y : C) (z : X ⟶ Y) (hz : Mono z) (u : P ⟶ X) (v : Q ⟶ Y) (sq : CommSq u f z v),
@@ -62,14 +65,18 @@ theorem StrongEpi.mk' {f : P ⟶ Q} [Epi f]
   { Epi := inferInstance
     llp := fun X Y z hz => ⟨fun u v sq => hf X Y z hz u v sq⟩ }
 #align category_theory.strong_epi.mk' CategoryTheory.StrongEpi.mk'
+-/
 
+#print CategoryTheory.StrongMono /-
 /-- A strong monomorphism `f` is a monomorphism which has the right lifting property
 with respect to epimorphisms. -/
 class StrongMono (f : P ⟶ Q) : Prop where
   Mono : Mono f
   rlp : ∀ ⦃X Y : C⦄ (z : X ⟶ Y) [Epi z], HasLiftingProperty z f
 #align category_theory.strong_mono CategoryTheory.StrongMono
+-/
 
+#print CategoryTheory.StrongMono.mk' /-
 theorem StrongMono.mk' {f : P ⟶ Q} [Mono f]
     (hf :
       ∀ (X Y : C) (z : X ⟶ Y) (hz : Epi z) (u : X ⟶ P) (v : Y ⟶ Q) (sq : CommSq u z f v),
@@ -78,39 +85,49 @@ theorem StrongMono.mk' {f : P ⟶ Q} [Mono f]
   { Mono := inferInstance
     rlp := fun X Y z hz => ⟨fun u v sq => hf X Y z hz u v sq⟩ }
 #align category_theory.strong_mono.mk' CategoryTheory.StrongMono.mk'
+-/
 
 attribute [instance] strong_epi.llp
 
 attribute [instance] strong_mono.rlp
 
+#print CategoryTheory.epi_of_strongEpi /-
 instance (priority := 100) epi_of_strongEpi (f : P ⟶ Q) [StrongEpi f] : Epi f :=
   StrongEpi.epi
 #align category_theory.epi_of_strong_epi CategoryTheory.epi_of_strongEpi
+-/
 
+#print CategoryTheory.mono_of_strongMono /-
 instance (priority := 100) mono_of_strongMono (f : P ⟶ Q) [StrongMono f] : Mono f :=
   StrongMono.mono
 #align category_theory.mono_of_strong_mono CategoryTheory.mono_of_strongMono
+-/
 
 section
 
 variable {R : C} (f : P ⟶ Q) (g : Q ⟶ R)
 
+#print CategoryTheory.strongEpi_comp /-
 /-- The composition of two strong epimorphisms is a strong epimorphism. -/
 theorem strongEpi_comp [StrongEpi f] [StrongEpi g] : StrongEpi (f ≫ g) :=
   { Epi := epi_comp _ _
     llp := by
       intros
       infer_instance }
 #align category_theory.strong_epi_comp CategoryTheory.strongEpi_comp
+-/
 
+#print CategoryTheory.strongMono_comp /-
 /-- The composition of two strong monomorphisms is a strong monomorphism. -/
 theorem strongMono_comp [StrongMono f] [StrongMono g] : StrongMono (f ≫ g) :=
   { Mono := mono_comp _ _
     rlp := by
       intros
       infer_instance }
 #align category_theory.strong_mono_comp CategoryTheory.strongMono_comp
+-/
 
+#print CategoryTheory.strongEpi_of_strongEpi /-
 /-- If `f ≫ g` is a strong epimorphism, then so is `g`. -/
 theorem strongEpi_of_strongEpi [StrongEpi (f ≫ g)] : StrongEpi g :=
   { Epi := epi_of_epi f g
@@ -124,7 +141,9 @@ theorem strongEpi_of_strongEpi [StrongEpi (f ≫ g)] : StrongEpi g :=
           ⟨(comm_sq.mk h₀).lift, by
             simp only [← cancel_mono z, category.assoc, comm_sq.fac_right, sq.w], by simp⟩ }
 #align category_theory.strong_epi_of_strong_epi CategoryTheory.strongEpi_of_strongEpi
+-/
 
+#print CategoryTheory.strongMono_of_strongMono /-
 /-- If `f ≫ g` is a strong monomorphism, then so is `f`. -/
 theorem strongMono_of_strongMono [StrongMono (f ≫ g)] : StrongMono f :=
   { Mono := mono_of_mono f g
@@ -135,21 +154,27 @@ theorem strongMono_of_strongMono [StrongMono (f ≫ g)] : StrongMono f :=
       have h₀ : u ≫ f ≫ g = z ≫ v ≫ g := by rw [reassoc_of sq.w]
       exact comm_sq.has_lift.mk' ⟨(comm_sq.mk h₀).lift, by simp, by simp [← cancel_epi z, sq.w]⟩ }
 #align category_theory.strong_mono_of_strong_mono CategoryTheory.strongMono_of_strongMono
+-/
 
+#print CategoryTheory.strongEpi_of_isIso /-
 /-- An isomorphism is in particular a strong epimorphism. -/
 instance (priority := 100) strongEpi_of_isIso [IsIso f] : StrongEpi f
     where
   Epi := by infer_instance
   llp X Y z hz := HasLiftingProperty.of_left_iso _ _
 #align category_theory.strong_epi_of_is_iso CategoryTheory.strongEpi_of_isIso
+-/
 
+#print CategoryTheory.strongMono_of_isIso /-
 /-- An isomorphism is in particular a strong monomorphism. -/
 instance (priority := 100) strongMono_of_isIso [IsIso f] : StrongMono f
     where
   Mono := by infer_instance
   rlp X Y z hz := HasLiftingProperty.of_right_iso _ _
 #align category_theory.strong_mono_of_is_iso CategoryTheory.strongMono_of_isIso
+-/
 
+#print CategoryTheory.StrongEpi.of_arrow_iso /-
 theorem StrongEpi.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
     (e : Arrow.mk f ≅ Arrow.mk g) [h : StrongEpi f] : StrongEpi g :=
   { Epi := by
@@ -160,7 +185,9 @@ theorem StrongEpi.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
       intro
       apply has_lifting_property.of_arrow_iso_left e z }
 #align category_theory.strong_epi.of_arrow_iso CategoryTheory.StrongEpi.of_arrow_iso
+-/
 
+#print CategoryTheory.StrongMono.of_arrow_iso /-
 theorem StrongMono.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
     (e : Arrow.mk f ≅ Arrow.mk g) [h : StrongMono f] : StrongMono g :=
   { Mono := by
@@ -171,74 +198,95 @@ theorem StrongMono.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
       intro
       apply has_lifting_property.of_arrow_iso_right z e }
 #align category_theory.strong_mono.of_arrow_iso CategoryTheory.StrongMono.of_arrow_iso
+-/
 
+#print CategoryTheory.StrongEpi.iff_of_arrow_iso /-
 theorem StrongEpi.iff_of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
     (e : Arrow.mk f ≅ Arrow.mk g) : StrongEpi f ↔ StrongEpi g :=
   by
   constructor <;> intro
   exacts[strong_epi.of_arrow_iso e, strong_epi.of_arrow_iso e.symm]
 #align category_theory.strong_epi.iff_of_arrow_iso CategoryTheory.StrongEpi.iff_of_arrow_iso
+-/
 
+#print CategoryTheory.StrongMono.iff_of_arrow_iso /-
 theorem StrongMono.iff_of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
     (e : Arrow.mk f ≅ Arrow.mk g) : StrongMono f ↔ StrongMono g :=
   by
   constructor <;> intro
   exacts[strong_mono.of_arrow_iso e, strong_mono.of_arrow_iso e.symm]
 #align category_theory.strong_mono.iff_of_arrow_iso CategoryTheory.StrongMono.iff_of_arrow_iso
+-/
 
 end
 
+#print CategoryTheory.isIso_of_mono_of_strongEpi /-
 /-- A strong epimorphism that is a monomorphism is an isomorphism. -/
 theorem isIso_of_mono_of_strongEpi (f : P ⟶ Q) [Mono f] [StrongEpi f] : IsIso f :=
   ⟨⟨(CommSq.mk (show 𝟙 P ≫ f = f ≫ 𝟙 Q by simp)).lift, by tidy⟩⟩
 #align category_theory.is_iso_of_mono_of_strong_epi CategoryTheory.isIso_of_mono_of_strongEpi
+-/
 
+#print CategoryTheory.isIso_of_epi_of_strongMono /-
 /-- A strong monomorphism that is an epimorphism is an isomorphism. -/
 theorem isIso_of_epi_of_strongMono (f : P ⟶ Q) [Epi f] [StrongMono f] : IsIso f :=
   ⟨⟨(CommSq.mk (show 𝟙 P ≫ f = f ≫ 𝟙 Q by simp)).lift, by tidy⟩⟩
 #align category_theory.is_iso_of_epi_of_strong_mono CategoryTheory.isIso_of_epi_of_strongMono
+-/
 
 section
 
 variable (C)
 
+#print CategoryTheory.StrongEpiCategory /-
 /-- A strong epi category is a category in which every epimorphism is strong. -/
 class StrongEpiCategory : Prop where
   strongEpi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [Epi f], StrongEpi f
 #align category_theory.strong_epi_category CategoryTheory.StrongEpiCategory
+-/
 
+#print CategoryTheory.StrongMonoCategory /-
 /-- A strong mono category is a category in which every monomorphism is strong. -/
 class StrongMonoCategory : Prop where
   strongMono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [Mono f], StrongMono f
 #align category_theory.strong_mono_category CategoryTheory.StrongMonoCategory
+-/
 
 end
 
+#print CategoryTheory.strongEpi_of_epi /-
 theorem strongEpi_of_epi [StrongEpiCategory C] (f : P ⟶ Q) [Epi f] : StrongEpi f :=
   StrongEpiCategory.strongEpi_of_epi _
 #align category_theory.strong_epi_of_epi CategoryTheory.strongEpi_of_epi
+-/
 
+#print CategoryTheory.strongMono_of_mono /-
 theorem strongMono_of_mono [StrongMonoCategory C] (f : P ⟶ Q) [Mono f] : StrongMono f :=
   StrongMonoCategory.strongMono_of_mono _
 #align category_theory.strong_mono_of_mono CategoryTheory.strongMono_of_mono
+-/
 
 section
 
 attribute [local instance] strong_epi_of_epi
 
+#print CategoryTheory.balanced_of_strongEpiCategory /-
 instance (priority := 100) balanced_of_strongEpiCategory [StrongEpiCategory C] : Balanced C
     where isIso_of_mono_of_epi _ _ _ _ _ := is_iso_of_mono_of_strong_epi _
 #align category_theory.balanced_of_strong_epi_category CategoryTheory.balanced_of_strongEpiCategory
+-/
 
 end
 
 section
 
 attribute [local instance] strong_mono_of_mono
 
+#print CategoryTheory.balanced_of_strongMonoCategory /-
 instance (priority := 100) balanced_of_strongMonoCategory [StrongMonoCategory C] : Balanced C
     where isIso_of_mono_of_epi _ _ _ _ _ := is_iso_of_epi_of_strong_mono _
 #align category_theory.balanced_of_strong_mono_category CategoryTheory.balanced_of_strongMonoCategory
+-/
 
 end
 

Mathbin/Data/Qpf/Multivariate/Constructions/Sigma.lean

@@ -26,25 +26,33 @@ variable {n : ℕ} {A : Type u}
 
 variable (F : A → TypeVec.{u} n → Type u)
 
+#print MvQPF.Sigma /-
 /-- Dependent sum of of an `n`-ary functor. The sum can range over
 data types like `ℕ` or over `Type.{u-1}` -/
 def Sigma (v : TypeVec.{u} n) : Type u :=
   Σα : A, F α v
 #align mvqpf.sigma MvQPF.Sigma
+-/
 
+#print MvQPF.Pi /-
 /-- Dependent product of of an `n`-ary functor. The sum can range over
 data types like `ℕ` or over `Type.{u-1}` -/
 def Pi (v : TypeVec.{u} n) : Type u :=
   ∀ α : A, F α v
 #align mvqpf.pi MvQPF.Pi
+-/
 
+#print MvQPF.Sigma.inhabited /-
 instance Sigma.inhabited {α} [Inhabited A] [Inhabited (F default α)] : Inhabited (Sigma F α) :=
   ⟨⟨default, default⟩⟩
 #align mvqpf.sigma.inhabited MvQPF.Sigma.inhabited
+-/
 
+#print MvQPF.Pi.inhabited /-
 instance Pi.inhabited {α} [∀ a, Inhabited (F a α)] : Inhabited (Pi F α) :=
   ⟨fun a => default⟩
 #align mvqpf.pi.inhabited MvQPF.Pi.inhabited
+-/
 
 variable [∀ α, MvFunctor <| F α]
 
@@ -54,25 +62,31 @@ instance : MvFunctor (Sigma F) where map := fun α β f ⟨a, x⟩ => ⟨a, f <$
 
 variable [∀ α, MvQPF <| F α]
 
+#print MvQPF.Sigma.P /-
 /-- polynomial functor representation of a dependent sum -/
-protected def p : MvPFunctor n :=
+protected def P : MvPFunctor n :=
   ⟨Σa, (p (F a)).A, fun x => (p (F x.1)).B x.2⟩
-#align mvqpf.sigma.P MvQPF.Sigma.p
+#align mvqpf.sigma.P MvQPF.Sigma.P
+-/
 
+#print MvQPF.Sigma.abs /-
 /-- abstraction function for dependent sums -/
-protected def abs ⦃α⦄ : (Sigma.p F).Obj α → Sigma F α
+protected def abs ⦃α⦄ : (Sigma.P F).Obj α → Sigma F α
   | ⟨a, f⟩ => ⟨a.1, MvQPF.abs ⟨a.2, f⟩⟩
 #align mvqpf.sigma.abs MvQPF.Sigma.abs
+-/
 
+#print MvQPF.Sigma.repr /-
 /-- representation function for dependent sums -/
-protected def repr ⦃α⦄ : Sigma F α → (Sigma.p F).Obj α
+protected def repr ⦃α⦄ : Sigma F α → (Sigma.P F).Obj α
   | ⟨a, f⟩ =>
     let x := MvQPF.repr f
     ⟨⟨a, x.1⟩, x.2⟩
 #align mvqpf.sigma.repr MvQPF.Sigma.repr
+-/
 
 instance : MvQPF (Sigma F) where
-  p := Sigma.p F
+  p := Sigma.P F
   abs := Sigma.abs F
   repr := Sigma.repr F
   abs_repr := by rintro α ⟨x, f⟩ <;> simp [sigma.repr, sigma.abs, abs_repr]
@@ -88,23 +102,29 @@ instance : MvFunctor (Pi F) where map α β f x a := f <$$> x a
 
 variable [∀ α, MvQPF <| F α]
 
+#print MvQPF.Pi.P /-
 /-- polynomial functor representation of a dependent product -/
-protected def p : MvPFunctor n :=
+protected def P : MvPFunctor n :=
   ⟨∀ a, (p (F a)).A, fun x i => Σa : A, (p (F a)).B (x a) i⟩
-#align mvqpf.pi.P MvQPF.Pi.p
+#align mvqpf.pi.P MvQPF.Pi.P
+-/
 
+#print MvQPF.Pi.abs /-
 /-- abstraction function for dependent products -/
-protected def abs ⦃α⦄ : (Pi.p F).Obj α → Pi F α
+protected def abs ⦃α⦄ : (Pi.P F).Obj α → Pi F α
   | ⟨a, f⟩ => fun x => MvQPF.abs ⟨a x, fun i y => f i ⟨_, y⟩⟩
 #align mvqpf.pi.abs MvQPF.Pi.abs
+-/
 
+#print MvQPF.Pi.repr /-
 /-- representation function for dependent products -/
-protected def repr ⦃α⦄ : Pi F α → (Pi.p F).Obj α
+protected def repr ⦃α⦄ : Pi F α → (Pi.P F).Obj α
   | f => ⟨fun a => (MvQPF.repr (f a)).1, fun i a => (MvQPF.repr (f _)).2 _ a.2⟩
 #align mvqpf.pi.repr MvQPF.Pi.repr
+-/
 
 instance : MvQPF (Pi F) where
-  p := Pi.p F
+  p := Pi.P F
   abs := Pi.abs F
   repr := Pi.repr F
   abs_repr := by rintro α f <;> ext <;> simp [pi.repr, pi.abs, abs_repr]