From e9eb901c11fb1925dfc3c03995b5026a177dd26e Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 30 Jun 2023 06:08:19 +0000 Subject: [PATCH] chore: reorder universes in ConcreteCategory (#5605) Co-authored-by: Scott Morrison --- Mathlib/AlgebraicGeometry/AffineScheme.lean | 4 ++-- Mathlib/CategoryTheory/ConcreteCategory/Basic.lean | 14 +++++++------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean index 182053da3d71d..ebaee42972b3d 100644 --- a/Mathlib/AlgebraicGeometry/AffineScheme.lean +++ b/Mathlib/AlgebraicGeometry/AffineScheme.lean @@ -630,7 +630,7 @@ theorem IsAffineOpen.isLocalization_stalk_aux {X : Scheme} (U : Opens X) rw [eqToHom_trans] #align algebraic_geometry.is_affine_open.is_localization_stalk_aux AlgebraicGeometry.IsAffineOpen.isLocalization_stalk_aux -set_option maxHeartbeats 1643256 in +set_option maxHeartbeats 3200000 in theorem IsAffineOpen.isLocalization_stalk_aux' {X : Scheme} {U : Opens X} (hU : IsAffineOpen U) (y : PrimeSpectrum (X.presheaf.obj <| op U)) (hy : hU.fromSpec.1.base y ∈ U) : hU.fromSpec.val.c.app (op U) ≫ (Scheme.Spec.obj <| op (X.presheaf.obj <| op U)).presheaf.germ @@ -661,7 +661,7 @@ theorem IsAffineOpen.isLocalization_stalk_aux' {X : Scheme} {U : Opens X} (hU : rw [Category.id_comp] rfl -set_option maxHeartbeats 420000 in +set_option maxHeartbeats 800000 in theorem IsAffineOpen.isLocalization_stalk' {X : Scheme} {U : Opens X} (hU : IsAffineOpen U) (y : PrimeSpectrum (X.presheaf.obj <| op U)) (hy : hU.fromSpec.1.base y ∈ U) : haveI : IsAffine _ := hU diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean index 80478de3de955..4729862737316 100644 --- a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean +++ b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison, Johannes Hölzl, Reid Barton, Sean Leather, Yury Kudryashov ! This file was ported from Lean 3 source module category_theory.concrete_category.basic -! leanprover-community/mathlib commit 05b820ec79b3c98a7dbf1cb32e181584166da2ca +! leanprover-community/mathlib commit 311ef8c4b4ae2804ea76b8a611bc5ea1d9c16872 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -41,7 +41,7 @@ related work. -/ -universe w w' v v' u +universe w w' v v' u u' namespace CategoryTheory @@ -68,13 +68,13 @@ attribute [instance] ConcreteCategory.forget_faithful /-- The forgetful functor from a concrete category to `Type u`. -/ @[reducible] -def forget (C : Type v) [Category C] [ConcreteCategory.{u} C] : C ⥤ Type u := +def forget (C : Type u) [Category.{v} C] [ConcreteCategory.{w} C] : C ⥤ Type w := ConcreteCategory.forget #align category_theory.forget CategoryTheory.forget -- this is reducible because we want `forget (Type u)` to unfold to `𝟭 _` @[reducible] -instance ConcreteCategory.types : ConcreteCategory (Type u) where +instance ConcreteCategory.types : ConcreteCategory.{u, u, u+1} (Type u) where forget := 𝟭 _ #align category_theory.concrete_category.types CategoryTheory.ConcreteCategory.types @@ -86,8 +86,8 @@ You can use it on particular examples as: instance : HasCoeToSort X := ConcreteCategory.hasCoeToSort X ``` -/ -def ConcreteCategory.hasCoeToSort (C : Type v) [Category C] [ConcreteCategory C] : - CoeSort C (Type u) where +def ConcreteCategory.hasCoeToSort (C : Type u) [Category.{v} C] [ConcreteCategory.{w} C] : + CoeSort C (Type w) where coe := fun X => (forget C).obj X #align category_theory.concrete_category.has_coe_to_sort CategoryTheory.ConcreteCategory.hasCoeToSort @@ -95,7 +95,7 @@ section attribute [local instance] ConcreteCategory.hasCoeToSort -variable {C : Type v} [Category C] [ConcreteCategory.{w} C] +variable {C : Type u} [Category.{v} C] [ConcreteCategory.{w} C] -- Porting note: forget_obj_eq_coe has become a syntactic tautology. #noalign category_theory.forget_obj_eq_coe