bump to nightly-2023-05-19-08

mathlib commit leanprover-community/mathlib@95a8761
leanprover-community · May 19, 2023 · 6fa3427 · 6fa3427
1 parent 8768dc8
commit 6fa3427
Show file tree

Hide file tree

Showing 6 changed files with 204 additions and 6 deletions.
diff --git a/Mathbin/Analysis/NormedSpace/Extend.lean b/Mathbin/Analysis/NormedSpace/Extend.lean
diff --git a/Mathbin/RingTheory/MatrixAlgebra.lean b/Mathbin/RingTheory/MatrixAlgebra.lean
diff --git a/Mathbin/Topology/Sheaves/Limits.lean b/Mathbin/Topology/Sheaves/Limits.lean
@@ -41,6 +41,12 @@ instance [HasLimits C] (X : TopCat) : CreatesLimits (Sheaf.forget C X) :=
 instance [HasLimits C] (X : TopCat) : HasLimitsOfSize.{v} (Sheaf.{v} C X) :=
   has_limits_of_has_limits_creates_limits (Sheaf.forget C X)
 
+/- warning: Top.is_sheaf_of_is_limit -> TopCat.isSheaf_of_isLimit is a dubious translation:
+lean 3 declaration is
+  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] {J : Type.{u1}} [_inst_2 : CategoryTheory.SmallCategory.{u1} J] [_inst_3 : CategoryTheory.Limits.HasLimits.{u1, u2} C _inst_1] {X : TopCat.{u1}} (F : CategoryTheory.Functor.{u1, u1, u1, max u2 u1} J _inst_2 (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.Presheaf.category.{u1, u1, u2} C _inst_1 X)), (forall (j : J), TopCat.Presheaf.IsSheaf.{u1, u1, u2} C _inst_1 X (CategoryTheory.Functor.obj.{u1, u1, u1, max u2 u1} J _inst_2 (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.Presheaf.category.{u1, u1, u2} C _inst_1 X) F j)) -> (forall {c : CategoryTheory.Limits.Cone.{u1, u1, u1, max u2 u1} J _inst_2 (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.Presheaf.category.{u1, u1, u2} C _inst_1 X) F}, (CategoryTheory.Limits.IsLimit.{u1, u1, u1, max u2 u1} J _inst_2 (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.Presheaf.category.{u1, u1, u2} C _inst_1 X) F c) -> (TopCat.Presheaf.IsSheaf.{u1, u1, u2} C _inst_1 X (CategoryTheory.Limits.Cone.pt.{u1, u1, u1, max u2 u1} J _inst_2 (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.Presheaf.category.{u1, u1, u2} C _inst_1 X) F c)))
+but is expected to have type
+  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] {J : Type.{u1}} [_inst_2 : CategoryTheory.SmallCategory.{u1} J] [_inst_3 : CategoryTheory.Limits.HasLimits.{u1, u2} C _inst_1] {X : TopCat.{u1}} (F : CategoryTheory.Functor.{u1, u1, u1, max u1 u2} J _inst_2 (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.instCategoryPresheaf.{u1, u1, u2} C _inst_1 X)), (forall (j : J), TopCat.Presheaf.IsSheaf.{u1, u1, u2} C _inst_1 X (Prefunctor.obj.{succ u1, succ u1, u1, max u2 u1} J (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} J (CategoryTheory.Category.toCategoryStruct.{u1, u1} J _inst_2)) (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (CategoryTheory.CategoryStruct.toQuiver.{u1, max u2 u1} (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (CategoryTheory.Category.toCategoryStruct.{u1, max u2 u1} (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.instCategoryPresheaf.{u1, u1, u2} C _inst_1 X))) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, max u2 u1} J _inst_2 (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.instCategoryPresheaf.{u1, u1, u2} C _inst_1 X) F) j)) -> (forall {c : CategoryTheory.Limits.Cone.{u1, u1, u1, max u2 u1} J _inst_2 (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.instCategoryPresheaf.{u1, u1, u2} C _inst_1 X) F}, (CategoryTheory.Limits.IsLimit.{u1, u1, u1, max u2 u1} J _inst_2 (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.instCategoryPresheaf.{u1, u1, u2} C _inst_1 X) F c) -> (TopCat.Presheaf.IsSheaf.{u1, u1, u2} C _inst_1 X (CategoryTheory.Limits.Cone.pt.{u1, u1, u1, max u2 u1} J _inst_2 (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.instCategoryPresheaf.{u1, u1, u2} C _inst_1 X) F c)))
+Case conversion may be inaccurate. Consider using '#align Top.is_sheaf_of_is_limit TopCat.isSheaf_of_isLimitₓ'. -/
 theorem isSheaf_of_isLimit [HasLimits C] {X : TopCat} (F : J ⥤ Presheaf.{v} C X)
     (H : ∀ j, (F.obj j).IsSheaf) {c : Cone F} (hc : IsLimit c) : c.pt.IsSheaf :=
   by
