From 3ce6456c8f46c9d632b2cddb744c8259a458b323 Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Thu, 23 Feb 2023 18:59:38 +0000 Subject: [PATCH] bump to nightly-2023-02-23-18 mathlib commit https://github.com/leanprover-community/mathlib/commit/3ade05ac9447ae31a22d2ea5423435e054131240 --- .../CategoryTheory/Functor/ReflectsIsomorphisms.lean | 12 ++++++++++++ lake-manifest.json | 8 ++++---- lakefile.lean | 4 ++-- 3 files changed, 18 insertions(+), 6 deletions(-) diff --git a/Mathbin/CategoryTheory/Functor/ReflectsIsomorphisms.lean b/Mathbin/CategoryTheory/Functor/ReflectsIsomorphisms.lean index 37fae3b120..e2874bf73c 100644 --- a/Mathbin/CategoryTheory/Functor/ReflectsIsomorphisms.lean +++ b/Mathbin/CategoryTheory/Functor/ReflectsIsomorphisms.lean @@ -37,6 +37,7 @@ variable {D : Type u₂} [Category.{v₂} D] variable {E : Type u₃} [Category.{v₃} E] +#print CategoryTheory.ReflectsIsomorphisms /- /-- Define what it means for a functor `F : C ⥤ D` to reflect isomorphisms: for any morphism `f : A ⟶ B`, if `F.map f` is an isomorphism then `f` is as well. Note that we do not assume or require that `F` is faithful. @@ -44,18 +45,27 @@ Note that we do not assume or require that `F` is faithful. class ReflectsIsomorphisms (F : C ⥤ D) : Prop where reflects : ∀ {A B : C} (f : A ⟶ B) [IsIso (F.map f)], IsIso f #align category_theory.reflects_isomorphisms CategoryTheory.ReflectsIsomorphisms +-/ +/- warning: category_theory.is_iso_of_reflects_iso -> CategoryTheory.isIso_of_reflects_iso is a dubious translation: +lean 3 declaration is + forall {C : Type.{u3}} [_inst_1 : CategoryTheory.Category.{u1, u3} C] {D : Type.{u4}} [_inst_2 : CategoryTheory.Category.{u2, u4} D] {A : C} {B : C} (f : Quiver.Hom.{succ u1, u3} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u3} C (CategoryTheory.Category.toCategoryStruct.{u1, u3} C _inst_1)) A B) (F : CategoryTheory.Functor.{u1, u2, u3, u4} C _inst_1 D _inst_2) [_inst_4 : CategoryTheory.IsIso.{u2, u4} D _inst_2 (CategoryTheory.Functor.obj.{u1, u2, u3, u4} C _inst_1 D _inst_2 F A) (CategoryTheory.Functor.obj.{u1, u2, u3, u4} C _inst_1 D _inst_2 F B) (CategoryTheory.Functor.map.{u1, u2, u3, u4} C _inst_1 D _inst_2 F A B f)] [_inst_5 : CategoryTheory.ReflectsIsomorphisms.{u1, u2, u3, u4} C _inst_1 D _inst_2 F], CategoryTheory.IsIso.{u1, u3} C _inst_1 A B f +but is expected to have type + forall {C : Type.{u3}} [_inst_1 : CategoryTheory.Category.{u1, u3} C] {D : Type.{u4}} [_inst_2 : CategoryTheory.Category.{u2, u4} D] {A : C} {B : C} (f : Quiver.Hom.{succ u1, u3} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u3} C (CategoryTheory.Category.toCategoryStruct.{u1, u3} C _inst_1)) A B) (F : CategoryTheory.Functor.{u1, u2, u3, u4} C _inst_1 D _inst_2) [_inst_4 : CategoryTheory.IsIso.{u2, u4} D _inst_2 (Prefunctor.obj.{succ u1, succ u2, u3, u4} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u3} C (CategoryTheory.Category.toCategoryStruct.{u1, u3} C _inst_1)) D (CategoryTheory.CategoryStruct.toQuiver.{u2, u4} D (CategoryTheory.Category.toCategoryStruct.{u2, u4} D _inst_2)) (CategoryTheory.Functor.toPrefunctor.{u1, u2, u3, u4} C _inst_1 D _inst_2 F) A) (Prefunctor.obj.{succ u1, succ u2, u3, u4} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u3} C (CategoryTheory.Category.toCategoryStruct.{u1, u3} C _inst_1)) D (CategoryTheory.CategoryStruct.toQuiver.{u2, u4} D (CategoryTheory.Category.toCategoryStruct.{u2, u4} D _inst_2)) (CategoryTheory.Functor.toPrefunctor.{u1, u2, u3, u4} C _inst_1 D _inst_2 F) B) (Prefunctor.map.{succ u1, succ u2, u3, u4} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u3} C (CategoryTheory.Category.toCategoryStruct.{u1, u3} C _inst_1)) D (CategoryTheory.CategoryStruct.toQuiver.{u2, u4} D (CategoryTheory.Category.toCategoryStruct.{u2, u4} D _inst_2)) (CategoryTheory.Functor.toPrefunctor.{u1, u2, u3, u4} C _inst_1 D _inst_2 F) A B f)] [_inst_5 : CategoryTheory.ReflectsIsomorphisms.{u1, u2, u3, u4} C _inst_1 D _inst_2 F], CategoryTheory.IsIso.{u1, u3} C _inst_1 A B f +Case conversion may be inaccurate. Consider using '#align category_theory.is_iso_of_reflects_iso CategoryTheory.isIso_of_reflects_isoₓ'. -/ /-- If `F` reflects isos and `F.map f` is an iso, then `f` is an iso. -/ theorem isIso_of_reflects_iso {A B : C} (f : A ⟶ B) (F : C ⥤ D) [IsIso (F.map f)] [ReflectsIsomorphisms F] : IsIso f := ReflectsIsomorphisms.reflects F f #align category_theory.is_iso_of_reflects_iso CategoryTheory.isIso_of_reflects_iso +#print CategoryTheory.of_full_and_faithful /- instance (priority := 100) of_full_and_faithful (F : C ⥤ D) [Full F] [Faithful F] : ReflectsIsomorphisms F where reflects X Y f i := ⟨⟨F.preimage (inv (F.map f)), ⟨F.map_injective (by simp), F.map_injective (by simp)⟩⟩⟩ #align category_theory.of_full_and_faithful CategoryTheory.of_full_and_faithful +-/ instance (F : C ⥤ D) (G : D ⥤ E) [ReflectsIsomorphisms F] [ReflectsIsomorphisms G] : ReflectsIsomorphisms (F ⋙ G) := @@ -64,6 +74,7 @@ instance (F : C ⥤ D) (G : D ⥤ E) [ReflectsIsomorphisms F] [ReflectsIsomorphi haveI := is_iso_of_reflects_iso (F.map f) G exact is_iso_of_reflects_iso f F⟩ +#print CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms /- instance (priority := 100) reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms [Balanced C] (F : C ⥤ D) [ReflectsMonomorphisms F] [ReflectsEpimorphisms F] : ReflectsIsomorphisms F @@ -73,6 +84,7 @@ instance (priority := 100) reflectsIsomorphisms_of_reflectsMonomorphisms_of_refl haveI : mono f := mono_of_mono_map F inferInstance exact is_iso_of_mono_of_epi f #align category_theory.reflects_isomorphisms_of_reflects_monomorphisms_of_reflects_epimorphisms CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms +-/ end ReflectsIso diff --git a/lake-manifest.json b/lake-manifest.json index f96d078887..98a9d5ad7c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,15 +4,15 @@ [{"git": {"url": "https://github.com/leanprover-community/lean3port.git", "subDir?": null, - "rev": "cd9e70903c704f5370c0d800da61fca82770dcc4", + "rev": "6eb0ab3ce9598ae6a412c3ab4392a524c3344c86", "name": "lean3port", - "inputRev?": "cd9e70903c704f5370c0d800da61fca82770dcc4"}}, + "inputRev?": "6eb0ab3ce9598ae6a412c3ab4392a524c3344c86"}}, {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "0245850bc54a9e55ae4ba1ebf872267f8b98ebed", + "rev": "139309db49d236449caabb349066113a9e3669b6", "name": "mathlib", - "inputRev?": "0245850bc54a9e55ae4ba1ebf872267f8b98ebed"}}, + "inputRev?": "139309db49d236449caabb349066113a9e3669b6"}}, {"git": {"url": "https://github.com/gebner/quote4", "subDir?": null, diff --git a/lakefile.lean b/lakefile.lean index 06c558f214..dce28a356a 100644 --- a/lakefile.lean +++ b/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-02-23-16" +def tag : String := "nightly-2023-02-23-18" def releaseRepo : String := "leanprover-community/mathport" def oleanTarName : String := "mathlib3-binport.tar.gz" @@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do untarReleaseArtifact releaseRepo tag oleanTarName libDir return .nil -require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"cd9e70903c704f5370c0d800da61fca82770dcc4" +require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"6eb0ab3ce9598ae6a412c3ab4392a524c3344c86" @[default_target] lean_lib Mathbin where