From f29e26a7672245118e279bc5779baa0e7ac96b58 Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Sun, 14 May 2023 04:43:39 +0000 Subject: [PATCH] bump to nightly-2023-05-14-04 mathlib commit https://github.com/leanprover-community/mathlib/commit/e3fb84046afd187b710170887195d50bada934ee --- Mathbin/Algebra/Category/Algebra/Limits.lean | 8 +- Mathbin/Algebra/Category/Ring/Basic.lean | 246 +++++++++++++----- .../Algebra/Category/Ring/Constructions.lean | 2 +- .../Category/Ring/FilteredColimits.lean | 146 ++++++----- Mathbin/Algebra/Category/Ring/Instances.lean | 2 +- Mathbin/Algebra/Category/Ring/Limits.lean | 236 +++++++++-------- Mathbin/AlgebraicGeometry/AffineScheme.lean | 4 +- .../AlgebraicGeometry/LocallyRingedSpace.lean | 2 +- .../LocallyRingedSpace/HasColimits.lean | 2 +- .../Morphisms/RingHomProperties.lean | 4 +- Mathbin/AlgebraicGeometry/OpenImmersion.lean | 2 +- Mathbin/AlgebraicGeometry/Properties.lean | 10 +- Mathbin/AlgebraicGeometry/Spec.lean | 4 +- Mathbin/AlgebraicGeometry/StructureSheaf.lean | 6 +- Mathbin/RingTheory/RingHomProperties.lean | 8 +- lake-manifest.json | 8 +- lakefile.lean | 4 +- 17 files changed, 417 insertions(+), 277 deletions(-) diff --git a/Mathbin/Algebra/Category/Algebra/Limits.lean b/Mathbin/Algebra/Category/Algebra/Limits.lean index 967dcaeaf0..91ad1c34e8 100644 --- a/Mathbin/Algebra/Category/Algebra/Limits.lean +++ b/Mathbin/Algebra/Category/Algebra/Limits.lean @@ -53,8 +53,8 @@ instance algebraObj (F : J ⥤ AlgebraCat.{max v w} R) (j) : -/ def sectionsSubalgebra (F : J ⥤ AlgebraCat.{max v w} R) : Subalgebra R (∀ j, F.obj j) := { - SemiRing.sectionsSubsemiring - (F ⋙ forget₂ (AlgebraCat R) RingCat.{max v w} ⋙ forget₂ RingCat SemiRing.{max v w}) with + SemiRingCat.sectionsSubsemiring + (F ⋙ forget₂ (AlgebraCat R) RingCat.{max v w} ⋙ forget₂ RingCat SemiRingCat.{max v w}) with algebraMap_mem' := fun r j j' f => (F.map f).commutes r } #align Algebra.sections_subalgebra AlgebraCat.sectionsSubalgebra @@ -81,8 +81,8 @@ def limitπAlgHom (F : J ⥤ AlgebraCat.{max v w} R) (j) : (Types.limitCone (F ⋙ forget (AlgebraCat R))).pt →ₐ[R] (F ⋙ forget (AlgebraCat.{max v w} R)).obj j := { - SemiRing.limitπRingHom - (F ⋙ forget₂ (AlgebraCat R) RingCat.{max v w} ⋙ forget₂ RingCat SemiRing.{max v w}) j with + SemiRingCat.limitπRingHom + (F ⋙ forget₂ (AlgebraCat R) RingCat.{max v w} ⋙ forget₂ RingCat SemiRingCat.{max v w}) j with commutes' := fun r => rfl } #align Algebra.limit_π_alg_hom AlgebraCat.limitπAlgHom diff --git a/Mathbin/Algebra/Category/Ring/Basic.lean b/Mathbin/Algebra/Category/Ring/Basic.lean index c0f39a9013..54d2e5061a 100644 --- a/Mathbin/Algebra/Category/Ring/Basic.lean +++ b/Mathbin/Algebra/Category/Ring/Basic.lean @@ -29,75 +29,99 @@ universe u v open CategoryTheory +#print SemiRingCat /- /-- The category of semirings. -/ -def SemiRing : Type (u + 1) := +def SemiRingCat : Type (u + 1) := Bundled Semiring -#align SemiRing SemiRing +#align SemiRing SemiRingCat +-/ -namespace SemiRing +namespace SemiRingCat +#print SemiRingCat.AssocRingHom /- /-- `ring_hom` doesn't actually assume associativity. This alias is needed to make the category theory machinery work. We use the same trick in `category_theory.Mon.assoc_monoid_hom`. -/ abbrev AssocRingHom (M N : Type _) [Semiring M] [Semiring N] := RingHom M N -#align SemiRing.assoc_ring_hom SemiRing.AssocRingHom +#align SemiRing.assoc_ring_hom SemiRingCat.AssocRingHom +-/ +#print SemiRingCat.bundledHom /- instance bundledHom : BundledHom AssocRingHom := ⟨fun M N [Semiring M] [Semiring N] => @RingHom.toFun M N _ _, fun M [Semiring M] => @RingHom.id M _, fun M N P [Semiring M] [Semiring N] [Semiring P] => @RingHom.comp M N P _ _ _, fun M N [Semiring M] [Semiring N] => @RingHom.coe_inj M N _ _⟩ -#align SemiRing.bundled_hom SemiRing.bundledHom +#align SemiRing.bundled_hom SemiRingCat.bundledHom +-/ -deriving instance LargeCategory, ConcreteCategory for SemiRing +deriving instance LargeCategory, ConcreteCategory for SemiRingCat -instance : CoeSort SemiRing (Type _) := +instance : CoeSort SemiRingCat (Type _) := Bundled.hasCoeToSort +#print SemiRingCat.of /- /-- Construct a bundled SemiRing from the underlying type and typeclass. -/ -def of (R : Type u) [Semiring R] : SemiRing := +def of (R : Type u) [Semiring R] : SemiRingCat := Bundled.of R -#align SemiRing.of SemiRing.of +#align SemiRing.of SemiRingCat.of +-/ +#print SemiRingCat.ofHom /- /-- Typecheck a `ring_hom` as a morphism in `SemiRing`. -/ def ofHom {R S : Type u} [Semiring R] [Semiring S] (f : R →+* S) : of R ⟶ of S := f -#align SemiRing.of_hom SemiRing.ofHom +#align SemiRing.of_hom SemiRingCat.ofHom +-/ +/- warning: SemiRing.of_hom_apply -> SemiRingCat.ofHom_apply is a dubious translation: +lean 3 declaration is + forall {R : Type.{u1}} {S : Type.{u1}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u1} S] (f : RingHom.{u1, u1} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} S _inst_2)) (x : R), Eq.{succ u1} (coeSort.{succ (succ u1), succ (succ u1)} (CategoryTheory.Bundled.{u1, u1} Semiring.{u1}) Type.{u1} (CategoryTheory.Bundled.hasCoeToSort.{u1, u1} Semiring.{u1}) (SemiRingCat.of.{u1} S _inst_2)) (coeFn.{succ u1, succ u1} (Quiver.Hom.{succ u1, succ u1} SemiRingCat.{u1} (CategoryTheory.CategoryStruct.toQuiver.{u1, succ u1} SemiRingCat.{u1} (CategoryTheory.Category.toCategoryStruct.{u1, succ u1} SemiRingCat.{u1} SemiRingCat.largeCategory.{u1})) (SemiRingCat.of.{u1} R _inst_1) (SemiRingCat.of.{u1} S _inst_2)) (fun (_x : RingHom.{u1, u1} (coeSort.{succ (succ u1), succ (succ u1)} (CategoryTheory.Bundled.{u1, u1} Semiring.{u1}) Type.{u1} (CategoryTheory.Bundled.hasCoeToSort.{u1, u1} Semiring.{u1}) (SemiRingCat.of.{u1} R _inst_1)) (coeSort.{succ (succ u1), succ (succ u1)} (CategoryTheory.Bundled.{u1, u1} Semiring.{u1}) Type.{u1} (CategoryTheory.Bundled.hasCoeToSort.{u1, u1} Semiring.{u1}) (SemiRingCat.of.{u1} S _inst_2)) (Semiring.toNonAssocSemiring.{u1} (coeSort.{succ (succ u1), succ (succ u1)} (CategoryTheory.Bundled.{u1, u1} Semiring.{u1}) Type.{u1} (CategoryTheory.Bundled.hasCoeToSort.{u1, u1} Semiring.{u1}) (SemiRingCat.of.{u1} R _inst_1)) (CategoryTheory.Bundled.str.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1))) (Semiring.toNonAssocSemiring.{u1} (coeSort.{succ (succ u1), succ (succ u1)} (CategoryTheory.Bundled.{u1, u1} Semiring.{u1}) Type.{u1} (CategoryTheory.Bundled.hasCoeToSort.{u1, u1} Semiring.{u1}) (SemiRingCat.of.{u1} S _inst_2)) (CategoryTheory.Bundled.str.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)))) => (coeSort.{succ (succ u1), succ (succ u1)} (CategoryTheory.Bundled.{u1, u1} Semiring.{u1}) Type.{u1} (CategoryTheory.Bundled.hasCoeToSort.{u1, u1} Semiring.{u1}) (SemiRingCat.of.{u1} R _inst_1)) -> (coeSort.{succ (succ u1), succ (succ u1)} (CategoryTheory.Bundled.{u1, u1} Semiring.{u1}) Type.{u1} (CategoryTheory.Bundled.hasCoeToSort.{u1, u1} Semiring.{u1}) (SemiRingCat.of.{u1} S _inst_2))) (RingHom.hasCoeToFun.{u1, u1} (coeSort.{succ (succ u1), succ (succ u1)} (CategoryTheory.Bundled.{u1, u1} Semiring.{u1}) Type.{u1} (CategoryTheory.Bundled.hasCoeToSort.{u1, u1} Semiring.{u1}) (SemiRingCat.of.{u1} R _inst_1)) (coeSort.{succ (succ u1), succ (succ u1)} (CategoryTheory.Bundled.{u1, u1} Semiring.{u1}) Type.{u1} (CategoryTheory.Bundled.hasCoeToSort.{u1, u1} Semiring.{u1}) (SemiRingCat.of.{u1} S _inst_2)) (Semiring.toNonAssocSemiring.{u1} (coeSort.{succ (succ u1), succ (succ u1)} (CategoryTheory.Bundled.{u1, u1} Semiring.{u1}) Type.{u1} (CategoryTheory.Bundled.hasCoeToSort.{u1, u1} Semiring.{u1}) (SemiRingCat.of.{u1} R _inst_1)) (CategoryTheory.Bundled.str.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1))) (Semiring.toNonAssocSemiring.{u1} (coeSort.{succ (succ u1), succ (succ u1)} (CategoryTheory.Bundled.{u1, u1} Semiring.{u1}) Type.{u1} (CategoryTheory.Bundled.hasCoeToSort.{u1, u1} Semiring.{u1}) (SemiRingCat.of.{u1} S _inst_2)) (CategoryTheory.Bundled.str.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)))) (SemiRingCat.ofHom.{u1} R S _inst_1 _inst_2 f) x) (coeFn.{succ u1, succ u1} (RingHom.{u1, u1} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} S _inst_2)) (fun (_x : RingHom.{u1, u1} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} S _inst_2)) => R -> S) (RingHom.hasCoeToFun.{u1, u1} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} S _inst_2)) f x) +but is expected to have type + forall {R : Type.{u1}} {S : Type.{u1}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u1} S] (f : RingHom.{u1, u1} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} S _inst_2)) (x : R), Eq.{succ u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) => CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) x) (FunLike.coe.{succ u1, succ u1, succ u1} (RingHom.{u1, u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (Semiring.toNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (SemiRingCat.instSemiringα.{u1} (SemiRingCat.of.{u1} R _inst_1))) (Semiring.toNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (SemiRingCat.instSemiringα.{u1} (SemiRingCat.of.{u1} S _inst_2)))) (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (fun (_x : CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) => CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) _x) (MulHomClass.toFunLike.{u1, u1, u1} (RingHom.{u1, u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (Semiring.toNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (SemiRingCat.instSemiringα.{u1} (SemiRingCat.of.{u1} R _inst_1))) (Semiring.toNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (SemiRingCat.instSemiringα.{u1} (SemiRingCat.of.{u1} S _inst_2)))) (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (NonUnitalNonAssocSemiring.toMul.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (SemiRingCat.instSemiringα.{u1} (SemiRingCat.of.{u1} R _inst_1))))) (NonUnitalNonAssocSemiring.toMul.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (Semiring.toNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (SemiRingCat.instSemiringα.{u1} (SemiRingCat.of.{u1} S _inst_2))))) (NonUnitalRingHomClass.toMulHomClass.{u1, u1, u1} (RingHom.{u1, u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (Semiring.toNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (SemiRingCat.instSemiringα.{u1} (SemiRingCat.of.{u1} R _inst_1))) (Semiring.toNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (SemiRingCat.instSemiringα.{u1} (SemiRingCat.of.{u1} S _inst_2)))) (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (SemiRingCat.instSemiringα.{u1} (SemiRingCat.of.{u1} R _inst_1)))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (Semiring.toNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (SemiRingCat.instSemiringα.{u1} (SemiRingCat.of.{u1} S _inst_2)))) (RingHomClass.toNonUnitalRingHomClass.{u1, u1, u1} (RingHom.{u1, u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (Semiring.toNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (SemiRingCat.instSemiringα.{u1} (SemiRingCat.of.{u1} R _inst_1))) (Semiring.toNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (SemiRingCat.instSemiringα.{u1} (SemiRingCat.of.{u1} S _inst_2)))) (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (Semiring.toNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (SemiRingCat.instSemiringα.{u1} (SemiRingCat.of.{u1} R _inst_1))) (Semiring.toNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (SemiRingCat.instSemiringα.{u1} (SemiRingCat.of.{u1} S _inst_2))) (RingHom.instRingHomClassRingHom.{u1, u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (Semiring.toNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} R _inst_1)) (SemiRingCat.instSemiringα.{u1} (SemiRingCat.of.{u1} R _inst_1))) (Semiring.toNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Semiring.{u1} (SemiRingCat.of.{u1} S _inst_2)) (SemiRingCat.instSemiringα.{u1} (SemiRingCat.of.{u1} S _inst_2))))))) (SemiRingCat.ofHom.{u1} R S _inst_1 _inst_2 f) x) (FunLike.coe.{succ u1, succ u1, succ u1} (RingHom.{u1, u1} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} S _inst_2)) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S) _x) (MulHomClass.toFunLike.{u1, u1, u1} (RingHom.{u1, u1} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} S _inst_2)) R S (NonUnitalNonAssocSemiring.toMul.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1))) (NonUnitalNonAssocSemiring.toMul.{u1} S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} S (Semiring.toNonAssocSemiring.{u1} S _inst_2))) (NonUnitalRingHomClass.toMulHomClass.{u1, u1, u1} (RingHom.{u1, u1} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} S _inst_2)) R S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} S (Semiring.toNonAssocSemiring.{u1} S _inst_2)) (RingHomClass.toNonUnitalRingHomClass.{u1, u1, u1} (RingHom.{u1, u1} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} S _inst_2)) R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} S _inst_2) (RingHom.instRingHomClassRingHom.{u1, u1} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u1} S _inst_2))))) f x) +Case conversion may be inaccurate. Consider using '#align SemiRing.of_hom_apply SemiRingCat.ofHom_applyₓ'. -/ @[simp] theorem ofHom_apply {R S : Type u} [Semiring R] [Semiring S] (f : R →+* S) (x : R) : ofHom f x = f x := rfl -#align SemiRing.of_hom_apply SemiRing.ofHom_apply +#align SemiRing.of_hom_apply SemiRingCat.ofHom_apply -instance : Inhabited SemiRing := +instance : Inhabited SemiRingCat := ⟨of PUnit⟩ -instance (R : SemiRing) : Semiring R := +instance (R : SemiRingCat) : Semiring R := R.str +#print SemiRingCat.coe_of /- @[simp] -theorem coe_of (R : Type u) [Semiring R] : (SemiRing.of R : Type u) = R := +theorem coe_of (R : Type u) [Semiring R] : (SemiRingCat.of R : Type u) = R := rfl -#align SemiRing.coe_of SemiRing.coe_of +#align SemiRing.coe_of SemiRingCat.coe_of +-/ -instance hasForgetToMon : HasForget₂ SemiRing MonCat := +#print SemiRingCat.hasForgetToMonCat /- +instance hasForgetToMonCat : HasForget₂ SemiRingCat MonCat := BundledHom.mkHasForget₂ (fun R hR => @MonoidWithZero.toMonoid R (@Semiring.toMonoidWithZero R hR)) (fun R₁ R₂ => RingHom.toMonoidHom) fun _ _ _ => rfl -#align SemiRing.has_forget_to_Mon SemiRing.hasForgetToMon +#align SemiRing.has_forget_to_Mon SemiRingCat.hasForgetToMonCat +-/ -instance hasForgetToAddCommMon : HasForget₂ SemiRing AddCommMonCat +#print SemiRingCat.hasForgetToAddCommMonCat /- +instance hasForgetToAddCommMonCat : HasForget₂ SemiRingCat AddCommMonCat where-- can't use bundled_hom.mk_has_forget₂, since AddCommMon is an induced category forget₂ := { obj := fun R => AddCommMonCat.of R map := fun R₁ R₂ f => RingHom.toAddMonoidHom f } -#align SemiRing.has_forget_to_AddCommMon SemiRing.hasForgetToAddCommMon +#align SemiRing.has_forget_to_AddCommMon SemiRingCat.hasForgetToAddCommMonCat +-/ -end SemiRing +end SemiRingCat +#print RingCat /- /-- The category of rings. -/ def RingCat : Type (u + 1) := Bundled Ring #align Ring RingCat +-/ namespace RingCat @@ -110,15 +134,19 @@ deriving instance «./././Mathport/Syntax/Translate/Command.lean:42:9: unsupported derive handler λ Ring, has_coe_to_sort[has_coe_to_sort] Ring (Type*)», LargeCategory, ConcreteCategory for RingCat +#print RingCat.of /- /-- Construct a bundled Ring from the underlying type and typeclass. -/ def of (R : Type u) [Ring R] : RingCat := Bundled.of R #align Ring.of RingCat.of +-/ +#print RingCat.ofHom /- /-- Typecheck a `ring_hom` as a morphism in `Ring`. -/ def ofHom {R S : Type u} [Ring R] [Ring S] (f : R →+* S) : of R ⟶ of S := f #align Ring.of_hom RingCat.ofHom +-/ @[simp] theorem ofHom_apply {R S : Type u} [Ring R] [Ring S] (f : R →+* S) (x : R) : ofHom f x = f x := @@ -131,82 +159,109 @@ instance : Inhabited RingCat := instance (R : RingCat) : Ring R := R.str +#print RingCat.coe_of /- @[simp] theorem coe_of (R : Type u) [Ring R] : (RingCat.of R : Type u) = R := rfl #align Ring.coe_of RingCat.coe_of +-/ -instance hasForgetToSemiRing : HasForget₂ RingCat SemiRing := +#print RingCat.hasForgetToSemiRingCat /- +instance hasForgetToSemiRingCat : HasForget₂ RingCat SemiRingCat := BundledHom.forget₂ _ _ -#align Ring.has_forget_to_SemiRing RingCat.hasForgetToSemiRing +#align Ring.has_forget_to_SemiRing RingCat.hasForgetToSemiRingCat +-/ -instance hasForgetToAddCommGroup : HasForget₂ RingCat AddCommGroupCat +#print RingCat.hasForgetToAddCommGroupCat /- +instance hasForgetToAddCommGroupCat : HasForget₂ RingCat AddCommGroupCat where-- can't use bundled_hom.mk_has_forget₂, since AddCommGroup is an induced category forget₂ := { obj := fun R => AddCommGroupCat.of R map := fun R₁ R₂ f => RingHom.toAddMonoidHom f } -#align Ring.has_forget_to_AddCommGroup RingCat.hasForgetToAddCommGroup +#align Ring.has_forget_to_AddCommGroup RingCat.hasForgetToAddCommGroupCat +-/ end RingCat +#print CommSemiRingCat /- /-- The category of commutative semirings. -/ -def CommSemiRing : Type (u + 1) := +def CommSemiRingCat : Type (u + 1) := Bundled CommSemiring -#align CommSemiRing CommSemiRing +#align CommSemiRing CommSemiRingCat +-/ -namespace CommSemiRing +namespace CommSemiRingCat instance : BundledHom.ParentProjection @CommSemiring.toSemiring := ⟨⟩ -deriving instance LargeCategory, ConcreteCategory for CommSemiRing +deriving instance LargeCategory, ConcreteCategory for CommSemiRingCat -instance : CoeSort CommSemiRing (Type _) := +instance : CoeSort CommSemiRingCat (Type _) := Bundled.hasCoeToSort +#print CommSemiRing.of /- /-- Construct a bundled CommSemiRing from the underlying type and typeclass. -/ -def of (R : Type u) [CommSemiring R] : CommSemiRing := +def of (R : Type u) [CommSemiring R] : CommSemiRingCat := Bundled.of R #align CommSemiRing.of CommSemiRing.of +-/ +#print CommSemiRing.ofHom /- /-- Typecheck a `ring_hom` as a morphism in `CommSemiRing`. -/ def ofHom {R S : Type u} [CommSemiring R] [CommSemiring S] (f : R →+* S) : of R ⟶ of S := f #align CommSemiRing.of_hom CommSemiRing.ofHom +-/ +/- warning: CommSemiRing.of_hom_apply clashes with [anonymous] -> [anonymous] +warning: CommSemiRing.of_hom_apply -> [anonymous] is a dubious translation: +lean 3 declaration is + forall {R : Type.{u}} {S : Type.{u}} [_inst_1 : CommSemiring.{u} R] [_inst_2 : CommSemiring.{u} S] (f : RingHom.{u, u} R S (Semiring.toNonAssocSemiring.{u} R (CommSemiring.toSemiring.{u} R _inst_1)) (Semiring.toNonAssocSemiring.{u} S (CommSemiring.toSemiring.{u} S _inst_2))) (x : R), Eq.{succ u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommSemiring.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommSemiring.{u}) (CommSemiRing.of.{u} S _inst_2)) (coeFn.{succ u, succ u} (Quiver.Hom.{succ u, succ u} CommSemiRingCat.{u} (CategoryTheory.CategoryStruct.toQuiver.{u, succ u} CommSemiRingCat.{u} (CategoryTheory.Category.toCategoryStruct.{u, succ u} CommSemiRingCat.{u} CommSemiRingCat.largeCategory.{u})) (CommSemiRing.of.{u} R _inst_1) (CommSemiRing.of.{u} S _inst_2)) (fun (_x : RingHom.{u, u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommSemiring.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommSemiring.{u}) (CommSemiRing.of.{u} R _inst_1)) (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommSemiring.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommSemiring.{u}) (CommSemiRing.of.{u} S _inst_2)) (Semiring.toNonAssocSemiring.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommSemiring.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommSemiring.{u}) (CommSemiRing.of.{u} R _inst_1)) (CommSemiring.toSemiring.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommSemiring.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommSemiring.{u}) (CommSemiRing.of.{u} R _inst_1)) (CategoryTheory.Bundled.str.{u, u} CommSemiring.{u} (CommSemiRing.of.{u} R _inst_1)))) (Semiring.toNonAssocSemiring.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommSemiring.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommSemiring.{u}) (CommSemiRing.of.{u} S _inst_2)) (CommSemiring.toSemiring.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommSemiring.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommSemiring.{u}) (CommSemiRing.of.{u} S _inst_2)) (CategoryTheory.Bundled.str.{u, u} CommSemiring.{u} (CommSemiRing.of.{u} S _inst_2))))) => (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommSemiring.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommSemiring.{u}) (CommSemiRing.of.{u} R _inst_1)) -> (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommSemiring.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommSemiring.{u}) (CommSemiRing.of.{u} S _inst_2))) (RingHom.hasCoeToFun.{u, u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommSemiring.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommSemiring.{u}) (CommSemiRing.of.{u} R _inst_1)) (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommSemiring.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommSemiring.{u}) (CommSemiRing.of.{u} S _inst_2)) (Semiring.toNonAssocSemiring.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommSemiring.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommSemiring.{u}) (CommSemiRing.of.{u} R _inst_1)) (CommSemiring.toSemiring.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommSemiring.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommSemiring.{u}) (CommSemiRing.of.{u} R _inst_1)) (CategoryTheory.Bundled.str.{u, u} CommSemiring.{u} (CommSemiRing.of.{u} R _inst_1)))) (Semiring.toNonAssocSemiring.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommSemiring.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommSemiring.{u}) (CommSemiRing.of.{u} S _inst_2)) (CommSemiring.toSemiring.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommSemiring.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommSemiring.{u}) (CommSemiRing.of.{u} S _inst_2)) (CategoryTheory.Bundled.str.{u, u} CommSemiring.{u} (CommSemiRing.of.{u} S _inst_2))))) (CommSemiRing.ofHom.{u} R S _inst_1 _inst_2 f) x) (coeFn.{succ u, succ u} (RingHom.{u, u} R S (Semiring.toNonAssocSemiring.{u} R (CommSemiring.toSemiring.{u} R _inst_1)) (Semiring.toNonAssocSemiring.{u} S (CommSemiring.toSemiring.{u} S _inst_2))) (fun (_x : RingHom.{u, u} R S (Semiring.toNonAssocSemiring.{u} R (CommSemiring.toSemiring.{u} R _inst_1)) (Semiring.toNonAssocSemiring.{u} S (CommSemiring.toSemiring.{u} S _inst_2))) => R -> S) (RingHom.hasCoeToFun.{u, u} R S (Semiring.toNonAssocSemiring.{u} R (CommSemiring.toSemiring.{u} R _inst_1)) (Semiring.toNonAssocSemiring.{u} S (CommSemiring.toSemiring.{u} S _inst_2))) f x) +but is expected to have type + forall {R : Type.{u}} {S : Type.{v}}, (Nat -> R -> S) -> Nat -> (List.{u} R) -> (List.{v} S) +Case conversion may be inaccurate. Consider using '#align CommSemiRing.of_hom_apply [anonymous]ₓ'. -/ @[simp] -theorem ofHom_apply {R S : Type u} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : R) : +theorem [anonymous] {R S : Type u} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : R) : ofHom f x = f x := rfl -#align CommSemiRing.of_hom_apply CommSemiRing.ofHom_apply +#align CommSemiRing.of_hom_apply [anonymous] -instance : Inhabited CommSemiRing := +instance : Inhabited CommSemiRingCat := ⟨of PUnit⟩ -instance (R : CommSemiRing) : CommSemiring R := +instance (R : CommSemiRingCat) : CommSemiring R := R.str +#print CommSemiRing.coe_of /- @[simp] theorem coe_of (R : Type u) [CommSemiring R] : (CommSemiRing.of R : Type u) = R := rfl #align CommSemiRing.coe_of CommSemiRing.coe_of +-/ -instance hasForgetToSemiRing : HasForget₂ CommSemiRing SemiRing := +#print CommSemiRing.hasForgetToSemiRingCat /- +instance hasForgetToSemiRingCat : HasForget₂ CommSemiRingCat SemiRingCat := BundledHom.forget₂ _ _ -#align CommSemiRing.has_forget_to_SemiRing CommSemiRing.hasForgetToSemiRing +#align CommSemiRing.has_forget_to_SemiRing CommSemiRing.hasForgetToSemiRingCat +-/ +#print CommSemiRing.hasForgetToCommMonCat /- /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/ -instance hasForgetToCommMon : HasForget₂ CommSemiRing CommMonCat := - HasForget₂.mk' (fun R : CommSemiRing => CommMonCat.of R) (fun R => rfl) +instance hasForgetToCommMonCat : HasForget₂ CommSemiRingCat CommMonCat := + HasForget₂.mk' (fun R : CommSemiRingCat => CommMonCat.of R) (fun R => rfl) (fun R₁ R₂ f => f.toMonoidHom) (by tidy) -#align CommSemiRing.has_forget_to_CommMon CommSemiRing.hasForgetToCommMon +#align CommSemiRing.has_forget_to_CommMon CommSemiRing.hasForgetToCommMonCat +-/ -end CommSemiRing +end CommSemiRingCat +#print CommRingCat /- /-- The category of commutative rings. -/ def CommRingCat : Type (u + 1) := Bundled CommRing #align CommRing CommRingCat +-/ namespace CommRingCat @@ -218,21 +273,32 @@ deriving instance LargeCategory, ConcreteCategory for CommRingCat instance : CoeSort CommRingCat (Type _) := Bundled.hasCoeToSort +#print CommRingCat.of /- /-- Construct a bundled CommRing from the underlying type and typeclass. -/ def of (R : Type u) [CommRing R] : CommRingCat := Bundled.of R #align CommRing.of CommRingCat.of +-/ +#print CommRingCat.ofHom /- /-- Typecheck a `ring_hom` as a morphism in `CommRing`. -/ def ofHom {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : of R ⟶ of S := f #align CommRing.of_hom CommRingCat.ofHom +-/ +/- warning: CommRing.of_hom_apply clashes with [anonymous] -> [anonymous] +warning: CommRing.of_hom_apply -> [anonymous] is a dubious translation: +lean 3 declaration is + forall {R : Type.{u}} {S : Type.{u}} [_inst_1 : CommRing.{u} R] [_inst_2 : CommRing.{u} S] (f : RingHom.{u, u} R S (NonAssocRing.toNonAssocSemiring.{u} R (Ring.toNonAssocRing.{u} R (CommRing.toRing.{u} R _inst_1))) (NonAssocRing.toNonAssocSemiring.{u} S (Ring.toNonAssocRing.{u} S (CommRing.toRing.{u} S _inst_2)))) (x : R), Eq.{succ u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} S _inst_2)) (coeFn.{succ u, succ u} (Quiver.Hom.{succ u, succ u} CommRingCat.{u} (CategoryTheory.CategoryStruct.toQuiver.{u, succ u} CommRingCat.{u} (CategoryTheory.Category.toCategoryStruct.{u, succ u} CommRingCat.{u} CommRingCat.largeCategory.{u})) (CommRingCat.of.{u} R _inst_1) (CommRingCat.of.{u} S _inst_2)) (fun (_x : RingHom.{u, u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} R _inst_1)) (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} S _inst_2)) (Semiring.toNonAssocSemiring.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} R _inst_1)) (Ring.toSemiring.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} R _inst_1)) (CommRing.toRing.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} R _inst_1)) (CategoryTheory.Bundled.str.{u, u} CommRing.{u} (CommRingCat.of.{u} R _inst_1))))) (Semiring.toNonAssocSemiring.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} S _inst_2)) (Ring.toSemiring.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} S _inst_2)) (CommRing.toRing.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} S _inst_2)) (CategoryTheory.Bundled.str.{u, u} CommRing.{u} (CommRingCat.of.{u} S _inst_2)))))) => (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} R _inst_1)) -> (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} S _inst_2))) (RingHom.hasCoeToFun.{u, u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} R _inst_1)) (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} S _inst_2)) (Semiring.toNonAssocSemiring.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} R _inst_1)) (Ring.toSemiring.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} R _inst_1)) (CommRing.toRing.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} R _inst_1)) (CategoryTheory.Bundled.str.{u, u} CommRing.{u} (CommRingCat.of.{u} R _inst_1))))) (Semiring.toNonAssocSemiring.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} S _inst_2)) (Ring.toSemiring.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} S _inst_2)) (CommRing.toRing.{u} (coeSort.{succ (succ u), succ (succ u)} (CategoryTheory.Bundled.{u, u} CommRing.{u}) Type.{u} (CategoryTheory.Bundled.hasCoeToSort.{u, u} CommRing.{u}) (CommRingCat.of.{u} S _inst_2)) (CategoryTheory.Bundled.str.{u, u} CommRing.{u} (CommRingCat.of.{u} S _inst_2)))))) (CommRingCat.ofHom.{u} R S _inst_1 _inst_2 f) x) (coeFn.{succ u, succ u} (RingHom.{u, u} R S (NonAssocRing.toNonAssocSemiring.{u} R (Ring.toNonAssocRing.{u} R (CommRing.toRing.{u} R _inst_1))) (NonAssocRing.toNonAssocSemiring.{u} S (Ring.toNonAssocRing.{u} S (CommRing.toRing.{u} S _inst_2)))) (fun (_x : RingHom.{u, u} R S (NonAssocRing.toNonAssocSemiring.{u} R (Ring.toNonAssocRing.{u} R (CommRing.toRing.{u} R _inst_1))) (NonAssocRing.toNonAssocSemiring.{u} S (Ring.toNonAssocRing.{u} S (CommRing.toRing.{u} S _inst_2)))) => R -> S) (RingHom.hasCoeToFun.{u, u} R S (NonAssocRing.toNonAssocSemiring.{u} R (Ring.toNonAssocRing.{u} R (CommRing.toRing.{u} R _inst_1))) (NonAssocRing.toNonAssocSemiring.{u} S (Ring.toNonAssocRing.{u} S (CommRing.toRing.{u} S _inst_2)))) f x) +but is expected to have type + forall {R : Type.{u}} {S : Type.{v}}, (Nat -> R -> S) -> Nat -> (List.{u} R) -> (List.{v} S) +Case conversion may be inaccurate. Consider using '#align CommRing.of_hom_apply [anonymous]ₓ'. -/ @[simp] -theorem ofHom_apply {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (x : R) : +theorem [anonymous] {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (x : R) : ofHom f x = f x := rfl -#align CommRing.of_hom_apply CommRingCat.ofHom_apply +#align CommRing.of_hom_apply [anonymous] instance : Inhabited CommRingCat := ⟨of PUnit⟩ @@ -240,22 +306,28 @@ instance : Inhabited CommRingCat := instance (R : CommRingCat) : CommRing R := R.str +#print CommRingCat.coe_of /- @[simp] theorem coe_of (R : Type u) [CommRing R] : (CommRingCat.of R : Type u) = R := rfl #align CommRing.coe_of CommRingCat.coe_of +-/ -instance hasForgetToRing : HasForget₂ CommRingCat RingCat := +#print CommRingCat.hasForgetToRingCat /- +instance hasForgetToRingCat : HasForget₂ CommRingCat RingCat := BundledHom.forget₂ _ _ -#align CommRing.has_forget_to_Ring CommRingCat.hasForgetToRing +#align CommRing.has_forget_to_Ring CommRingCat.hasForgetToRingCat +-/ +#print CommRingCat.hasForgetToCommSemiRingCat /- /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/ -instance hasForgetToCommSemiRing : HasForget₂ CommRingCat CommSemiRing := +instance hasForgetToCommSemiRingCat : HasForget₂ CommRingCat CommSemiRingCat := HasForget₂.mk' (fun R : CommRingCat => CommSemiRing.of R) (fun R => rfl) (fun R₁ R₂ f => f) (by tidy) -#align CommRing.has_forget_to_CommSemiRing CommRingCat.hasForgetToCommSemiRing +#align CommRing.has_forget_to_CommSemiRing CommRingCat.hasForgetToCommSemiRingCat +-/ -instance : Full (forget₂ CommRingCat CommSemiRing) where preimage X Y f := f +instance : Full (forget₂ CommRingCat CommSemiRingCat) where preimage X Y f := f end CommRingCat @@ -269,28 +341,46 @@ namespace RingEquiv variable {X Y : Type u} +/- warning: ring_equiv.to_Ring_iso -> RingEquiv.toRingCatIso is a dubious translation: +lean 3 declaration is + forall {X : Type.{u1}} {Y : Type.{u1}} [_inst_1 : Ring.{u1} X] [_inst_2 : Ring.{u1} Y], (RingEquiv.{u1, u1} X Y (Distrib.toHasMul.{u1} X (Ring.toDistrib.{u1} X _inst_1)) (Distrib.toHasAdd.{u1} X (Ring.toDistrib.{u1} X _inst_1)) (Distrib.toHasMul.{u1} Y (Ring.toDistrib.{u1} Y _inst_2)) (Distrib.toHasAdd.{u1} Y (Ring.toDistrib.{u1} Y _inst_2))) -> (CategoryTheory.Iso.{u1, succ u1} RingCat.{u1} RingCat.largeCategory.{u1} (RingCat.of.{u1} X _inst_1) (RingCat.of.{u1} Y _inst_2)) +but is expected to have type + forall {X : Type.{u1}} {Y : Type.{u1}} [_inst_1 : Ring.{u1} X] [_inst_2 : Ring.{u1} Y], (RingEquiv.{u1, u1} X Y (NonUnitalNonAssocRing.toMul.{u1} X (NonAssocRing.toNonUnitalNonAssocRing.{u1} X (Ring.toNonAssocRing.{u1} X _inst_1))) (NonUnitalNonAssocRing.toMul.{u1} Y (NonAssocRing.toNonUnitalNonAssocRing.{u1} Y (Ring.toNonAssocRing.{u1} Y _inst_2))) (Distrib.toAdd.{u1} X (NonUnitalNonAssocSemiring.toDistrib.{u1} X (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} X (NonAssocRing.toNonUnitalNonAssocRing.{u1} X (Ring.toNonAssocRing.{u1} X _inst_1))))) (Distrib.toAdd.{u1} Y (NonUnitalNonAssocSemiring.toDistrib.{u1} Y (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} Y (NonAssocRing.toNonUnitalNonAssocRing.{u1} Y (Ring.toNonAssocRing.{u1} Y _inst_2)))))) -> (CategoryTheory.Iso.{u1, succ u1} RingCat.{u1} instRingCatLargeCategory.{u1} (RingCat.of.{u1} X _inst_1) (RingCat.of.{u1} Y _inst_2)) +Case conversion may be inaccurate. Consider using '#align ring_equiv.to_Ring_iso RingEquiv.toRingCatIsoₓ'. -/ /-- Build an isomorphism in the category `Ring` from a `ring_equiv` between `ring`s. -/ @[simps] -def toRingIso [Ring X] [Ring Y] (e : X ≃+* Y) : RingCat.of X ≅ RingCat.of Y +def toRingCatIso [Ring X] [Ring Y] (e : X ≃+* Y) : RingCat.of X ≅ RingCat.of Y where Hom := e.toRingHom inv := e.symm.toRingHom -#align ring_equiv.to_Ring_iso RingEquiv.toRingIso - +#align ring_equiv.to_Ring_iso RingEquiv.toRingCatIso + +/- warning: ring_equiv.to_CommRing_iso -> RingEquiv.toCommRingCatIso is a dubious translation: +lean 3 declaration is + forall {X : Type.{u1}} {Y : Type.{u1}} [_inst_1 : CommRing.{u1} X] [_inst_2 : CommRing.{u1} Y], (RingEquiv.{u1, u1} X Y (Distrib.toHasMul.{u1} X (Ring.toDistrib.{u1} X (CommRing.toRing.{u1} X _inst_1))) (Distrib.toHasAdd.{u1} X (Ring.toDistrib.{u1} X (CommRing.toRing.{u1} X _inst_1))) (Distrib.toHasMul.{u1} Y (Ring.toDistrib.{u1} Y (CommRing.toRing.{u1} Y _inst_2))) (Distrib.toHasAdd.{u1} Y (Ring.toDistrib.{u1} Y (CommRing.toRing.{u1} Y _inst_2)))) -> (CategoryTheory.Iso.{u1, succ u1} CommRingCat.{u1} CommRingCat.largeCategory.{u1} (CommRingCat.of.{u1} X _inst_1) (CommRingCat.of.{u1} Y _inst_2)) +but is expected to have type + forall {X : Type.{u1}} {Y : Type.{u1}} [_inst_1 : CommRing.{u1} X] [_inst_2 : CommRing.{u1} Y], (RingEquiv.{u1, u1} X Y (NonUnitalNonAssocRing.toMul.{u1} X (NonAssocRing.toNonUnitalNonAssocRing.{u1} X (Ring.toNonAssocRing.{u1} X (CommRing.toRing.{u1} X _inst_1)))) (NonUnitalNonAssocRing.toMul.{u1} Y (NonAssocRing.toNonUnitalNonAssocRing.{u1} Y (Ring.toNonAssocRing.{u1} Y (CommRing.toRing.{u1} Y _inst_2)))) (Distrib.toAdd.{u1} X (NonUnitalNonAssocSemiring.toDistrib.{u1} X (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} X (NonAssocRing.toNonUnitalNonAssocRing.{u1} X (Ring.toNonAssocRing.{u1} X (CommRing.toRing.{u1} X _inst_1)))))) (Distrib.toAdd.{u1} Y (NonUnitalNonAssocSemiring.toDistrib.{u1} Y (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} Y (NonAssocRing.toNonUnitalNonAssocRing.{u1} Y (Ring.toNonAssocRing.{u1} Y (CommRing.toRing.{u1} Y _inst_2))))))) -> (CategoryTheory.Iso.{u1, succ u1} CommRingCat.{u1} instCommRingCatLargeCategory.{u1} (CommRingCat.of.{u1} X _inst_1) (CommRingCat.of.{u1} Y _inst_2)) +Case conversion may be inaccurate. Consider using '#align ring_equiv.to_CommRing_iso RingEquiv.toCommRingCatIsoₓ'. -/ /-- Build an isomorphism in the category `CommRing` from a `ring_equiv` between `comm_ring`s. -/ @[simps] -def toCommRingIso [CommRing X] [CommRing Y] (e : X ≃+* Y) : CommRingCat.of X ≅ CommRingCat.of Y +def toCommRingCatIso [CommRing X] [CommRing Y] (e : X ≃+* Y) : CommRingCat.of X ≅ CommRingCat.of Y where Hom := e.toRingHom inv := e.symm.toRingHom -#align ring_equiv.to_CommRing_iso RingEquiv.toCommRingIso +#align ring_equiv.to_CommRing_iso RingEquiv.toCommRingCatIso end RingEquiv namespace CategoryTheory.Iso +/- warning: category_theory.iso.Ring_iso_to_ring_equiv -> CategoryTheory.Iso.ringCatIsoToRingEquiv is a dubious translation: +lean 3 declaration is + forall {X : RingCat.{u1}} {Y : RingCat.{u1}}, (CategoryTheory.Iso.{u1, succ u1} RingCat.{u1} RingCat.largeCategory.{u1} X Y) -> (RingEquiv.{u1, u1} (coeSort.{succ (succ u1), succ (succ u1)} RingCat.{u1} Type.{u1} RingCat.hasCoeToSort.{u1} X) (coeSort.{succ (succ u1), succ (succ u1)} RingCat.{u1} Type.{u1} RingCat.hasCoeToSort.{u1} Y) (Distrib.toHasMul.{u1} (coeSort.{succ (succ u1), succ (succ u1)} RingCat.{u1} Type.{u1} RingCat.hasCoeToSort.{u1} X) (Ring.toDistrib.{u1} (coeSort.{succ (succ u1), succ (succ u1)} RingCat.{u1} Type.{u1} RingCat.hasCoeToSort.{u1} X) (RingCat.ring.{u1} X))) (Distrib.toHasAdd.{u1} (coeSort.{succ (succ u1), succ (succ u1)} RingCat.{u1} Type.{u1} RingCat.hasCoeToSort.{u1} X) (Ring.toDistrib.{u1} (coeSort.{succ (succ u1), succ (succ u1)} RingCat.{u1} Type.{u1} RingCat.hasCoeToSort.{u1} X) (RingCat.ring.{u1} X))) (Distrib.toHasMul.{u1} (coeSort.{succ (succ u1), succ (succ u1)} RingCat.{u1} Type.{u1} RingCat.hasCoeToSort.{u1} Y) (Ring.toDistrib.{u1} (coeSort.{succ (succ u1), succ (succ u1)} RingCat.{u1} Type.{u1} RingCat.hasCoeToSort.{u1} Y) (RingCat.ring.{u1} Y))) (Distrib.toHasAdd.{u1} (coeSort.{succ (succ u1), succ (succ u1)} RingCat.{u1} Type.{u1} RingCat.hasCoeToSort.{u1} Y) (Ring.toDistrib.{u1} (coeSort.{succ (succ u1), succ (succ u1)} RingCat.{u1} Type.{u1} RingCat.hasCoeToSort.{u1} Y) (RingCat.ring.{u1} Y)))) +but is expected to have type + forall {X : RingCat.{u1}} {Y : RingCat.{u1}}, (CategoryTheory.Iso.{u1, succ u1} RingCat.{u1} instRingCatLargeCategory.{u1} X Y) -> (RingEquiv.{u1, u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} X) (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} Y) (NonUnitalNonAssocRing.toMul.{u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} X) (NonAssocRing.toNonUnitalNonAssocRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} X) (Ring.toNonAssocRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} X) (RingCat.instRingα_1.{u1} X)))) (NonUnitalNonAssocRing.toMul.{u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} Y) (NonAssocRing.toNonUnitalNonAssocRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} Y) (Ring.toNonAssocRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} Y) (RingCat.instRingα_1.{u1} Y)))) (Distrib.toAdd.{u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} X) (NonUnitalNonAssocSemiring.toDistrib.{u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} X) (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} X) (NonAssocRing.toNonUnitalNonAssocRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} X) (Ring.toNonAssocRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} X) (RingCat.instRingα_1.{u1} X)))))) (Distrib.toAdd.{u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} Y) (NonUnitalNonAssocSemiring.toDistrib.{u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} Y) (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} Y) (NonAssocRing.toNonUnitalNonAssocRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} Y) (Ring.toNonAssocRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} Ring.{u1} Y) (RingCat.instRingα_1.{u1} Y))))))) +Case conversion may be inaccurate. Consider using '#align category_theory.iso.Ring_iso_to_ring_equiv CategoryTheory.Iso.ringCatIsoToRingEquivₓ'. -/ /-- Build a `ring_equiv` from an isomorphism in the category `Ring`. -/ -def ringIsoToRingEquiv {X Y : RingCat} (i : X ≅ Y) : X ≃+* Y +def ringCatIsoToRingEquiv {X Y : RingCat} (i : X ≅ Y) : X ≃+* Y where toFun := i.Hom invFun := i.inv @@ -298,10 +388,16 @@ def ringIsoToRingEquiv {X Y : RingCat} (i : X ≅ Y) : X ≃+* Y right_inv := by tidy map_add' := by tidy map_mul' := by tidy -#align category_theory.iso.Ring_iso_to_ring_equiv CategoryTheory.Iso.ringIsoToRingEquiv - +#align category_theory.iso.Ring_iso_to_ring_equiv CategoryTheory.Iso.ringCatIsoToRingEquiv + +/- warning: category_theory.iso.CommRing_iso_to_ring_equiv -> CategoryTheory.Iso.commRingCatIsoToRingEquiv is a dubious translation: +lean 3 declaration is + forall {X : CommRingCat.{u1}} {Y : CommRingCat.{u1}}, (CategoryTheory.Iso.{u1, succ u1} CommRingCat.{u1} CommRingCat.largeCategory.{u1} X Y) -> (RingEquiv.{u1, u1} (coeSort.{succ (succ u1), succ (succ u1)} CommRingCat.{u1} Type.{u1} CommRingCat.hasCoeToSort.{u1} X) (coeSort.{succ (succ u1), succ (succ u1)} CommRingCat.{u1} Type.{u1} CommRingCat.hasCoeToSort.{u1} Y) (Distrib.toHasMul.{u1} (coeSort.{succ (succ u1), succ (succ u1)} CommRingCat.{u1} Type.{u1} CommRingCat.hasCoeToSort.{u1} X) (Ring.toDistrib.{u1} (coeSort.{succ (succ u1), succ (succ u1)} CommRingCat.{u1} Type.{u1} CommRingCat.hasCoeToSort.{u1} X) (CommRing.toRing.{u1} (coeSort.{succ (succ u1), succ (succ u1)} CommRingCat.{u1} Type.{u1} CommRingCat.hasCoeToSort.{u1} X) (CommRingCat.commRing.{u1} X)))) (Distrib.toHasAdd.{u1} (coeSort.{succ (succ u1), succ (succ u1)} CommRingCat.{u1} Type.{u1} CommRingCat.hasCoeToSort.{u1} X) (Ring.toDistrib.{u1} (coeSort.{succ (succ u1), succ (succ u1)} CommRingCat.{u1} Type.{u1} CommRingCat.hasCoeToSort.{u1} X) (CommRing.toRing.{u1} (coeSort.{succ (succ u1), succ (succ u1)} CommRingCat.{u1} Type.{u1} CommRingCat.hasCoeToSort.{u1} X) (CommRingCat.commRing.{u1} X)))) (Distrib.toHasMul.{u1} (coeSort.{succ (succ u1), succ (succ u1)} CommRingCat.{u1} Type.{u1} CommRingCat.hasCoeToSort.{u1} Y) (Ring.toDistrib.{u1} (coeSort.{succ (succ u1), succ (succ u1)} CommRingCat.{u1} Type.{u1} CommRingCat.hasCoeToSort.{u1} Y) (CommRing.toRing.{u1} (coeSort.{succ (succ u1), succ (succ u1)} CommRingCat.{u1} Type.{u1} CommRingCat.hasCoeToSort.{u1} Y) (CommRingCat.commRing.{u1} Y)))) (Distrib.toHasAdd.{u1} (coeSort.{succ (succ u1), succ (succ u1)} CommRingCat.{u1} Type.{u1} CommRingCat.hasCoeToSort.{u1} Y) (Ring.toDistrib.{u1} (coeSort.{succ (succ u1), succ (succ u1)} CommRingCat.{u1} Type.{u1} CommRingCat.hasCoeToSort.{u1} Y) (CommRing.toRing.{u1} (coeSort.{succ (succ u1), succ (succ u1)} CommRingCat.{u1} Type.{u1} CommRingCat.hasCoeToSort.{u1} Y) (CommRingCat.commRing.{u1} Y))))) +but is expected to have type + forall {X : CommRingCat.{u1}} {Y : CommRingCat.{u1}}, (CategoryTheory.Iso.{u1, succ u1} CommRingCat.{u1} instCommRingCatLargeCategory.{u1} X Y) -> (RingEquiv.{u1, u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} X) (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} Y) (NonUnitalNonAssocRing.toMul.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} X) (NonAssocRing.toNonUnitalNonAssocRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} X) (Ring.toNonAssocRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} X) (CommRing.toRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} X) (CommRingCat.instCommRingα_1.{u1} X))))) (NonUnitalNonAssocRing.toMul.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} Y) (NonAssocRing.toNonUnitalNonAssocRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} Y) (Ring.toNonAssocRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} Y) (CommRing.toRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} Y) (CommRingCat.instCommRingα_1.{u1} Y))))) (Distrib.toAdd.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} X) (NonUnitalNonAssocSemiring.toDistrib.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} X) (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} X) (NonAssocRing.toNonUnitalNonAssocRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} X) (Ring.toNonAssocRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} X) (CommRing.toRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} X) (CommRingCat.instCommRingα_1.{u1} X))))))) (Distrib.toAdd.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} Y) (NonUnitalNonAssocSemiring.toDistrib.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} Y) (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} Y) (NonAssocRing.toNonUnitalNonAssocRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} Y) (Ring.toNonAssocRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} Y) (CommRing.toRing.{u1} (CategoryTheory.Bundled.α.{u1, u1} CommRing.{u1} Y) (CommRingCat.instCommRingα_1.{u1} Y)))))))) +Case conversion may be inaccurate. Consider using '#align category_theory.iso.CommRing_iso_to_ring_equiv CategoryTheory.Iso.commRingCatIsoToRingEquivₓ'. -/ /-- Build a `ring_equiv` from an isomorphism in the category `CommRing`. -/ -def commRingIsoToRingEquiv {X Y : CommRingCat} (i : X ≅ Y) : X ≃+* Y +def commRingCatIsoToRingEquiv {X Y : CommRingCat} (i : X ≅ Y) : X ≃+* Y where toFun := i.Hom invFun := i.inv @@ -309,42 +405,59 @@ def commRingIsoToRingEquiv {X Y : CommRingCat} (i : X ≅ Y) : X ≃+* Y right_inv := by tidy map_add' := by tidy map_mul' := by tidy -#align category_theory.iso.CommRing_iso_to_ring_equiv CategoryTheory.Iso.commRingIsoToRingEquiv +#align category_theory.iso.CommRing_iso_to_ring_equiv CategoryTheory.Iso.commRingCatIsoToRingEquiv +#print CategoryTheory.Iso.commRingIsoToRingEquiv_toRingHom /- @[simp] theorem commRingIsoToRingEquiv_toRingHom {X Y : CommRingCat} (i : X ≅ Y) : - i.commRingIsoToRingEquiv.toRingHom = i.Hom := + i.commRingCatIsoToRingEquiv.toRingHom = i.Hom := by ext rfl #align category_theory.iso.CommRing_iso_to_ring_equiv_to_ring_hom CategoryTheory.Iso.commRingIsoToRingEquiv_toRingHom +-/ +#print CategoryTheory.Iso.commRingIsoToRingEquiv_symm_toRingHom /- @[simp] theorem commRingIsoToRingEquiv_symm_toRingHom {X Y : CommRingCat} (i : X ≅ Y) : - i.commRingIsoToRingEquiv.symm.toRingHom = i.inv := + i.commRingCatIsoToRingEquiv.symm.toRingHom = i.inv := by ext rfl #align category_theory.iso.CommRing_iso_to_ring_equiv_symm_to_ring_hom CategoryTheory.Iso.commRingIsoToRingEquiv_symm_toRingHom +-/ end CategoryTheory.Iso +/- warning: ring_equiv_iso_Ring_iso -> ringEquivIsoRingIso is a dubious translation: +lean 3 declaration is + forall {X : Type.{u1}} {Y : Type.{u1}} [_inst_1 : Ring.{u1} X] [_inst_2 : Ring.{u1} Y], CategoryTheory.Iso.{u1, succ u1} Type.{u1} CategoryTheory.types.{u1} (RingEquiv.{u1, u1} X Y (Distrib.toHasMul.{u1} X (Ring.toDistrib.{u1} X _inst_1)) (Distrib.toHasAdd.{u1} X (Ring.toDistrib.{u1} X _inst_1)) (Distrib.toHasMul.{u1} Y (Ring.toDistrib.{u1} Y _inst_2)) (Distrib.toHasAdd.{u1} Y (Ring.toDistrib.{u1} Y _inst_2))) (CategoryTheory.Iso.{u1, succ u1} RingCat.{u1} RingCat.largeCategory.{u1} (RingCat.of.{u1} X _inst_1) (RingCat.of.{u1} Y _inst_2)) +but is expected to have type + forall {X : Type.{u1}} {Y : Type.{u1}} [_inst_1 : Ring.{u1} X] [_inst_2 : Ring.{u1} Y], CategoryTheory.Iso.{u1, succ u1} Type.{u1} CategoryTheory.types.{u1} (RingEquiv.{u1, u1} X Y (NonUnitalNonAssocRing.toMul.{u1} X (NonAssocRing.toNonUnitalNonAssocRing.{u1} X (Ring.toNonAssocRing.{u1} X _inst_1))) (NonUnitalNonAssocRing.toMul.{u1} Y (NonAssocRing.toNonUnitalNonAssocRing.{u1} Y (Ring.toNonAssocRing.{u1} Y _inst_2))) (Distrib.toAdd.{u1} X (NonUnitalNonAssocSemiring.toDistrib.{u1} X (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} X (NonAssocRing.toNonUnitalNonAssocRing.{u1} X (Ring.toNonAssocRing.{u1} X _inst_1))))) (Distrib.toAdd.{u1} Y (NonUnitalNonAssocSemiring.toDistrib.{u1} Y (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} Y (NonAssocRing.toNonUnitalNonAssocRing.{u1} Y (Ring.toNonAssocRing.{u1} Y _inst_2)))))) (CategoryTheory.Iso.{u1, succ u1} RingCat.{u1} instRingCatLargeCategory.{u1} (RingCat.of.{u1} X _inst_1) (RingCat.of.{u1} Y _inst_2)) +Case conversion may be inaccurate. Consider using '#align ring_equiv_iso_Ring_iso ringEquivIsoRingIsoₓ'. -/ /-- Ring equivalences between `ring`s are the same as (isomorphic to) isomorphisms in `Ring`. -/ def ringEquivIsoRingIso {X Y : Type u} [Ring X] [Ring Y] : X ≃+* Y ≅ RingCat.of X ≅ RingCat.of Y where - Hom e := e.toRingIso - inv i := i.ringIsoToRingEquiv + Hom e := e.toRingCatIso + inv i := i.ringCatIsoToRingEquiv #align ring_equiv_iso_Ring_iso ringEquivIsoRingIso +/- warning: ring_equiv_iso_CommRing_iso -> ringEquivIsoCommRingIso is a dubious translation: +lean 3 declaration is + forall {X : Type.{u1}} {Y : Type.{u1}} [_inst_1 : CommRing.{u1} X] [_inst_2 : CommRing.{u1} Y], CategoryTheory.Iso.{u1, succ u1} Type.{u1} CategoryTheory.types.{u1} (RingEquiv.{u1, u1} X Y (Distrib.toHasMul.{u1} X (Ring.toDistrib.{u1} X (CommRing.toRing.{u1} X _inst_1))) (Distrib.toHasAdd.{u1} X (Ring.toDistrib.{u1} X (CommRing.toRing.{u1} X _inst_1))) (Distrib.toHasMul.{u1} Y (Ring.toDistrib.{u1} Y (CommRing.toRing.{u1} Y _inst_2))) (Distrib.toHasAdd.{u1} Y (Ring.toDistrib.{u1} Y (CommRing.toRing.{u1} Y _inst_2)))) (CategoryTheory.Iso.{u1, succ u1} CommRingCat.{u1} CommRingCat.largeCategory.{u1} (CommRingCat.of.{u1} X _inst_1) (CommRingCat.of.{u1} Y _inst_2)) +but is expected to have type + forall {X : Type.{u1}} {Y : Type.{u1}} [_inst_1 : CommRing.{u1} X] [_inst_2 : CommRing.{u1} Y], CategoryTheory.Iso.{u1, succ u1} Type.{u1} CategoryTheory.types.{u1} (RingEquiv.{u1, u1} X Y (NonUnitalNonAssocRing.toMul.{u1} X (NonAssocRing.toNonUnitalNonAssocRing.{u1} X (Ring.toNonAssocRing.{u1} X (CommRing.toRing.{u1} X _inst_1)))) (NonUnitalNonAssocRing.toMul.{u1} Y (NonAssocRing.toNonUnitalNonAssocRing.{u1} Y (Ring.toNonAssocRing.{u1} Y (CommRing.toRing.{u1} Y _inst_2)))) (Distrib.toAdd.{u1} X (NonUnitalNonAssocSemiring.toDistrib.{u1} X (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} X (NonAssocRing.toNonUnitalNonAssocRing.{u1} X (Ring.toNonAssocRing.{u1} X (CommRing.toRing.{u1} X _inst_1)))))) (Distrib.toAdd.{u1} Y (NonUnitalNonAssocSemiring.toDistrib.{u1} Y (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} Y (NonAssocRing.toNonUnitalNonAssocRing.{u1} Y (Ring.toNonAssocRing.{u1} Y (CommRing.toRing.{u1} Y _inst_2))))))) (CategoryTheory.Iso.{u1, succ u1} CommRingCat.{u1} instCommRingCatLargeCategory.{u1} (CommRingCat.of.{u1} X _inst_1) (CommRingCat.of.{u1} Y _inst_2)) +Case conversion may be inaccurate. Consider using '#align ring_equiv_iso_CommRing_iso ringEquivIsoCommRingIsoₓ'. -/ /-- Ring equivalences between `comm_ring`s are the same as (isomorphic to) isomorphisms in `CommRing`. -/ def ringEquivIsoCommRingIso {X Y : Type u} [CommRing X] [CommRing Y] : X ≃+* Y ≅ CommRingCat.of X ≅ CommRingCat.of Y where - Hom e := e.toCommRingIso - inv i := i.commRingIsoToRingEquiv + Hom e := e.toCommRingCatIso + inv i := i.commRingCatIsoToRingEquiv #align ring_equiv_iso_CommRing_iso ringEquivIsoCommRingIso +#print RingCat.forget_reflects_isos /- instance RingCat.forget_reflects_isos : ReflectsIsomorphisms (forget RingCat.{u}) where reflects X Y f _ := by skip @@ -352,7 +465,9 @@ instance RingCat.forget_reflects_isos : ReflectsIsomorphisms (forget RingCat.{u} let e : X ≃+* Y := { f, i.to_equiv with } exact ⟨(is_iso.of_iso e.to_Ring_iso).1⟩ #align Ring.forget_reflects_isos RingCat.forget_reflects_isos +-/ +#print CommRingCat.forget_reflects_isos /- instance CommRingCat.forget_reflects_isos : ReflectsIsomorphisms (forget CommRingCat.{u}) where reflects X Y f _ := by skip @@ -360,16 +475,21 @@ instance CommRingCat.forget_reflects_isos : ReflectsIsomorphisms (forget CommRin let e : X ≃+* Y := { f, i.to_equiv with } exact ⟨(is_iso.of_iso e.to_CommRing_iso).1⟩ #align CommRing.forget_reflects_isos CommRingCat.forget_reflects_isos +-/ +#print CommRingCat.comp_eq_ring_hom_comp /- theorem CommRingCat.comp_eq_ring_hom_comp {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) : f ≫ g = g.comp f := rfl #align CommRing.comp_eq_ring_hom_comp CommRingCat.comp_eq_ring_hom_comp +-/ +#print CommRingCat.ringHom_comp_eq_comp /- theorem CommRingCat.ringHom_comp_eq_comp {R S T : Type _} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) : g.comp f = CommRingCat.ofHom f ≫ CommRingCat.ofHom g := rfl #align CommRing.ring_hom_comp_eq_comp CommRingCat.ringHom_comp_eq_comp +-/ -- It would be nice if we could have the following, -- but it requires making `reflects_isomorphisms_forget₂` an instance, diff --git a/Mathbin/Algebra/Category/Ring/Constructions.lean b/Mathbin/Algebra/Category/Ring/Constructions.lean index 50f171e755..1ea824ee96 100644 --- a/Mathbin/Algebra/Category/Ring/Constructions.lean +++ b/Mathbin/Algebra/Category/Ring/Constructions.lean @@ -154,7 +154,7 @@ instance commRingCat_hasStrictTerminalObjects : HasStrictTerminalObjects CommRin #align CommRing.CommRing_has_strict_terminal_objects CommRingCat.commRingCat_hasStrictTerminalObjects theorem subsingleton_of_isTerminal {X : CommRingCat} (hX : IsTerminal X) : Subsingleton X := - (hX.uniqueUpToIso punitIsTerminal).commRingIsoToRingEquiv.toEquiv.subsingleton_congr.mpr + (hX.uniqueUpToIso punitIsTerminal).commRingCatIsoToRingEquiv.toEquiv.subsingleton_congr.mpr (show Subsingleton PUnit by infer_instance) #align CommRing.subsingleton_of_is_terminal CommRingCat.subsingleton_of_isTerminal diff --git a/Mathbin/Algebra/Category/Ring/FilteredColimits.lean b/Mathbin/Algebra/Category/Ring/FilteredColimits.lean index c9e3b19a4b..bff27c256f 100644 --- a/Mathbin/Algebra/Category/Ring/FilteredColimits.lean +++ b/Mathbin/Algebra/Category/Ring/FilteredColimits.lean @@ -43,20 +43,20 @@ open AddMonCat.FilteredColimits (colimit_zero_eq colimit_add_mk_eq) open MonCat.FilteredColimits (colimit_one_eq colimit_mul_mk_eq) -namespace SemiRing.FilteredColimits +namespace SemiRingCat.FilteredColimits section -- We use parameters here, mainly so we can have the abbreviations `R` and `R.mk` below, without -- passing around `F` all the time. -parameter {J : Type v}[SmallCategory J](F : J ⥤ SemiRing.{max v u}) +parameter {J : Type v}[SmallCategory J](F : J ⥤ SemiRingCat.{max v u}) -- This instance is needed below in `colimit_semiring`, during the verification of the -- semiring axioms. instance semiringObj (j : J) : - Semiring (((F ⋙ forget₂ SemiRing MonCat.{max v u}) ⋙ forget MonCat).obj j) := + Semiring (((F ⋙ forget₂ SemiRingCat MonCat.{max v u}) ⋙ forget MonCat).obj j) := show Semiring (F.obj j) by infer_instance -#align SemiRing.filtered_colimits.semiring_obj SemiRing.FilteredColimits.semiringObj +#align SemiRing.filtered_colimits.semiring_obj SemiRingCat.FilteredColimits.semiringObj variable [IsFiltered J] @@ -64,14 +64,14 @@ variable [IsFiltered J] In the following, we will show that this has the structure of a semiring. -/ abbrev r : MonCat := - MonCat.FilteredColimits.colimit (F ⋙ forget₂ SemiRing MonCat.{max v u}) -#align SemiRing.filtered_colimits.R SemiRing.FilteredColimits.r + MonCat.FilteredColimits.colimit (F ⋙ forget₂ SemiRingCat MonCat.{max v u}) +#align SemiRing.filtered_colimits.R SemiRingCat.FilteredColimits.r instance colimitSemiring : Semiring R := { R.Monoid, AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ - forget₂ SemiRing + forget₂ SemiRingCat AddCommMonCat.{max v u}) with mul_zero := fun x => by @@ -112,131 +112,136 @@ instance colimitSemiring : Semiring R := simp only [CategoryTheory.Functor.map_id, id_apply] erw [right_distrib (F.map f x) (F.map g y) (F.map h z)] rfl } -#align SemiRing.filtered_colimits.colimit_semiring SemiRing.FilteredColimits.colimitSemiring +#align SemiRing.filtered_colimits.colimit_semiring SemiRingCat.FilteredColimits.colimitSemiring /-- The bundled semiring giving the filtered colimit of a diagram. -/ -def colimit : SemiRing := - SemiRing.of R -#align SemiRing.filtered_colimits.colimit SemiRing.FilteredColimits.colimit +def colimit : SemiRingCat := + SemiRingCat.of R +#align SemiRing.filtered_colimits.colimit SemiRingCat.FilteredColimits.colimit /-- The cocone over the proposed colimit semiring. -/ def colimitCocone : cocone F where pt := colimit ι := { app := fun j => - { (MonCat.FilteredColimits.colimitCocone (F ⋙ forget₂ SemiRing MonCat.{max v u})).ι.app j, + { + (MonCat.FilteredColimits.colimitCocone (F ⋙ forget₂ SemiRingCat MonCat.{max v u})).ι.app + j, (AddCommMonCat.FilteredColimits.colimitCocone - (F ⋙ forget₂ SemiRing AddCommMonCat.{max v u})).ι.app + (F ⋙ forget₂ SemiRingCat AddCommMonCat.{max v u})).ι.app j with } naturality' := fun j j' f => - RingHom.coe_inj ((Types.colimitCocone (F ⋙ forget SemiRing)).ι.naturality f) } -#align SemiRing.filtered_colimits.colimit_cocone SemiRing.FilteredColimits.colimitCocone + RingHom.coe_inj ((Types.colimitCocone (F ⋙ forget SemiRingCat)).ι.naturality f) } +#align SemiRing.filtered_colimits.colimit_cocone SemiRingCat.FilteredColimits.colimitCocone /-- The proposed colimit cocone is a colimit in `SemiRing`. -/ def colimitCoconeIsColimit : IsColimit colimit_cocone where desc t := { - (MonCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ SemiRing MonCat.{max v u})).desc - ((forget₂ SemiRing MonCat.{max v u}).mapCocone t), + (MonCat.FilteredColimits.colimitCoconeIsColimit + (F ⋙ forget₂ SemiRingCat MonCat.{max v u})).desc + ((forget₂ SemiRingCat MonCat.{max v u}).mapCocone t), (AddCommMonCat.FilteredColimits.colimitCoconeIsColimit - (F ⋙ forget₂ SemiRing AddCommMonCat.{max v u})).desc - ((forget₂ SemiRing AddCommMonCat.{max v u}).mapCocone t) with } + (F ⋙ forget₂ SemiRingCat AddCommMonCat.{max v u})).desc + ((forget₂ SemiRingCat AddCommMonCat.{max v u}).mapCocone t) with } fac t j := RingHom.coe_inj <| - (Types.colimitCoconeIsColimit (F ⋙ forget SemiRing)).fac ((forget SemiRing).mapCocone t) j + (Types.colimitCoconeIsColimit (F ⋙ forget SemiRingCat)).fac ((forget SemiRingCat).mapCocone t) + j uniq t m h := RingHom.coe_inj <| - (Types.colimitCoconeIsColimit (F ⋙ forget SemiRing)).uniq ((forget SemiRing).mapCocone t) m - fun j => funext fun x => RingHom.congr_fun (h j) x -#align SemiRing.filtered_colimits.colimit_cocone_is_colimit SemiRing.FilteredColimits.colimitCoconeIsColimit + (Types.colimitCoconeIsColimit (F ⋙ forget SemiRingCat)).uniq + ((forget SemiRingCat).mapCocone t) m fun j => funext fun x => RingHom.congr_fun (h j) x +#align SemiRing.filtered_colimits.colimit_cocone_is_colimit SemiRingCat.FilteredColimits.colimitCoconeIsColimit instance forget₂MonPreservesFilteredColimits : - PreservesFilteredColimits (forget₂ SemiRing MonCat.{u}) + PreservesFilteredColimits (forget₂ SemiRingCat MonCat.{u}) where PreservesFilteredColimits J _ _ := { PreservesColimit := fun F => preserves_colimit_of_preserves_colimit_cocone (colimitCoconeIsColimit.{u, u} F) - (MonCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ SemiRing MonCat.{u})) } -#align SemiRing.filtered_colimits.forget₂_Mon_preserves_filtered_colimits SemiRing.FilteredColimits.forget₂MonPreservesFilteredColimits + (MonCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ SemiRingCat MonCat.{u})) } +#align SemiRing.filtered_colimits.forget₂_Mon_preserves_filtered_colimits SemiRingCat.FilteredColimits.forget₂MonPreservesFilteredColimits -instance forgetPreservesFilteredColimits : PreservesFilteredColimits (forget SemiRing.{u}) := - Limits.compPreservesFilteredColimits (forget₂ SemiRing MonCat) (forget MonCat.{u}) -#align SemiRing.filtered_colimits.forget_preserves_filtered_colimits SemiRing.FilteredColimits.forgetPreservesFilteredColimits +instance forgetPreservesFilteredColimits : PreservesFilteredColimits (forget SemiRingCat.{u}) := + Limits.compPreservesFilteredColimits (forget₂ SemiRingCat MonCat) (forget MonCat.{u}) +#align SemiRing.filtered_colimits.forget_preserves_filtered_colimits SemiRingCat.FilteredColimits.forgetPreservesFilteredColimits end -end SemiRing.FilteredColimits +end SemiRingCat.FilteredColimits -namespace CommSemiRing.FilteredColimits +namespace CommSemiRingCat.FilteredColimits section -- We use parameters here, mainly so we can have the abbreviation `R` below, without -- passing around `F` all the time. -parameter {J : Type v}[SmallCategory J][IsFiltered J](F : J ⥤ CommSemiRing.{max v u}) +parameter {J : Type v}[SmallCategory J][IsFiltered J](F : J ⥤ CommSemiRingCat.{max v u}) /-- The colimit of `F ⋙ forget₂ CommSemiRing SemiRing` in the category `SemiRing`. In the following, we will show that this has the structure of a _commutative_ semiring. -/ -abbrev r : SemiRing := - SemiRing.FilteredColimits.colimit (F ⋙ forget₂ CommSemiRing SemiRing.{max v u}) -#align CommSemiRing.filtered_colimits.R CommSemiRing.FilteredColimits.r +abbrev r : SemiRingCat := + SemiRingCat.FilteredColimits.colimit (F ⋙ forget₂ CommSemiRingCat SemiRingCat.{max v u}) +#align CommSemiRing.filtered_colimits.R CommSemiRingCat.FilteredColimits.r instance colimitCommSemiring : CommSemiring R := { R.Semiring, CommMonCat.FilteredColimits.colimitCommMonoid - (F ⋙ forget₂ CommSemiRing CommMonCat.{max v u}) with } -#align CommSemiRing.filtered_colimits.colimit_comm_semiring CommSemiRing.FilteredColimits.colimitCommSemiring + (F ⋙ forget₂ CommSemiRingCat CommMonCat.{max v u}) with } +#align CommSemiRing.filtered_colimits.colimit_comm_semiring CommSemiRingCat.FilteredColimits.colimitCommSemiring /-- The bundled commutative semiring giving the filtered colimit of a diagram. -/ -def colimit : CommSemiRing := +def colimit : CommSemiRingCat := CommSemiRing.of R -#align CommSemiRing.filtered_colimits.colimit CommSemiRing.FilteredColimits.colimit +#align CommSemiRing.filtered_colimits.colimit CommSemiRingCat.FilteredColimits.colimit /-- The cocone over the proposed colimit commutative semiring. -/ def colimitCocone : cocone F where pt := colimit ι := { - (SemiRing.FilteredColimits.colimitCocone - (F ⋙ forget₂ CommSemiRing SemiRing.{max v u})).ι with } -#align CommSemiRing.filtered_colimits.colimit_cocone CommSemiRing.FilteredColimits.colimitCocone + (SemiRingCat.FilteredColimits.colimitCocone + (F ⋙ forget₂ CommSemiRingCat SemiRingCat.{max v u})).ι with } +#align CommSemiRing.filtered_colimits.colimit_cocone CommSemiRingCat.FilteredColimits.colimitCocone /-- The proposed colimit cocone is a colimit in `CommSemiRing`. -/ def colimitCoconeIsColimit : IsColimit colimit_cocone where desc t := - (SemiRing.FilteredColimits.colimitCoconeIsColimit - (F ⋙ forget₂ CommSemiRing SemiRing.{max v u})).desc - ((forget₂ CommSemiRing SemiRing).mapCocone t) + (SemiRingCat.FilteredColimits.colimitCoconeIsColimit + (F ⋙ forget₂ CommSemiRingCat SemiRingCat.{max v u})).desc + ((forget₂ CommSemiRingCat SemiRingCat).mapCocone t) fac t j := RingHom.coe_inj <| - (Types.colimitCoconeIsColimit (F ⋙ forget CommSemiRing)).fac - ((forget CommSemiRing).mapCocone t) j + (Types.colimitCoconeIsColimit (F ⋙ forget CommSemiRingCat)).fac + ((forget CommSemiRingCat).mapCocone t) j uniq t m h := RingHom.coe_inj <| - (Types.colimitCoconeIsColimit (F ⋙ forget CommSemiRing)).uniq - ((forget CommSemiRing).mapCocone t) m fun j => funext fun x => RingHom.congr_fun (h j) x -#align CommSemiRing.filtered_colimits.colimit_cocone_is_colimit CommSemiRing.FilteredColimits.colimitCoconeIsColimit + (Types.colimitCoconeIsColimit (F ⋙ forget CommSemiRingCat)).uniq + ((forget CommSemiRingCat).mapCocone t) m fun j => funext fun x => RingHom.congr_fun (h j) x +#align CommSemiRing.filtered_colimits.colimit_cocone_is_colimit CommSemiRingCat.FilteredColimits.colimitCoconeIsColimit instance forget₂SemiRingPreservesFilteredColimits : - PreservesFilteredColimits (forget₂ CommSemiRing SemiRing.{u}) + PreservesFilteredColimits (forget₂ CommSemiRingCat SemiRingCat.{u}) where PreservesFilteredColimits J _ _ := { PreservesColimit := fun F => preserves_colimit_of_preserves_colimit_cocone (colimitCoconeIsColimit.{u, u} F) - (SemiRing.FilteredColimits.colimitCoconeIsColimit - (F ⋙ forget₂ CommSemiRing SemiRing.{u})) } -#align CommSemiRing.filtered_colimits.forget₂_SemiRing_preserves_filtered_colimits CommSemiRing.FilteredColimits.forget₂SemiRingPreservesFilteredColimits + (SemiRingCat.FilteredColimits.colimitCoconeIsColimit + (F ⋙ forget₂ CommSemiRingCat SemiRingCat.{u})) } +#align CommSemiRing.filtered_colimits.forget₂_SemiRing_preserves_filtered_colimits CommSemiRingCat.FilteredColimits.forget₂SemiRingPreservesFilteredColimits -instance forgetPreservesFilteredColimits : PreservesFilteredColimits (forget CommSemiRing.{u}) := - Limits.compPreservesFilteredColimits (forget₂ CommSemiRing SemiRing) (forget SemiRing.{u}) -#align CommSemiRing.filtered_colimits.forget_preserves_filtered_colimits CommSemiRing.FilteredColimits.forgetPreservesFilteredColimits +instance forgetPreservesFilteredColimits : PreservesFilteredColimits (forget CommSemiRingCat.{u}) := + Limits.compPreservesFilteredColimits (forget₂ CommSemiRingCat SemiRingCat) + (forget SemiRingCat.{u}) +#align CommSemiRing.filtered_colimits.forget_preserves_filtered_colimits CommSemiRingCat.FilteredColimits.forgetPreservesFilteredColimits end -end CommSemiRing.FilteredColimits +end CommSemiRingCat.FilteredColimits namespace RingCat.FilteredColimits @@ -249,8 +254,8 @@ parameter {J : Type v}[SmallCategory J][IsFiltered J](F : J ⥤ RingCat.{max v u /-- The colimit of `F ⋙ forget₂ Ring SemiRing` in the category `SemiRing`. In the following, we will show that this has the structure of a ring. -/ -abbrev r : SemiRing := - SemiRing.FilteredColimits.colimit (F ⋙ forget₂ RingCat SemiRing.{max v u}) +abbrev r : SemiRingCat := + SemiRingCat.FilteredColimits.colimit (F ⋙ forget₂ RingCat SemiRingCat.{max v u}) #align Ring.filtered_colimits.R RingCat.FilteredColimits.r instance colimitRing : Ring R := @@ -267,15 +272,19 @@ def colimit : RingCat := /-- The cocone over the proposed colimit ring. -/ def colimitCocone : cocone F where pt := colimit - ι := { (SemiRing.FilteredColimits.colimitCocone (F ⋙ forget₂ RingCat SemiRing.{max v u})).ι with } + ι := + { + (SemiRingCat.FilteredColimits.colimitCocone + (F ⋙ forget₂ RingCat SemiRingCat.{max v u})).ι with } #align Ring.filtered_colimits.colimit_cocone RingCat.FilteredColimits.colimitCocone /-- The proposed colimit cocone is a colimit in `Ring`. -/ def colimitCoconeIsColimit : IsColimit colimit_cocone where desc t := - (SemiRing.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ RingCat SemiRing.{max v u})).desc - ((forget₂ RingCat SemiRing).mapCocone t) + (SemiRingCat.FilteredColimits.colimitCoconeIsColimit + (F ⋙ forget₂ RingCat SemiRingCat.{max v u})).desc + ((forget₂ RingCat SemiRingCat).mapCocone t) fac t j := RingHom.coe_inj <| (Types.colimitCoconeIsColimit (F ⋙ forget RingCat)).fac ((forget RingCat).mapCocone t) j @@ -286,16 +295,17 @@ def colimitCoconeIsColimit : IsColimit colimit_cocone #align Ring.filtered_colimits.colimit_cocone_is_colimit RingCat.FilteredColimits.colimitCoconeIsColimit instance forget₂SemiRingPreservesFilteredColimits : - PreservesFilteredColimits (forget₂ RingCat SemiRing.{u}) + PreservesFilteredColimits (forget₂ RingCat SemiRingCat.{u}) where PreservesFilteredColimits J _ _ := { PreservesColimit := fun F => preserves_colimit_of_preserves_colimit_cocone (colimitCoconeIsColimit.{u, u} F) - (SemiRing.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ RingCat SemiRing.{u})) } + (SemiRingCat.FilteredColimits.colimitCoconeIsColimit + (F ⋙ forget₂ RingCat SemiRingCat.{u})) } #align Ring.filtered_colimits.forget₂_SemiRing_preserves_filtered_colimits RingCat.FilteredColimits.forget₂SemiRingPreservesFilteredColimits instance forgetPreservesFilteredColimits : PreservesFilteredColimits (forget RingCat.{u}) := - Limits.compPreservesFilteredColimits (forget₂ RingCat SemiRing) (forget SemiRing.{u}) + Limits.compPreservesFilteredColimits (forget₂ RingCat SemiRingCat) (forget SemiRingCat.{u}) #align Ring.filtered_colimits.forget_preserves_filtered_colimits RingCat.FilteredColimits.forgetPreservesFilteredColimits end @@ -319,8 +329,8 @@ abbrev r : RingCat := instance colimitCommRing : CommRing R := { R.Ring, - CommSemiRing.FilteredColimits.colimitCommSemiring - (F ⋙ forget₂ CommRingCat CommSemiRing.{max v u}) with } + CommSemiRingCat.FilteredColimits.colimitCommSemiring + (F ⋙ forget₂ CommRingCat CommSemiRingCat.{max v u}) with } #align CommRing.filtered_colimits.colimit_comm_ring CommRingCat.FilteredColimits.colimitCommRing /-- The bundled commutative ring giving the filtered colimit of a diagram. -/ diff --git a/Mathbin/Algebra/Category/Ring/Instances.lean b/Mathbin/Algebra/Category/Ring/Instances.lean index a2e282e9be..fb6bedc996 100644 --- a/Mathbin/Algebra/Category/Ring/Instances.lean +++ b/Mathbin/Algebra/Category/Ring/Instances.lean @@ -21,7 +21,7 @@ open CategoryTheory instance localization_unit_isIso (R : CommRingCat) : IsIso (CommRingCat.ofHom <| algebraMap R (Localization.Away (1 : R))) := - IsIso.of_iso (IsLocalization.atOne R (Localization.Away (1 : R))).toRingEquiv.toCommRingIso + IsIso.of_iso (IsLocalization.atOne R (Localization.Away (1 : R))).toRingEquiv.toCommRingCatIso #align localization_unit_is_iso localization_unit_isIso instance localization_unit_is_iso' (R : CommRingCat) : diff --git a/Mathbin/Algebra/Category/Ring/Limits.lean b/Mathbin/Algebra/Category/Ring/Limits.lean index add9d0d26d..4d8d238f9a 100644 --- a/Mathbin/Algebra/Category/Ring/Limits.lean +++ b/Mathbin/Algebra/Category/Ring/Limits.lean @@ -38,40 +38,42 @@ universe v u noncomputable section -namespace SemiRing +namespace SemiRingCat variable {J : Type v} [SmallCategory J] -instance semiringObj (F : J ⥤ SemiRing.{max v u}) (j) : Semiring ((F ⋙ forget SemiRing).obj j) := +instance semiringObj (F : J ⥤ SemiRingCat.{max v u}) (j) : + Semiring ((F ⋙ forget SemiRingCat).obj j) := by change Semiring (F.obj j) infer_instance -#align SemiRing.semiring_obj SemiRing.semiringObj +#align SemiRing.semiring_obj SemiRingCat.semiringObj /-- The flat sections of a functor into `SemiRing` form a subsemiring of all sections. -/ -def sectionsSubsemiring (F : J ⥤ SemiRing.{max v u}) : Subsemiring (∀ j, F.obj j) := +def sectionsSubsemiring (F : J ⥤ SemiRingCat.{max v u}) : Subsemiring (∀ j, F.obj j) := { AddMonCat.sectionsAddSubmonoid - (F ⋙ forget₂ SemiRing AddCommMonCat.{max v u} ⋙ forget₂ AddCommMonCat AddMonCat.{max v u}), - MonCat.sectionsSubmonoid (F ⋙ forget₂ SemiRing MonCat.{max v u}) with - carrier := (F ⋙ forget SemiRing).sections } -#align SemiRing.sections_subsemiring SemiRing.sectionsSubsemiring + (F ⋙ forget₂ SemiRingCat AddCommMonCat.{max v u} ⋙ forget₂ AddCommMonCat AddMonCat.{max v u}), + MonCat.sectionsSubmonoid (F ⋙ forget₂ SemiRingCat MonCat.{max v u}) with + carrier := (F ⋙ forget SemiRingCat).sections } +#align SemiRing.sections_subsemiring SemiRingCat.sectionsSubsemiring -instance limitSemiring (F : J ⥤ SemiRing.{max v u}) : - Semiring (Types.limitCone (F ⋙ forget SemiRing.{max v u})).pt := +instance limitSemiring (F : J ⥤ SemiRingCat.{max v u}) : + Semiring (Types.limitCone (F ⋙ forget SemiRingCat.{max v u})).pt := (sectionsSubsemiring F).toSemiring -#align SemiRing.limit_semiring SemiRing.limitSemiring +#align SemiRing.limit_semiring SemiRingCat.limitSemiring /-- `limit.π (F ⋙ forget SemiRing) j` as a `ring_hom`. -/ -def limitπRingHom (F : J ⥤ SemiRing.{max v u}) (j) : - (Types.limitCone (F ⋙ forget SemiRing)).pt →+* (F ⋙ forget SemiRing).obj j := +def limitπRingHom (F : J ⥤ SemiRingCat.{max v u}) (j) : + (Types.limitCone (F ⋙ forget SemiRingCat)).pt →+* (F ⋙ forget SemiRingCat).obj j := { AddMonCat.limitπAddMonoidHom - (F ⋙ forget₂ SemiRing AddCommMonCat.{max v u} ⋙ forget₂ AddCommMonCat AddMonCat.{max v u}) j, - MonCat.limitπMonoidHom (F ⋙ forget₂ SemiRing MonCat.{max v u}) j with - toFun := (Types.limitCone (F ⋙ forget SemiRing)).π.app j } -#align SemiRing.limit_π_ring_hom SemiRing.limitπRingHom + (F ⋙ forget₂ SemiRingCat AddCommMonCat.{max v u} ⋙ forget₂ AddCommMonCat AddMonCat.{max v u}) + j, + MonCat.limitπMonoidHom (F ⋙ forget₂ SemiRingCat MonCat.{max v u}) j with + toFun := (Types.limitCone (F ⋙ forget SemiRingCat)).π.app j } +#align SemiRing.limit_π_ring_hom SemiRingCat.limitπRingHom namespace HasLimits @@ -81,24 +83,24 @@ namespace HasLimits /-- Construction of a limit cone in `SemiRing`. (Internal use only; use the limits API.) -/ -def limitCone (F : J ⥤ SemiRing.{max v u}) : Cone F +def limitCone (F : J ⥤ SemiRingCat.{max v u}) : Cone F where - pt := SemiRing.of (Types.limitCone (F ⋙ forget _)).pt + pt := SemiRingCat.of (Types.limitCone (F ⋙ forget _)).pt π := { app := limitπRingHom F naturality' := fun j j' f => RingHom.coe_inj ((Types.limitCone (F ⋙ forget _)).π.naturality f) } -#align SemiRing.has_limits.limit_cone SemiRing.HasLimits.limitCone +#align SemiRing.has_limits.limit_cone SemiRingCat.HasLimits.limitCone /-- Witness that the limit cone in `SemiRing` is a limit cone. (Internal use only; use the limits API.) -/ -def limitConeIsLimit (F : J ⥤ SemiRing.{max v u}) : IsLimit (limitCone F) := by +def limitConeIsLimit (F : J ⥤ SemiRingCat.{max v u}) : IsLimit (limitCone F) := by refine' - is_limit.of_faithful (forget SemiRing) (types.limit_cone_is_limit _) + is_limit.of_faithful (forget SemiRingCat) (types.limit_cone_is_limit _) (fun s => ⟨_, _, _, _, _⟩) fun s => rfl <;> tidy -#align SemiRing.has_limits.limit_cone_is_limit SemiRing.HasLimits.limitConeIsLimit +#align SemiRing.has_limits.limit_cone_is_limit SemiRingCat.HasLimits.limitConeIsLimit end HasLimits @@ -106,7 +108,7 @@ open HasLimits /- ./././Mathport/Syntax/Translate/Command.lean:322:38: unsupported irreducible non-definition -/ /-- The category of rings has all limits. -/ -irreducible_def hasLimitsOfSize : HasLimitsOfSize.{v} SemiRing.{max v u} := +irreducible_def hasLimitsOfSize : HasLimitsOfSize.{v} SemiRingCat.{max v u} := { HasLimitsOfShape := fun J 𝒥 => { @@ -114,163 +116,170 @@ irreducible_def hasLimitsOfSize : HasLimitsOfSize.{v} SemiRing.{max v u} := has_limit.mk { Cone := limit_cone F IsLimit := limit_cone_is_limit F } } } -#align SemiRing.has_limits_of_size SemiRing.hasLimitsOfSize +#align SemiRing.has_limits_of_size SemiRingCat.hasLimitsOfSize -instance hasLimits : HasLimits SemiRing.{u} := - SemiRing.hasLimitsOfSize.{u, u} -#align SemiRing.has_limits SemiRing.hasLimits +instance hasLimits : HasLimits SemiRingCat.{u} := + SemiRingCat.hasLimitsOfSize.{u, u} +#align SemiRing.has_limits SemiRingCat.hasLimits /-- An auxiliary declaration to speed up typechecking. -/ -def forget₂AddCommMonPreservesLimitsAux (F : J ⥤ SemiRing.{max v u}) : - IsLimit ((forget₂ SemiRing AddCommMonCat).mapCone (limitCone F)) := by - apply AddCommMonCat.limitConeIsLimit (F ⋙ forget₂ SemiRing AddCommMonCat.{max v u}) -#align SemiRing.forget₂_AddCommMon_preserves_limits_aux SemiRing.forget₂AddCommMonPreservesLimitsAux +def forget₂AddCommMonPreservesLimitsAux (F : J ⥤ SemiRingCat.{max v u}) : + IsLimit ((forget₂ SemiRingCat AddCommMonCat).mapCone (limitCone F)) := by + apply AddCommMonCat.limitConeIsLimit (F ⋙ forget₂ SemiRingCat AddCommMonCat.{max v u}) +#align SemiRing.forget₂_AddCommMon_preserves_limits_aux SemiRingCat.forget₂AddCommMonPreservesLimitsAux /-- The forgetful functor from semirings to additive commutative monoids preserves all limits. -/ instance forget₂AddCommMonPreservesLimitsOfSize : - PreservesLimitsOfSize.{v, v} (forget₂ SemiRing AddCommMonCat.{max v u}) + PreservesLimitsOfSize.{v, v} (forget₂ SemiRingCat AddCommMonCat.{max v u}) where PreservesLimitsOfShape J 𝒥 := { PreservesLimit := fun F => preserves_limit_of_preserves_limit_cone (limit_cone_is_limit F) (forget₂_AddCommMon_preserves_limits_aux F) } -#align SemiRing.forget₂_AddCommMon_preserves_limits_of_size SemiRing.forget₂AddCommMonPreservesLimitsOfSize +#align SemiRing.forget₂_AddCommMon_preserves_limits_of_size SemiRingCat.forget₂AddCommMonPreservesLimitsOfSize -instance forget₂AddCommMonPreservesLimits : PreservesLimits (forget₂ SemiRing AddCommMonCat.{u}) := - SemiRing.forget₂AddCommMonPreservesLimitsOfSize.{u, u} -#align SemiRing.forget₂_AddCommMon_preserves_limits SemiRing.forget₂AddCommMonPreservesLimits +instance forget₂AddCommMonPreservesLimits : + PreservesLimits (forget₂ SemiRingCat AddCommMonCat.{u}) := + SemiRingCat.forget₂AddCommMonPreservesLimitsOfSize.{u, u} +#align SemiRing.forget₂_AddCommMon_preserves_limits SemiRingCat.forget₂AddCommMonPreservesLimits /-- An auxiliary declaration to speed up typechecking. -/ -def forget₂MonPreservesLimitsAux (F : J ⥤ SemiRing.{max v u}) : - IsLimit ((forget₂ SemiRing MonCat).mapCone (limitCone F)) := by - apply MonCat.HasLimits.limitConeIsLimit (F ⋙ forget₂ SemiRing MonCat.{max v u}) -#align SemiRing.forget₂_Mon_preserves_limits_aux SemiRing.forget₂MonPreservesLimitsAux +def forget₂MonPreservesLimitsAux (F : J ⥤ SemiRingCat.{max v u}) : + IsLimit ((forget₂ SemiRingCat MonCat).mapCone (limitCone F)) := by + apply MonCat.HasLimits.limitConeIsLimit (F ⋙ forget₂ SemiRingCat MonCat.{max v u}) +#align SemiRing.forget₂_Mon_preserves_limits_aux SemiRingCat.forget₂MonPreservesLimitsAux /-- The forgetful functor from semirings to monoids preserves all limits. -/ instance forget₂MonPreservesLimitsOfSize : - PreservesLimitsOfSize.{v, v} (forget₂ SemiRing MonCat.{max v u}) + PreservesLimitsOfSize.{v, v} (forget₂ SemiRingCat MonCat.{max v u}) where PreservesLimitsOfShape J 𝒥 := { PreservesLimit := fun F => preserves_limit_of_preserves_limit_cone (limit_cone_is_limit F) (forget₂_Mon_preserves_limits_aux F) } -#align SemiRing.forget₂_Mon_preserves_limits_of_size SemiRing.forget₂MonPreservesLimitsOfSize +#align SemiRing.forget₂_Mon_preserves_limits_of_size SemiRingCat.forget₂MonPreservesLimitsOfSize -instance forget₂MonPreservesLimits : PreservesLimits (forget₂ SemiRing MonCat.{u}) := - SemiRing.forget₂MonPreservesLimitsOfSize.{u, u} -#align SemiRing.forget₂_Mon_preserves_limits SemiRing.forget₂MonPreservesLimits +instance forget₂MonPreservesLimits : PreservesLimits (forget₂ SemiRingCat MonCat.{u}) := + SemiRingCat.forget₂MonPreservesLimitsOfSize.{u, u} +#align SemiRing.forget₂_Mon_preserves_limits SemiRingCat.forget₂MonPreservesLimits /-- The forgetful functor from semirings to types preserves all limits. -/ -instance forgetPreservesLimitsOfSize : PreservesLimitsOfSize.{v, v} (forget SemiRing.{max v u}) +instance forgetPreservesLimitsOfSize : PreservesLimitsOfSize.{v, v} (forget SemiRingCat.{max v u}) where PreservesLimitsOfShape J 𝒥 := { PreservesLimit := fun F => preserves_limit_of_preserves_limit_cone (limit_cone_is_limit F) (types.limit_cone_is_limit (F ⋙ forget _)) } -#align SemiRing.forget_preserves_limits_of_size SemiRing.forgetPreservesLimitsOfSize +#align SemiRing.forget_preserves_limits_of_size SemiRingCat.forgetPreservesLimitsOfSize -instance forgetPreservesLimits : PreservesLimits (forget SemiRing.{u}) := - SemiRing.forgetPreservesLimitsOfSize.{u, u} -#align SemiRing.forget_preserves_limits SemiRing.forgetPreservesLimits +instance forgetPreservesLimits : PreservesLimits (forget SemiRingCat.{u}) := + SemiRingCat.forgetPreservesLimitsOfSize.{u, u} +#align SemiRing.forget_preserves_limits SemiRingCat.forgetPreservesLimits -end SemiRing +end SemiRingCat -namespace CommSemiRing +namespace CommSemiRingCat variable {J : Type v} [SmallCategory J] -instance commSemiringObj (F : J ⥤ CommSemiRing.{max v u}) (j) : - CommSemiring ((F ⋙ forget CommSemiRing).obj j) := +instance commSemiringObj (F : J ⥤ CommSemiRingCat.{max v u}) (j) : + CommSemiring ((F ⋙ forget CommSemiRingCat).obj j) := by change CommSemiring (F.obj j) infer_instance -#align CommSemiRing.comm_semiring_obj CommSemiRing.commSemiringObj +#align CommSemiRing.comm_semiring_obj CommSemiRingCat.commSemiringObj -instance limitCommSemiring (F : J ⥤ CommSemiRing.{max v u}) : - CommSemiring (Types.limitCone (F ⋙ forget CommSemiRing.{max v u})).pt := +instance limitCommSemiring (F : J ⥤ CommSemiRingCat.{max v u}) : + CommSemiring (Types.limitCone (F ⋙ forget CommSemiRingCat.{max v u})).pt := @Subsemiring.toCommSemiring (∀ j, F.obj j) _ - (SemiRing.sectionsSubsemiring (F ⋙ forget₂ CommSemiRing SemiRing.{max v u})) -#align CommSemiRing.limit_comm_semiring CommSemiRing.limitCommSemiring + (SemiRingCat.sectionsSubsemiring (F ⋙ forget₂ CommSemiRingCat SemiRingCat.{max v u})) +#align CommSemiRing.limit_comm_semiring CommSemiRingCat.limitCommSemiring /-- We show that the forgetful functor `CommSemiRing ⥤ SemiRing` creates limits. All we need to do is notice that the limit point has a `comm_semiring` instance available, and then reuse the existing limit. -/ -instance (F : J ⥤ CommSemiRing.{max v u}) : - CreatesLimit F (forget₂ CommSemiRing SemiRing.{max v u}) := +instance (F : J ⥤ CommSemiRingCat.{max v u}) : + CreatesLimit F (forget₂ CommSemiRingCat SemiRingCat.{max v u}) := createsLimitOfReflectsIso fun c' t => { liftedCone := { pt := CommSemiRing.of (Types.limitCone (F ⋙ forget _)).pt π := - { app := by apply SemiRing.limitπRingHom (F ⋙ forget₂ CommSemiRing SemiRing.{max v u}) + { app := by + apply SemiRingCat.limitπRingHom (F ⋙ forget₂ CommSemiRingCat SemiRingCat.{max v u}) naturality' := - (SemiRing.HasLimits.limitCone - (F ⋙ forget₂ CommSemiRing SemiRing.{max v u})).π.naturality } } - validLift := by apply is_limit.unique_up_to_iso (SemiRing.HasLimits.limitConeIsLimit _) t + (SemiRingCat.HasLimits.limitCone + (F ⋙ forget₂ CommSemiRingCat SemiRingCat.{max v u})).π.naturality } } + validLift := by apply is_limit.unique_up_to_iso (SemiRingCat.HasLimits.limitConeIsLimit _) t makesLimit := - IsLimit.ofFaithful (forget₂ CommSemiRing SemiRing.{max v u}) - (by apply SemiRing.HasLimits.limitConeIsLimit _) - (fun s => (SemiRing.HasLimits.limitConeIsLimit _).lift ((forget₂ _ SemiRing).mapCone s)) + IsLimit.ofFaithful (forget₂ CommSemiRingCat SemiRingCat.{max v u}) + (by apply SemiRingCat.HasLimits.limitConeIsLimit _) + (fun s => + (SemiRingCat.HasLimits.limitConeIsLimit _).lift ((forget₂ _ SemiRingCat).mapCone s)) fun s => rfl } /-- A choice of limit cone for a functor into `CommSemiRing`. (Generally, you'll just want to use `limit F`.) -/ -def limitCone (F : J ⥤ CommSemiRing.{max v u}) : Cone F := - liftLimit (limit.isLimit (F ⋙ forget₂ CommSemiRing SemiRing.{max v u})) -#align CommSemiRing.limit_cone CommSemiRing.limitCone +def limitCone (F : J ⥤ CommSemiRingCat.{max v u}) : Cone F := + liftLimit (limit.isLimit (F ⋙ forget₂ CommSemiRingCat SemiRingCat.{max v u})) +#align CommSemiRing.limit_cone CommSemiRingCat.limitCone /-- The chosen cone is a limit cone. (Generally, you'll just want to use `limit.cone F`.) -/ -def limitConeIsLimit (F : J ⥤ CommSemiRing.{max v u}) : IsLimit (limitCone F) := +def limitConeIsLimit (F : J ⥤ CommSemiRingCat.{max v u}) : IsLimit (limitCone F) := liftedLimitIsLimit _ -#align CommSemiRing.limit_cone_is_limit CommSemiRing.limitConeIsLimit +#align CommSemiRing.limit_cone_is_limit CommSemiRingCat.limitConeIsLimit /- ./././Mathport/Syntax/Translate/Command.lean:322:38: unsupported irreducible non-definition -/ /-- The category of rings has all limits. -/ -irreducible_def hasLimitsOfSize : HasLimitsOfSize.{v, v} CommSemiRing.{max v u} := +irreducible_def hasLimitsOfSize : HasLimitsOfSize.{v, v} CommSemiRingCat.{max v u} := { HasLimitsOfShape := fun J 𝒥 => - { HasLimit := fun F => has_limit_of_created F (forget₂ CommSemiRing SemiRing.{max v u}) } } -#align CommSemiRing.has_limits_of_size CommSemiRing.hasLimitsOfSize + { + HasLimit := fun F => + has_limit_of_created F (forget₂ CommSemiRingCat SemiRingCat.{max v u}) } } +#align CommSemiRing.has_limits_of_size CommSemiRingCat.hasLimitsOfSize -instance hasLimits : HasLimits CommSemiRing.{u} := - CommSemiRing.hasLimitsOfSize.{u, u} -#align CommSemiRing.has_limits CommSemiRing.hasLimits +instance hasLimits : HasLimits CommSemiRingCat.{u} := + CommSemiRingCat.hasLimitsOfSize.{u, u} +#align CommSemiRing.has_limits CommSemiRingCat.hasLimits /-- The forgetful functor from rings to semirings preserves all limits. -/ instance forget₂SemiRingPreservesLimitsOfSize : - PreservesLimitsOfSize.{v, v} (forget₂ CommSemiRing SemiRing.{max v u}) + PreservesLimitsOfSize.{v, v} (forget₂ CommSemiRingCat SemiRingCat.{max v u}) where PreservesLimitsOfShape J 𝒥 := { PreservesLimit := fun F => by infer_instance } -#align CommSemiRing.forget₂_SemiRing_preserves_limits_of_size CommSemiRing.forget₂SemiRingPreservesLimitsOfSize +#align CommSemiRing.forget₂_SemiRing_preserves_limits_of_size CommSemiRingCat.forget₂SemiRingPreservesLimitsOfSize -instance forget₂SemiRingPreservesLimits : PreservesLimits (forget₂ CommSemiRing SemiRing.{u}) := - CommSemiRing.forget₂SemiRingPreservesLimitsOfSize.{u, u} -#align CommSemiRing.forget₂_SemiRing_preserves_limits CommSemiRing.forget₂SemiRingPreservesLimits +instance forget₂SemiRingPreservesLimits : + PreservesLimits (forget₂ CommSemiRingCat SemiRingCat.{u}) := + CommSemiRingCat.forget₂SemiRingPreservesLimitsOfSize.{u, u} +#align CommSemiRing.forget₂_SemiRing_preserves_limits CommSemiRingCat.forget₂SemiRingPreservesLimits /-- The forgetful functor from rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.) -/ -instance forgetPreservesLimitsOfSize : PreservesLimitsOfSize.{v, v} (forget CommSemiRing.{max v u}) +instance forgetPreservesLimitsOfSize : + PreservesLimitsOfSize.{v, v} (forget CommSemiRingCat.{max v u}) where PreservesLimitsOfShape J 𝒥 := { PreservesLimit := fun F => - limits.comp_preserves_limit (forget₂ CommSemiRing SemiRing) (forget SemiRing) } -#align CommSemiRing.forget_preserves_limits_of_size CommSemiRing.forgetPreservesLimitsOfSize + limits.comp_preserves_limit (forget₂ CommSemiRingCat SemiRingCat) (forget SemiRingCat) } +#align CommSemiRing.forget_preserves_limits_of_size CommSemiRingCat.forgetPreservesLimitsOfSize -instance forgetPreservesLimits : PreservesLimits (forget CommSemiRing.{u}) := - CommSemiRing.forgetPreservesLimitsOfSize.{u, u} -#align CommSemiRing.forget_preserves_limits CommSemiRing.forgetPreservesLimits +instance forgetPreservesLimits : PreservesLimits (forget CommSemiRingCat.{u}) := + CommSemiRingCat.forgetPreservesLimitsOfSize.{u, u} +#align CommSemiRing.forget_preserves_limits CommSemiRingCat.forgetPreservesLimits -end CommSemiRing +end CommSemiRingCat namespace RingCat @@ -289,7 +298,7 @@ def sectionsSubring (F : J ⥤ RingCat.{max v u}) : Subring (∀ j, F.obj j) := AddGroupCat.sectionsAddSubgroup (F ⋙ forget₂ RingCat AddCommGroupCat.{max v u} ⋙ forget₂ AddCommGroupCat AddGroupCat.{max v u}), - SemiRing.sectionsSubsemiring (F ⋙ forget₂ RingCat SemiRing.{max v u}) with + SemiRingCat.sectionsSubsemiring (F ⋙ forget₂ RingCat SemiRingCat.{max v u}) with carrier := (F ⋙ forget RingCat).sections } #align Ring.sections_subring RingCat.sectionsSubring @@ -303,25 +312,25 @@ instance limitRing (F : J ⥤ RingCat.{max v u}) : All we need to do is notice that the limit point has a `ring` instance available, and then reuse the existing limit. -/ -instance (F : J ⥤ RingCat.{max v u}) : CreatesLimit F (forget₂ RingCat SemiRing.{max v u}) := +instance (F : J ⥤ RingCat.{max v u}) : CreatesLimit F (forget₂ RingCat SemiRingCat.{max v u}) := createsLimitOfReflectsIso fun c' t => { liftedCone := { pt := RingCat.of (Types.limitCone (F ⋙ forget _)).pt π := - { app := by apply SemiRing.limitπRingHom (F ⋙ forget₂ RingCat SemiRing.{max v u}) + { app := by apply SemiRingCat.limitπRingHom (F ⋙ forget₂ RingCat SemiRingCat.{max v u}) naturality' := - (SemiRing.HasLimits.limitCone - (F ⋙ forget₂ RingCat SemiRing.{max v u})).π.naturality } } - validLift := by apply is_limit.unique_up_to_iso (SemiRing.HasLimits.limitConeIsLimit _) t + (SemiRingCat.HasLimits.limitCone + (F ⋙ forget₂ RingCat SemiRingCat.{max v u})).π.naturality } } + validLift := by apply is_limit.unique_up_to_iso (SemiRingCat.HasLimits.limitConeIsLimit _) t makesLimit := - IsLimit.ofFaithful (forget₂ RingCat SemiRing.{max v u}) - (by apply SemiRing.HasLimits.limitConeIsLimit _) (fun s => _) fun s => rfl } + IsLimit.ofFaithful (forget₂ RingCat SemiRingCat.{max v u}) + (by apply SemiRingCat.HasLimits.limitConeIsLimit _) (fun s => _) fun s => rfl } /-- A choice of limit cone for a functor into `Ring`. (Generally, you'll just want to use `limit F`.) -/ def limitCone (F : J ⥤ RingCat.{max v u}) : Cone F := - liftLimit (limit.isLimit (F ⋙ forget₂ RingCat SemiRing.{max v u})) + liftLimit (limit.isLimit (F ⋙ forget₂ RingCat SemiRingCat.{max v u})) #align Ring.limit_cone RingCat.limitCone /-- The chosen cone is a limit cone. @@ -336,7 +345,7 @@ def limitConeIsLimit (F : J ⥤ RingCat.{max v u}) : IsLimit (limitCone F) := irreducible_def hasLimitsOfSize : HasLimitsOfSize.{v, v} RingCat.{max v u} := { HasLimitsOfShape := fun J 𝒥 => - { HasLimit := fun F => has_limit_of_created F (forget₂ RingCat SemiRing.{max v u}) } } + { HasLimit := fun F => has_limit_of_created F (forget₂ RingCat SemiRingCat.{max v u}) } } #align Ring.has_limits_of_size RingCat.hasLimitsOfSize instance hasLimits : HasLimits RingCat.{u} := @@ -346,11 +355,11 @@ instance hasLimits : HasLimits RingCat.{u} := /-- The forgetful functor from rings to semirings preserves all limits. -/ instance forget₂SemiRingPreservesLimitsOfSize : - PreservesLimitsOfSize.{v, v} (forget₂ RingCat SemiRing.{max v u}) + PreservesLimitsOfSize.{v, v} (forget₂ RingCat SemiRingCat.{max v u}) where PreservesLimitsOfShape J 𝒥 := { PreservesLimit := fun F => by infer_instance } #align Ring.forget₂_SemiRing_preserves_limits_of_size RingCat.forget₂SemiRingPreservesLimitsOfSize -instance forget₂SemiRingPreservesLimits : PreservesLimits (forget₂ RingCat SemiRing.{u}) := +instance forget₂SemiRingPreservesLimits : PreservesLimits (forget₂ RingCat SemiRingCat.{u}) := RingCat.forget₂SemiRingPreservesLimitsOfSize.{u, u} #align Ring.forget₂_SemiRing_preserves_limits RingCat.forget₂SemiRingPreservesLimits @@ -384,7 +393,7 @@ instance forgetPreservesLimitsOfSize : PreservesLimitsOfSize.{v, v} (forget Ring where PreservesLimitsOfShape J 𝒥 := { PreservesLimit := fun F => - limits.comp_preserves_limit (forget₂ RingCat SemiRing) (forget SemiRing.{max v u}) } + limits.comp_preserves_limit (forget₂ RingCat SemiRingCat) (forget SemiRingCat.{max v u}) } #align Ring.forget_preserves_limits_of_size RingCat.forgetPreservesLimitsOfSize instance forgetPreservesLimits : PreservesLimits (forget RingCat.{u}) := @@ -430,13 +439,14 @@ instance (F : J ⥤ CommRingCat.{max v u}) : CreatesLimit F (forget₂ CommRingC π := { app := by apply - SemiRing.limitπRingHom - (F ⋙ forget₂ CommRingCat RingCat.{max v u} ⋙ forget₂ RingCat SemiRing.{max v u}) + SemiRingCat.limitπRingHom + (F ⋙ + forget₂ CommRingCat RingCat.{max v u} ⋙ forget₂ RingCat SemiRingCat.{max v u}) naturality' := - (SemiRing.HasLimits.limitCone + (SemiRingCat.HasLimits.limitCone (F ⋙ forget₂ _ RingCat.{max v u} ⋙ - forget₂ _ SemiRing.{max v u})).π.naturality } } + forget₂ _ SemiRingCat.{max v u})).π.naturality } } validLift := by apply is_limit.unique_up_to_iso (RingCat.limitConeIsLimit _) t makesLimit := IsLimit.ofFaithful (forget₂ _ RingCat.{max v u}) @@ -485,8 +495,8 @@ instance forget₂RingPreservesLimits : PreservesLimits (forget₂ CommRingCat R /-- An auxiliary declaration to speed up typechecking. -/ def forget₂CommSemiRingPreservesLimitsAux (F : J ⥤ CommRingCat.{max v u}) : - IsLimit ((forget₂ CommRingCat CommSemiRing).mapCone (limitCone F)) := by - apply CommSemiRing.limitConeIsLimit (F ⋙ forget₂ CommRingCat CommSemiRing.{max v u}) + IsLimit ((forget₂ CommRingCat CommSemiRingCat).mapCone (limitCone F)) := by + apply CommSemiRingCat.limitConeIsLimit (F ⋙ forget₂ CommRingCat CommSemiRingCat.{max v u}) #align CommRing.forget₂_CommSemiRing_preserves_limits_aux CommRingCat.forget₂CommSemiRingPreservesLimitsAux /-- The forgetful functor from commutative rings to commutative semirings preserves all limits. @@ -494,7 +504,7 @@ def forget₂CommSemiRingPreservesLimitsAux (F : J ⥤ CommRingCat.{max v u}) : in the category of commutative semirings.) -/ instance forget₂CommSemiRingPreservesLimitsOfSize : - PreservesLimitsOfSize.{v, v} (forget₂ CommRingCat CommSemiRing.{max v u}) + PreservesLimitsOfSize.{v, v} (forget₂ CommRingCat CommSemiRingCat.{max v u}) where PreservesLimitsOfShape J 𝒥 := { PreservesLimit := fun F => @@ -503,7 +513,7 @@ instance forget₂CommSemiRingPreservesLimitsOfSize : #align CommRing.forget₂_CommSemiRing_preserves_limits_of_size CommRingCat.forget₂CommSemiRingPreservesLimitsOfSize instance forget₂CommSemiRingPreservesLimits : - PreservesLimits (forget₂ CommRingCat CommSemiRing.{u}) := + PreservesLimits (forget₂ CommRingCat CommSemiRingCat.{u}) := CommRingCat.forget₂CommSemiRingPreservesLimitsOfSize.{u, u} #align CommRing.forget₂_CommSemiRing_preserves_limits CommRingCat.forget₂CommSemiRingPreservesLimits diff --git a/Mathbin/AlgebraicGeometry/AffineScheme.lean b/Mathbin/AlgebraicGeometry/AffineScheme.lean index 4087f3d567..9b27ef5949 100644 --- a/Mathbin/AlgebraicGeometry/AffineScheme.lean +++ b/Mathbin/AlgebraicGeometry/AffineScheme.lean @@ -504,7 +504,7 @@ theorem is_localization_basicOpen {X : Scheme} {U : Opens X.carrier} (hU : IsAff (as_iso <| basic_open_sections_to_affine hU f ≫ (Scheme.Spec.obj _).Presheaf.map - (eq_to_hom (basic_open_eq_of_affine _).symm).op).commRingIsoToRingEquiv).mpr + (eq_to_hom (basic_open_eq_of_affine _).symm).op).commRingCatIsoToRingEquiv).mpr convert structure_sheaf.is_localization.to_basic_open _ f change _ ≫ basic_open_sections_to_affine hU f ≫ _ = _ delta basic_open_sections_to_affine @@ -635,7 +635,7 @@ theorem IsAffineOpen.is_localization_stalk {X : Scheme} {U : Opens X.carrier} (h subst this apply (IsLocalization.isLocalization_iff_of_ringEquiv _ - (as_iso <| PresheafedSpace.stalk_map hU.from_Spec.1 y).commRingIsoToRingEquiv).mpr + (as_iso <| PresheafedSpace.stalk_map hU.from_Spec.1 y).commRingCatIsoToRingEquiv).mpr convert structure_sheaf.is_localization.to_stalk _ _ using 1 delta structure_sheaf.stalk_algebra congr 1 diff --git a/Mathbin/AlgebraicGeometry/LocallyRingedSpace.lean b/Mathbin/AlgebraicGeometry/LocallyRingedSpace.lean index e472dd17de..150b24f32d 100644 --- a/Mathbin/AlgebraicGeometry/LocallyRingedSpace.lean +++ b/Mathbin/AlgebraicGeometry/LocallyRingedSpace.lean @@ -231,7 +231,7 @@ def restrict {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : O dsimp at * -- We show that the stalk of the restriction is isomorphic to the original stalk, apply @RingEquiv.localRing _ _ _ (X.local_ring (f x)) - exact (X.to_PresheafedSpace.restrict_stalk_iso h x).symm.commRingIsoToRingEquiv + exact (X.to_PresheafedSpace.restrict_stalk_iso h x).symm.commRingCatIsoToRingEquiv toSheafedSpace := X.toSheafedSpace.restrict h #align algebraic_geometry.LocallyRingedSpace.restrict AlgebraicGeometry.LocallyRingedSpace.restrict diff --git a/Mathbin/AlgebraicGeometry/LocallyRingedSpace/HasColimits.lean b/Mathbin/AlgebraicGeometry/LocallyRingedSpace/HasColimits.lean index 07ebde0350..4d1bcf7e28 100644 --- a/Mathbin/AlgebraicGeometry/LocallyRingedSpace/HasColimits.lean +++ b/Mathbin/AlgebraicGeometry/LocallyRingedSpace/HasColimits.lean @@ -74,7 +74,7 @@ noncomputable def coproduct : LocallyRingedSpace exact (as_iso (PresheafedSpace.stalk_map (colimit.ι (F ⋙ forget_to_SheafedSpace) i : _) - y)).symm.commRingIsoToRingEquiv.LocalRing + y)).symm.commRingCatIsoToRingEquiv.LocalRing #align algebraic_geometry.LocallyRingedSpace.coproduct AlgebraicGeometry.LocallyRingedSpace.coproduct /-- The explicit coproduct cofan for `F : discrete ι ⥤ LocallyRingedSpace`. -/ diff --git a/Mathbin/AlgebraicGeometry/Morphisms/RingHomProperties.lean b/Mathbin/AlgebraicGeometry/Morphisms/RingHomProperties.lean index b8a5efcd58..a5093279e0 100644 --- a/Mathbin/AlgebraicGeometry/Morphisms/RingHomProperties.lean +++ b/Mathbin/AlgebraicGeometry/Morphisms/RingHomProperties.lean @@ -289,12 +289,12 @@ theorem source_affine_locally_of_source_open_cover_aux (h₁ : RingHom.RespectsI rintro ⟨s, r, hr, hs⟩ have := (@Localization.algEquiv _ _ _ _ _ - (@AlgebraicGeometry.Γ_restrict_is_localization _ U.2 s)).toRingEquiv.toCommRingIso + (@AlgebraicGeometry.Γ_restrict_is_localization _ U.2 s)).toRingEquiv.toCommRingCatIso refine' (h₁.cancel_right_is_iso _ (@Localization.algEquiv _ _ _ _ _ (@AlgebraicGeometry.Γ_restrict_is_localization _ U.2 - s)).toRingEquiv.toCommRingIso.Hom).mp + s)).toRingEquiv.toCommRingCatIso.Hom).mp _ subst hs rw [CommRingCat.comp_eq_ring_hom_comp, ← RingHom.comp_assoc] diff --git a/Mathbin/AlgebraicGeometry/OpenImmersion.lean b/Mathbin/AlgebraicGeometry/OpenImmersion.lean index 9497771dda..018083390e 100644 --- a/Mathbin/AlgebraicGeometry/OpenImmersion.lean +++ b/Mathbin/AlgebraicGeometry/OpenImmersion.lean @@ -665,7 +665,7 @@ def toLocallyRingedSpace : LocallyRingedSpace toSheafedSpace := toSheafedSpace Y.toSheafedSpace f LocalRing x := haveI : LocalRing (Y.to_SheafedSpace.to_PresheafedSpace.stalk (f.base x)) := Y.local_ring _ - (as_iso (stalk_map f x)).commRingIsoToRingEquiv.LocalRing + (as_iso (stalk_map f x)).commRingCatIsoToRingEquiv.LocalRing #align algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace @[simp] diff --git a/Mathbin/AlgebraicGeometry/Properties.lean b/Mathbin/AlgebraicGeometry/Properties.lean index a77df21165..beb5bb8ab6 100644 --- a/Mathbin/AlgebraicGeometry/Properties.lean +++ b/Mathbin/AlgebraicGeometry/Properties.lean @@ -99,7 +99,7 @@ theorem isReduced_of_open_immersion {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImme exact isReduced_of_injective (inv <| f.1.c.app (op <| H.base_open.is_open_map.functor.obj U)) (as_iso <| f.1.c.app (op <| H.base_open.is_open_map.functor.obj U) : - Y.presheaf.obj _ ≅ _).symm.commRingIsoToRingEquiv.Injective + Y.presheaf.obj _ ≅ _).symm.commRingCatIsoToRingEquiv.Injective #align algebraic_geometry.is_reduced_of_open_immersion AlgebraicGeometry.isReduced_of_open_immersion instance {R : CommRingCat} [H : IsReduced R] : IsReduced (Scheme.spec.obj <| op R) := @@ -113,7 +113,7 @@ instance {R : CommRingCat} [H : IsReduced R] : IsReduced (Scheme.spec.obj <| op infer_instance exact isReduced_of_injective (structure_sheaf.stalk_iso R x).Hom - (structure_sheaf.stalk_iso R x).commRingIsoToRingEquiv.Injective + (structure_sheaf.stalk_iso R x).commRingCatIsoToRingEquiv.Injective theorem affine_isReduced_iff (R : CommRingCat) : IsReduced (Scheme.spec.obj <| op R) ↔ IsReduced R := @@ -127,7 +127,7 @@ theorem affine_isReduced_iff (R : CommRingCat) : change _root_.is_reduced ((Scheme.Spec.obj <| op R).Presheaf.obj <| op ⊤) infer_instance exact - isReduced_of_injective (to_Spec_Γ R) (as_iso <| to_Spec_Γ R).commRingIsoToRingEquiv.Injective + isReduced_of_injective (to_Spec_Γ R) (as_iso <| to_Spec_Γ R).commRingCatIsoToRingEquiv.Injective #align algebraic_geometry.affine_is_reduced_iff AlgebraicGeometry.affine_isReduced_iff theorem isReduced_of_isAffine_isReduced [IsAffine X] [h : IsReduced (X.Presheaf.obj (op ⊤))] : @@ -335,7 +335,7 @@ theorem isIntegral_of_open_immersion {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImm refine' ⟨⟨_, _, hU.some.prop, rfl⟩⟩ exact (as_iso <| f.1.c.app (op <| H.base_open.is_open_map.functor.obj U) : - Y.presheaf.obj _ ≅ _).symm.commRingIsoToRingEquiv.IsDomain + Y.presheaf.obj _ ≅ _).symm.commRingCatIsoToRingEquiv.IsDomain _ #align algebraic_geometry.is_integral_of_open_immersion AlgebraicGeometry.isIntegral_of_open_immersion @@ -350,7 +350,7 @@ theorem affine_isIntegral_iff (R : CommRingCat) : IsIntegral (Scheme.spec.obj <| op R) ↔ IsDomain R := ⟨fun h => RingEquiv.isDomain ((Scheme.Spec.obj <| op R).Presheaf.obj _) - (as_iso <| to_Spec_Γ R).commRingIsoToRingEquiv, + (as_iso <| to_Spec_Γ R).commRingCatIsoToRingEquiv, fun h => inferInstance⟩ #align algebraic_geometry.affine_is_integral_iff AlgebraicGeometry.affine_isIntegral_iff diff --git a/Mathbin/AlgebraicGeometry/Spec.lean b/Mathbin/AlgebraicGeometry/Spec.lean index ff62b4605b..ee3ed3f2c9 100644 --- a/Mathbin/AlgebraicGeometry/Spec.lean +++ b/Mathbin/AlgebraicGeometry/Spec.lean @@ -195,7 +195,7 @@ def Spec.locallyRingedSpaceObj (R : CommRingCat) : LocallyRingedSpace := { Spec.sheafedSpaceObj R with LocalRing := fun x => @RingEquiv.localRing _ (show LocalRing (Localization.AtPrime _) by infer_instance) _ - (Iso.commRingIsoToRingEquiv <| stalkIso R x).symm } + (Iso.commRingCatIsoToRingEquiv <| stalkIso R x).symm } #align algebraic_geometry.Spec.LocallyRingedSpace_obj AlgebraicGeometry.Spec.locallyRingedSpaceObj @[elementwise] @@ -325,7 +325,7 @@ theorem Spec_map_localization_isIso (R : CommRingCat) (M : Submonoid R) show is_iso (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M - x.as_ideal).toRingEquiv.toCommRingIso.Hom + x.as_ideal).toRingEquiv.toCommRingCatIso.Hom by infer_instance infer_instance #align algebraic_geometry.Spec_map_localization_is_iso AlgebraicGeometry.Spec_map_localization_isIso diff --git a/Mathbin/AlgebraicGeometry/StructureSheaf.lean b/Mathbin/AlgebraicGeometry/StructureSheaf.lean index 457be3e4f8..89155cf0aa 100644 --- a/Mathbin/AlgebraicGeometry/StructureSheaf.lean +++ b/Mathbin/AlgebraicGeometry/StructureSheaf.lean @@ -942,7 +942,7 @@ instance IsLocalization.to_stalk (p : PrimeSpectrum R) : IsLocalization.AtPrime ((structureSheaf R).Presheaf.stalk p) p.asIdeal := by convert(IsLocalization.isLocalization_iff_of_ringEquiv _ - (stalk_iso R p).symm.commRingIsoToRingEquiv).mp + (stalk_iso R p).symm.commRingCatIsoToRingEquiv).mp Localization.isLocalization apply Algebra.algebra_ext intro @@ -967,7 +967,7 @@ instance IsLocalization.to_basicOpen (r : R) : IsLocalization.Away r ((structureSheaf R).val.obj (op <| basicOpen r)) := by convert(IsLocalization.isLocalization_iff_of_ringEquiv _ - (basic_open_iso R r).symm.commRingIsoToRingEquiv).mp + (basic_open_iso R r).symm.commRingCatIsoToRingEquiv).mp Localization.isLocalization apply Algebra.algebra_ext intro x @@ -999,7 +999,7 @@ instance isIso_to_global : IsIso (toOpen R ⊤) := by let hom := CommRingCat.ofHom (algebraMap R (Localization.Away (1 : R))) haveI : is_iso hom := - is_iso.of_iso (IsLocalization.atOne R (Localization.Away (1 : R))).toRingEquiv.toCommRingIso + is_iso.of_iso (IsLocalization.atOne R (Localization.Away (1 : R))).toRingEquiv.toCommRingCatIso rw [to_global_factors R] infer_instance #align algebraic_geometry.structure_sheaf.is_iso_to_global AlgebraicGeometry.StructureSheaf.isIso_to_global diff --git a/Mathbin/RingTheory/RingHomProperties.lean b/Mathbin/RingTheory/RingHomProperties.lean index 4cf7278d74..d7594b3040 100644 --- a/Mathbin/RingTheory/RingHomProperties.lean +++ b/Mathbin/RingTheory/RingHomProperties.lean @@ -54,16 +54,16 @@ variable {P} theorem RespectsIso.cancel_left_isIso (hP : RespectsIso @P) {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) [IsIso f] : P (f ≫ g) ↔ P g := ⟨fun H => by - convert hP.2 (f ≫ g) (as_iso f).symm.commRingIsoToRingEquiv H - exact (is_iso.inv_hom_id_assoc _ _).symm, hP.2 g (asIso f).commRingIsoToRingEquiv⟩ + convert hP.2 (f ≫ g) (as_iso f).symm.commRingCatIsoToRingEquiv H + exact (is_iso.inv_hom_id_assoc _ _).symm, hP.2 g (asIso f).commRingCatIsoToRingEquiv⟩ #align ring_hom.respects_iso.cancel_left_is_iso RingHom.RespectsIso.cancel_left_isIso theorem RespectsIso.cancel_right_isIso (hP : RespectsIso @P) {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) [IsIso g] : P (f ≫ g) ↔ P f := ⟨fun H => by - convert hP.1 (f ≫ g) (as_iso g).symm.commRingIsoToRingEquiv H + convert hP.1 (f ≫ g) (as_iso g).symm.commRingCatIsoToRingEquiv H change f = f ≫ g ≫ inv g - simp, hP.1 f (asIso g).commRingIsoToRingEquiv⟩ + simp, hP.1 f (asIso g).commRingCatIsoToRingEquiv⟩ #align ring_hom.respects_iso.cancel_right_is_iso RingHom.RespectsIso.cancel_right_isIso theorem RespectsIso.is_localization_away_iff (hP : RingHom.RespectsIso @P) {R S : Type _} diff --git a/lake-manifest.json b/lake-manifest.json index ae9572f839..22c3d0ffce 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": "96ad256f1fa49c8584166ef85898d4c45beb0839", + "rev": "c73fd045fad618cb69393119bd7d11cb4cc9961d", "name": "lean3port", - "inputRev?": "96ad256f1fa49c8584166ef85898d4c45beb0839"}}, + "inputRev?": "c73fd045fad618cb69393119bd7d11cb4cc9961d"}}, {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "bb17f9bbca775827bc6d27267b4a5539878160d1", + "rev": "759a5219eb74e3a4561f3f19b0a158d3befb2bf4", "name": "mathlib", - "inputRev?": "bb17f9bbca775827bc6d27267b4a5539878160d1"}}, + "inputRev?": "759a5219eb74e3a4561f3f19b0a158d3befb2bf4"}}, {"git": {"url": "https://github.com/gebner/quote4", "subDir?": null, diff --git a/lakefile.lean b/lakefile.lean index 14c72cded7..a29316d808 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-05-14-02" +def tag : String := "nightly-2023-05-14-04" 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"@"96ad256f1fa49c8584166ef85898d4c45beb0839" +require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"c73fd045fad618cb69393119bd7d11cb4cc9961d" @[default_target] lean_lib Mathbin where