bump to nightly-2024-04-14-09

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Algebra/Category/AlgebraCat/Basic.lean

@@ -232,7 +232,8 @@ instance (X : Type u) [Ring X] [Algebra R X] : Coe (Subalgebra R X) (AlgebraCat
   ⟨fun N => AlgebraCat.of R N⟩
 
 #print AlgebraCat.forget_reflects_isos /-
-instance AlgebraCat.forget_reflects_isos : ReflectsIsomorphisms (forget (AlgebraCat.{u} R))
+instance AlgebraCat.forget_reflects_isos :
+    CategoryTheory.Functor.ReflectsIsomorphisms (forget (AlgebraCat.{u} R))
     where reflects X Y f _ := by
     skip
     let i := as_iso ((forget (AlgebraCat.{u} R)).map f)

Mathbin/Algebra/Category/FGModuleCat/Basic.lean

@@ -84,7 +84,8 @@ instance (V : FGModuleCat R) : Module.Finite R V.obj :=
 instance : HasForget₂ (FGModuleCat.{u} R) (ModuleCat.{u} R) := by dsimp [FGModuleCat];
   infer_instance
 
-instance : Full (forget₂ (FGModuleCat R) (ModuleCat.{u} R)) where preimage X Y f := f
+instance : CategoryTheory.Functor.Full (forget₂ (FGModuleCat R) (ModuleCat.{u} R))
+    where preimage X Y f := f
 
 variable {R}
 
@@ -147,8 +148,8 @@ def forget₂Monoidal : MonoidalFunctor (FGModuleCat R) (ModuleCat.{u} R) :=
 -/
 
 #print FGModuleCat.forget₂Monoidal_faithful /-
-instance forget₂Monoidal_faithful : Faithful (forget₂Monoidal R).toFunctor := by
-  dsimp [forget₂_monoidal]; infer_instance
+instance forget₂Monoidal_faithful : CategoryTheory.Functor.Faithful (forget₂Monoidal R).toFunctor :=
+  by dsimp [forget₂_monoidal]; infer_instance
 #align fgModule.forget₂_monoidal_faithful FGModuleCat.forget₂Monoidal_faithful
 -/
 

Mathbin/Algebra/Category/GroupCat/Basic.lean

@@ -433,7 +433,8 @@ end CategoryTheory.Aut
 
 #print GroupCat.forget_reflects_isos /-
 @[to_additive]
-instance GroupCat.forget_reflects_isos : ReflectsIsomorphisms (forget GroupCat.{u})
+instance GroupCat.forget_reflects_isos :
+    CategoryTheory.Functor.ReflectsIsomorphisms (forget GroupCat.{u})
     where reflects X Y f _ := by
     skip
     let i := as_iso ((forget GroupCat).map f)
@@ -445,7 +446,8 @@ instance GroupCat.forget_reflects_isos : ReflectsIsomorphisms (forget GroupCat.{
 
 #print CommGroupCat.forget_reflects_isos /-
 @[to_additive]
-instance CommGroupCat.forget_reflects_isos : ReflectsIsomorphisms (forget CommGroupCat.{u})
+instance CommGroupCat.forget_reflects_isos :
+    CategoryTheory.Functor.ReflectsIsomorphisms (forget CommGroupCat.{u})
     where reflects X Y f _ := by
     skip
     let i := as_iso ((forget CommGroupCat).map f)

Mathbin/Algebra/Category/GroupCat/ZModuleEquivalence.lean

@@ -30,7 +30,8 @@ namespace ModuleCat
 
 #print ModuleCat.forget₂AddCommGroupFull /-
 /-- The forgetful functor from `ℤ` modules to `AddCommGroup` is full. -/
-instance forget₂AddCommGroupFull : Full (forget₂ (ModuleCat ℤ) AddCommGroupCat.{u})
+instance forget₂AddCommGroupFull :
+    CategoryTheory.Functor.Full (forget₂ (ModuleCat ℤ) AddCommGroupCat.{u})
     where preimage A B
     f :=-- `add_monoid_hom.to_int_linear_map` doesn't work here because `A` and `B` are not definitionally
     -- equal to the canonical `add_comm_group.int_module` module instances it expects.
@@ -43,7 +44,8 @@ instance forget₂AddCommGroupFull : Full (forget₂ (ModuleCat ℤ) AddCommGrou
 
 #print ModuleCat.forget₂_addCommGroupCat_essSurj /-
 /-- The forgetful functor from `ℤ` modules to `AddCommGroup` is essentially surjective. -/
-instance forget₂_addCommGroupCat_essSurj : EssSurj (forget₂ (ModuleCat ℤ) AddCommGroupCat.{u})
+instance forget₂_addCommGroupCat_essSurj :
+    CategoryTheory.Functor.EssSurj (forget₂ (ModuleCat ℤ) AddCommGroupCat.{u})
     where mem_essImage A :=
     ⟨ModuleCat.of ℤ A,
       ⟨{  Hom := 𝟙 A
@@ -53,8 +55,9 @@ instance forget₂_addCommGroupCat_essSurj : EssSurj (forget₂ (ModuleCat ℤ)
 
 #print ModuleCat.forget₂AddCommGroupIsEquivalence /-
 noncomputable instance forget₂AddCommGroupIsEquivalence :
-    IsEquivalence (forget₂ (ModuleCat ℤ) AddCommGroupCat.{u}) :=
-  Equivalence.ofFullyFaithfullyEssSurj (forget₂ (ModuleCat ℤ) AddCommGroupCat)
+    CategoryTheory.Functor.IsEquivalence (forget₂ (ModuleCat ℤ) AddCommGroupCat.{u}) :=
+  CategoryTheory.Functor.IsEquivalence.ofFullyFaithfullyEssSurj
+    (forget₂ (ModuleCat ℤ) AddCommGroupCat)
 #align Module.forget₂_AddCommGroup_is_equivalence ModuleCat.forget₂AddCommGroupIsEquivalence
 -/
 

Mathbin/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -91,7 +91,7 @@ def ModuleCat.restrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S]
 -/
 
 instance {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) :
-    CategoryTheory.Faithful (ModuleCat.restrictScalars.{v} f)
+    CategoryTheory.Functor.Faithful (ModuleCat.restrictScalars.{v} f)
     where map_injective' _ _ _ _ h :=
     LinearMap.ext fun x => by simpa only using DFunLike.congr_fun h x
 

Mathbin/Algebra/Category/MonCat/Basic.lean

@@ -309,7 +309,8 @@ def mulEquivIsoCommMonCatIso {X Y : Type u} [CommMonoid X] [CommMonoid Y] :
 
 #print MonCat.forget_reflects_isos /-
 @[to_additive]
-instance MonCat.forget_reflects_isos : ReflectsIsomorphisms (forget MonCat.{u})
+instance MonCat.forget_reflects_isos :
+    CategoryTheory.Functor.ReflectsIsomorphisms (forget MonCat.{u})
     where reflects X Y f _ := by
     skip
     let i := as_iso ((forget MonCat).map f)
@@ -321,7 +322,8 @@ instance MonCat.forget_reflects_isos : ReflectsIsomorphisms (forget MonCat.{u})
 
 #print CommMonCat.forget_reflects_isos /-
 @[to_additive]
-instance CommMonCat.forget_reflects_isos : ReflectsIsomorphisms (forget CommMonCat.{u})
+instance CommMonCat.forget_reflects_isos :
+    CategoryTheory.Functor.ReflectsIsomorphisms (forget CommMonCat.{u})
     where reflects X Y f _ := by
     skip
     let i := as_iso ((forget CommMonCat).map f)
@@ -338,5 +340,6 @@ reflect isomorphisms.
 -/
 
 
-example : ReflectsIsomorphisms (forget₂ CommMonCat MonCat) := by infer_instance
+example : CategoryTheory.Functor.ReflectsIsomorphisms (forget₂ CommMonCat MonCat) := by
+  infer_instance
 

Mathbin/Algebra/Category/Ring/Basic.lean

@@ -309,7 +309,8 @@ instance hasForgetToCommSemiRingCat : HasForget₂ CommRingCat CommSemiRingCat :
 #align CommRing.has_forget_to_CommSemiRing CommRingCat.hasForgetToCommSemiRingCat
 -/
 
-instance : Full (forget₂ CommRingCat CommSemiRingCat) where preimage X Y f := f
+instance : CategoryTheory.Functor.Full (forget₂ CommRingCat CommSemiRingCat)
+    where preimage X Y f := f
 
 end CommRingCat
 
@@ -410,7 +411,8 @@ def ringEquivIsoCommRingIso {X Y : Type u} [CommRing X] [CommRing Y] :
 -/
 
 #print RingCat.forget_reflects_isos /-
-instance RingCat.forget_reflects_isos : ReflectsIsomorphisms (forget RingCat.{u})
+instance RingCat.forget_reflects_isos :
+    CategoryTheory.Functor.ReflectsIsomorphisms (forget RingCat.{u})
     where reflects X Y f _ := by
     skip
     let i := as_iso ((forget RingCat).map f)
@@ -420,7 +422,8 @@ instance RingCat.forget_reflects_isos : ReflectsIsomorphisms (forget RingCat.{u}
 -/
 
 #print CommRingCat.forget_reflects_isos /-
-instance CommRingCat.forget_reflects_isos : ReflectsIsomorphisms (forget CommRingCat.{u})
+instance CommRingCat.forget_reflects_isos :
+    CategoryTheory.Functor.ReflectsIsomorphisms (forget CommRingCat.{u})
     where reflects X Y f _ := by
     skip
     let i := as_iso ((forget CommRingCat).map f)
@@ -448,5 +451,6 @@ theorem CommRingCat.ringHom_comp_eq_comp {R S T : Type _} [CommRing R] [CommRing
 -- which can cause typeclass loops:
 attribute [local instance] reflects_isomorphisms_forget₂
 
-example : ReflectsIsomorphisms (forget₂ RingCat AddCommGroupCat) := by infer_instance
+example : CategoryTheory.Functor.ReflectsIsomorphisms (forget₂ RingCat AddCommGroupCat) := by
+  infer_instance
 

Mathbin/Algebra/Category/SemigroupCat/Basic.lean

@@ -304,7 +304,8 @@ def mulEquivIsoSemigroupCatIso {X Y : Type u} [Semigroup X] [Semigroup Y] :
 
 #print MagmaCat.forgetReflectsIsos /-
 @[to_additive]
-instance MagmaCat.forgetReflectsIsos : ReflectsIsomorphisms (forget MagmaCat.{u})
+instance MagmaCat.forgetReflectsIsos :
+    CategoryTheory.Functor.ReflectsIsomorphisms (forget MagmaCat.{u})
     where reflects X Y f _ := by
     skip
     let i := as_iso ((forget MagmaCat).map f)
@@ -316,7 +317,8 @@ instance MagmaCat.forgetReflectsIsos : ReflectsIsomorphisms (forget MagmaCat.{u}
 
 #print SemigroupCat.forgetReflectsIsos /-
 @[to_additive]
-instance SemigroupCat.forgetReflectsIsos : ReflectsIsomorphisms (forget SemigroupCat.{u})
+instance SemigroupCat.forgetReflectsIsos :
+    CategoryTheory.Functor.ReflectsIsomorphisms (forget SemigroupCat.{u})
     where reflects X Y f _ := by
     skip
     let i := as_iso ((forget SemigroupCat).map f)
@@ -333,5 +335,6 @@ reflect isomorphisms.
 -/
 
 
-example : ReflectsIsomorphisms (forget₂ SemigroupCat MagmaCat) := by infer_instance
+example : CategoryTheory.Functor.ReflectsIsomorphisms (forget₂ SemigroupCat MagmaCat) := by
+  infer_instance
 

Mathbin/Algebra/Homology/Additive.lean

@@ -204,8 +204,8 @@ instance Functor.map_homogical_complex_additive (F : V ⥤ W) [F.Additive] (c :
 
 #print CategoryTheory.Functor.mapHomologicalComplex_reflects_iso /-
 instance Functor.mapHomologicalComplex_reflects_iso (F : V ⥤ W) [F.Additive]
-    [ReflectsIsomorphisms F] (c : ComplexShape ι) :
-    ReflectsIsomorphisms (F.mapHomologicalComplex c) :=
+    [CategoryTheory.Functor.ReflectsIsomorphisms F] (c : ComplexShape ι) :
+    CategoryTheory.Functor.ReflectsIsomorphisms (F.mapHomologicalComplex c) :=
   ⟨fun X Y f => by
     intro
     haveI : ∀ n : ι, is_iso (F.map (f.f n)) := fun n =>

Mathbin/Algebra/Homology/LocalCohomology.lean

@@ -299,7 +299,7 @@ def SelfLERadical.cast (hJK : J.radical = K.radical) : SelfLERadical J ⥤ SelfL
 #print localCohomology.SelfLERadical.castIsEquivalence /-
 -- TODO generalize this to the equivalence of full categories for any `iff`.
 instance SelfLERadical.castIsEquivalence (hJK : J.radical = K.radical) :
-    IsEquivalence (SelfLERadical.cast hJK)
+    CategoryTheory.Functor.IsEquivalence (SelfLERadical.cast hJK)
     where
   inverse := SelfLERadical.cast hJK.symm
   unitIso := by tidy

Mathbin/Algebra/Homology/QuasiIso.lean

@@ -250,7 +250,8 @@ end ToSingle₀
 end HomologicalComplex.Hom
 
 variable {A : Type _} [Category A] [Abelian A] {B : Type _} [Category B] [Abelian B] (F : A ⥤ B)
-  [Functor.Additive F] [PreservesFiniteLimits F] [PreservesFiniteColimits F] [Faithful F]
+  [Functor.Additive F] [PreservesFiniteLimits F] [PreservesFiniteColimits F]
+  [CategoryTheory.Functor.Faithful F]
 
 #print CategoryTheory.Functor.quasiIso'_of_map_quasiIso' /-
 theorem CategoryTheory.Functor.quasiIso'_of_map_quasiIso' {C D : HomologicalComplex A c} (f : C ⟶ D)

Mathbin/Algebra/Homology/Single.lean

@@ -93,7 +93,7 @@ theorem single_map_f_self (j : ι) {A B : V} (f : A ⟶ B) :
 #align homological_complex.single_map_f_self HomologicalComplex.single_map_f_self
 -/
 
-instance (j : ι) : Faithful (single V c j)
+instance (j : ι) : CategoryTheory.Functor.Faithful (single V c j)
     where map_injective' X Y f g w := by
     have := congr_hom w j
     dsimp at this
@@ -103,7 +103,7 @@ instance (j : ι) : Faithful (single V c j)
       eq_to_hom_refl, category.comp_id] at this
     exact this
 
-instance (j : ι) : Full (single V c j)
+instance (j : ι) : CategoryTheory.Functor.Full (single V c j)
     where
   preimage X Y f := eqToHom (by simp) ≫ f.f j ≫ eqToHom (by simp)
   witness' X Y f := by
@@ -298,11 +298,11 @@ def single₀IsoSingle : single₀ V ≅ single V _ 0 :=
     fun X Y f => by ext (_ | i) <;> · dsimp; simp
 #align chain_complex.single₀_iso_single ChainComplex.single₀IsoSingle
 
-instance : Faithful (single₀ V) :=
-  Faithful.of_iso (single₀IsoSingle V).symm
+instance : CategoryTheory.Functor.Faithful (single₀ V) :=
+  CategoryTheory.Functor.Faithful.of_iso (single₀IsoSingle V).symm
 
-instance : Full (single₀ V) :=
-  Full.ofIso (single₀IsoSingle V).symm
+instance : CategoryTheory.Functor.Full (single₀ V) :=
+  CategoryTheory.Functor.Full.ofIso (single₀IsoSingle V).symm
 
 end ChainComplex
 
@@ -452,11 +452,11 @@ def single₀IsoSingle : single₀ V ≅ single V _ 0 :=
     fun X Y f => by ext (_ | i) <;> · dsimp; simp
 #align cochain_complex.single₀_iso_single CochainComplex.single₀IsoSingle
 
-instance : Faithful (single₀ V) :=
-  Faithful.of_iso (single₀IsoSingle V).symm
+instance : CategoryTheory.Functor.Faithful (single₀ V) :=
+  CategoryTheory.Functor.Faithful.of_iso (single₀IsoSingle V).symm
 
-instance : Full (single₀ V) :=
-  Full.ofIso (single₀IsoSingle V).symm
+instance : CategoryTheory.Functor.Full (single₀ V) :=
+  CategoryTheory.Functor.Full.ofIso (single₀IsoSingle V).symm
 
 end CochainComplex
 

Mathbin/AlgebraicGeometry/AffineScheme.lean

@@ -126,7 +126,8 @@ namespace AffineScheme
 /-- The `Spec` functor into the category of affine schemes. -/
 def Spec : CommRingCatᵒᵖ ⥤ AffineScheme :=
   Scheme.Spec.toEssImage
-deriving Full, Faithful, EssSurj
+deriving CategoryTheory.Functor.Full, CategoryTheory.Functor.Faithful,
+  CategoryTheory.Functor.EssSurj
 #align algebraic_geometry.AffineScheme.Spec AlgebraicGeometry.AffineScheme.Spec
 -/
 
@@ -135,7 +136,7 @@ deriving Full, Faithful, EssSurj
 @[simps]
 def forgetToScheme : AffineScheme ⥤ Scheme :=
   Scheme.Spec.essImageInclusion
-deriving Full, Faithful
+deriving CategoryTheory.Functor.Full, CategoryTheory.Functor.Faithful
 #align algebraic_geometry.AffineScheme.forget_to_Scheme AlgebraicGeometry.AffineScheme.forgetToScheme
 -/
 
@@ -154,7 +155,7 @@ def equivCommRingCat : AffineScheme ≌ CommRingCatᵒᵖ :=
 -/
 
 #print AlgebraicGeometry.AffineScheme.ΓIsEquiv /-
-instance ΓIsEquiv : IsEquivalence Γ.{u} :=
+instance ΓIsEquiv : CategoryTheory.Functor.IsEquivalence Γ.{u} :=
   haveI : is_equivalence Γ.{u}.rightOp.op := is_equivalence.of_equivalence equiv_CommRing.op
   (functor.is_equivalence_trans Γ.{u}.rightOp.op (op_op_equivalence _).Functor : _)
 #align algebraic_geometry.AffineScheme.Γ_is_equiv AlgebraicGeometry.AffineScheme.ΓIsEquiv
@@ -172,7 +173,7 @@ instance : HasLimits AffineScheme.{u} :=
 
 noncomputable instance : PreservesLimits Γ.{u}.rightOp :=
   @Adjunction.isEquivalencePreservesLimits _ _ Γ.rightOp
-    (IsEquivalence.ofEquivalence equivCommRingCat)
+    (CategoryTheory.Functor.IsEquivalence.ofEquivalence equivCommRingCat)
 
 noncomputable instance : PreservesLimits forgetToScheme :=
   by

Mathbin/AlgebraicGeometry/GammaSpecAdjunction.lean

@@ -491,21 +491,21 @@ instance Spec.preservesLimits : Limits.preservesLimits Scheme.Spec :=
 -/
 
 /-- Spec is a full functor. -/
-instance : Full Spec.toLocallyRingedSpace :=
+instance : CategoryTheory.Functor.Full Spec.toLocallyRingedSpace :=
   rFullOfCounitIsIso ΓSpec.locallyRingedSpaceAdjunction
 
 #print AlgebraicGeometry.Spec.full /-
-instance Spec.full : Full Scheme.Spec :=
+instance Spec.full : CategoryTheory.Functor.Full Scheme.Spec :=
   rFullOfCounitIsIso ΓSpec.adjunction
 #align algebraic_geometry.Spec.full AlgebraicGeometry.Spec.full
 -/
 
 /-- Spec is a faithful functor. -/
-instance : Faithful Spec.toLocallyRingedSpace :=
+instance : CategoryTheory.Functor.Faithful Spec.toLocallyRingedSpace :=
   R_faithful_of_counit_isIso ΓSpec.locallyRingedSpaceAdjunction
 
 #print AlgebraicGeometry.Spec.faithful /-
-instance Spec.faithful : Faithful Scheme.Spec :=
+instance Spec.faithful : CategoryTheory.Functor.Faithful Scheme.Spec :=
   R_faithful_of_counit_isIso ΓSpec.adjunction
 #align algebraic_geometry.Spec.faithful AlgebraicGeometry.Spec.faithful
 -/

Mathbin/AlgebraicGeometry/Scheme.lean

@@ -81,7 +81,7 @@ protected abbrev sheaf (X : Scheme) :=
 @[simps]
 def forgetToLocallyRingedSpace : Scheme ⥤ LocallyRingedSpace :=
   inducedFunctor _
-deriving Full, Faithful
+deriving CategoryTheory.Functor.Full, CategoryTheory.Functor.Faithful
 #align algebraic_geometry.Scheme.forget_to_LocallyRingedSpace AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
 -/
 

Mathbin/AlgebraicTopology/DoldKan/NReflectsIso.lean

@@ -45,7 +45,9 @@ variable {C : Type _} [Category C] [Preadditive C]
 
 open MorphComponents
 
-instance : ReflectsIsomorphisms (N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ)) :=
+instance :
+    CategoryTheory.Functor.ReflectsIsomorphisms
+      (N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ)) :=
   ⟨fun X Y f => by
     intro
     -- restating the result in a way that allows induction on the degree n
@@ -115,7 +117,9 @@ theorem compatibility_N₂_N₁_karoubi :
 /-- We deduce that `N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ))`
 reflects isomorphisms from the fact that
 `N₁ : simplicial_object (karoubi C) ⥤ karoubi (chain_complex (karoubi C) ℕ)` does. -/
-instance : ReflectsIsomorphisms (N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ)) :=
+instance :
+    CategoryTheory.Functor.ReflectsIsomorphisms
+      (N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ)) :=
   ⟨fun X Y f => by
     intro
     -- The following functor `F` reflects isomorphism because it is