@@ -54,6 +60,12 @@ theorem isSheaf_of_isLimit [HasLimits C] {X : TopCat} (F : J ⥤ Presheaf.{v} C
       (limit F').2
 #align Top.is_sheaf_of_is_limit TopCat.isSheaf_of_isLimit
 
+/- warning: Top.limit_is_sheaf -> TopCat.limit_isSheaf is a dubious translation:
+lean 3 declaration is
+  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] {J : Type.{u1}} [_inst_2 : CategoryTheory.SmallCategory.{u1} J] [_inst_3 : CategoryTheory.Limits.HasLimits.{u1, u2} C _inst_1] {X : TopCat.{u1}} (F : CategoryTheory.Functor.{u1, u1, u1, max u2 u1} J _inst_2 (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.Presheaf.category.{u1, u1, u2} C _inst_1 X)), (forall (j : J), TopCat.Presheaf.IsSheaf.{u1, u1, u2} C _inst_1 X (CategoryTheory.Functor.obj.{u1, u1, u1, max u2 u1} J _inst_2 (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.Presheaf.category.{u1, u1, u2} C _inst_1 X) F j)) -> (TopCat.Presheaf.IsSheaf.{u1, u1, u2} C _inst_1 X (CategoryTheory.Limits.limit.{u1, u1, u1, max u2 u1} J _inst_2 (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.Presheaf.category.{u1, u1, u2} C _inst_1 X) F (CategoryTheory.Limits.hasLimitOfHasLimitsOfShape.{u1, u1, u1, max u2 u1} (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.Presheaf.category.{u1, u1, u2} C _inst_1 X) J _inst_2 (CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits.{u1, u1, u1, max u2 u1} (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.Presheaf.category.{u1, u1, u2} C _inst_1 X) J _inst_2 (TopCat.Presheaf.CategoryTheory.Limits.hasLimits.{u1, u2} C _inst_1 _inst_3 X)) F)))
+but is expected to have type
+  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] {J : Type.{u1}} [_inst_2 : CategoryTheory.SmallCategory.{u1} J] [_inst_3 : CategoryTheory.Limits.HasLimits.{u1, u2} C _inst_1] {X : TopCat.{u1}} (F : CategoryTheory.Functor.{u1, u1, u1, max u1 u2} J _inst_2 (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.instCategoryPresheaf.{u1, u1, u2} C _inst_1 X)), (forall (j : J), TopCat.Presheaf.IsSheaf.{u1, u1, u2} C _inst_1 X (Prefunctor.obj.{succ u1, succ u1, u1, max u2 u1} J (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} J (CategoryTheory.Category.toCategoryStruct.{u1, u1} J _inst_2)) (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (CategoryTheory.CategoryStruct.toQuiver.{u1, max u2 u1} (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (CategoryTheory.Category.toCategoryStruct.{u1, max u2 u1} (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.instCategoryPresheaf.{u1, u1, u2} C _inst_1 X))) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, max u2 u1} J _inst_2 (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.instCategoryPresheaf.{u1, u1, u2} C _inst_1 X) F) j)) -> (TopCat.Presheaf.IsSheaf.{u1, u1, u2} C _inst_1 X (CategoryTheory.Limits.limit.{u1, u1, u1, max u2 u1} J _inst_2 (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.instCategoryPresheaf.{u1, u1, u2} C _inst_1 X) F (CategoryTheory.Limits.hasLimitOfHasLimitsOfShape.{u1, u1, u1, max u2 u1} (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.instCategoryPresheaf.{u1, u1, u2} C _inst_1 X) J _inst_2 (CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits.{u1, u1, u1, max u2 u1} (TopCat.Presheaf.{u1, u1, u2} C _inst_1 X) (TopCat.instCategoryPresheaf.{u1, u1, u2} C _inst_1 X) J _inst_2 (TopCat.instHasLimitsPresheafInstCategoryPresheaf.{u1, u2} C _inst_1 _inst_3 X)) F)))
+Case conversion may be inaccurate. Consider using '#align Top.limit_is_sheaf TopCat.limit_isSheafₓ'. -/
 theorem limit_isSheaf [HasLimits C] {X : TopCat} (F : J ⥤ Presheaf.{v} C X)
     (H : ∀ j, (F.obj j).IsSheaf) : (limit F).IsSheaf :=
   isSheaf_of_isLimit F H (limit.isLimit F)