bump to nightly-2023-07-07-09

mathlib commit leanprover-community/mathlib@8905e5e

Mathbin/Algebra/Category/Algebra/Limits.lean

@@ -35,14 +35,19 @@ variable {R : Type u} [CommRing R]
 
 variable {J : Type v} [SmallCategory J]
 
+#print AlgebraCat.semiringObj /-
 instance semiringObj (F : J ⥤ AlgebraCat.{max v w} R) (j) :
     Semiring ((F ⋙ forget (AlgebraCat R)).obj j) := by change Semiring (F.obj j); infer_instance
 #align Algebra.semiring_obj AlgebraCat.semiringObj
+-/
 
+#print AlgebraCat.algebraObj /-
 instance algebraObj (F : J ⥤ AlgebraCat.{max v w} R) (j) :
     Algebra R ((F ⋙ forget (AlgebraCat R)).obj j) := by change Algebra R (F.obj j); infer_instance
 #align Algebra.algebra_obj AlgebraCat.algebraObj
+-/
 
+#print AlgebraCat.sectionsSubalgebra /-
 /-- The flat sections of a functor into `Algebra R` form a submodule of all sections.
 -/
 def sectionsSubalgebra (F : J ⥤ AlgebraCat.{max v w} R) : Subalgebra R (∀ j, F.obj j) :=
@@ -51,14 +56,18 @@ def sectionsSubalgebra (F : J ⥤ AlgebraCat.{max v w} R) : Subalgebra R (∀ j,
       (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
+-/
 
+#print AlgebraCat.limitSemiring /-
 instance limitSemiring (F : J ⥤ AlgebraCat.{max v w} R) :
     Ring (Types.limitCone (F ⋙ forget (AlgebraCat.{max v w} R))).pt :=
   by
   change Ring (sections_subalgebra F)
   infer_instance
 #align Algebra.limit_semiring AlgebraCat.limitSemiring
+-/
 
+#print AlgebraCat.limitAlgebra /-
 instance limitAlgebra (F : J ⥤ AlgebraCat.{max v w} R) :
     Algebra R (Types.limitCone (F ⋙ forget (AlgebraCat.{max v w} R))).pt :=
   by
@@ -69,7 +78,9 @@ instance limitAlgebra (F : J ⥤ AlgebraCat.{max v w} R) :
   rw [this]
   infer_instance
 #align Algebra.limit_algebra AlgebraCat.limitAlgebra
+-/
 
+#print AlgebraCat.limitπAlgHom /-
 /-- `limit.π (F ⋙ forget (Algebra R)) j` as a `alg_hom`. -/
 def limitπAlgHom (F : J ⥤ AlgebraCat.{max v w} R) (j) :
     (Types.limitCone (F ⋙ forget (AlgebraCat R))).pt →ₐ[R]
@@ -79,9 +90,11 @@ def limitπAlgHom (F : J ⥤ AlgebraCat.{max v w} R) (j) :
       (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
+-/
 
 namespace HasLimits
 
+#print AlgebraCat.HasLimits.limitCone /-
 -- The next two definitions are used in the construction of `has_limits (Algebra R)`.
 -- After that, the limits should be constructed using the generic limits API,
 -- e.g. `limit F`, `limit.cone F`, and `limit.is_limit F`.
@@ -96,7 +109,9 @@ def limitCone (F : J ⥤ AlgebraCat.{max v w} R) : Cone F
       naturality' := fun j j' f =>
         AlgHom.coe_fn_injective ((Types.limitCone (F ⋙ forget _)).π.naturality f) }
 #align Algebra.has_limits.limit_cone AlgebraCat.HasLimits.limitCone
+-/
 
+#print AlgebraCat.HasLimits.limitConeIsLimit /-
 /-- Witness that the limit cone in `Algebra R` is a limit cone.
 (Internal use only; use the limits API.)
 -/
@@ -111,12 +126,14 @@ def limitConeIsLimit (F : J ⥤ AlgebraCat.{max v w} R) : IsLimit (limitCone F)
   · intro x y; simp only [forget_map_eq_coe, AlgHom.map_add, functor.map_cone_π_app]; rfl
   · intro r; ext j; exact (s.π.app j).commutes r
 #align Algebra.has_limits.limit_cone_is_limit AlgebraCat.HasLimits.limitConeIsLimit
+-/
 
 end HasLimits
 
 open HasLimits
 
 /- ./././Mathport/Syntax/Translate/Command.lean:322:38: unsupported irreducible non-definition -/
+#print AlgebraCat.hasLimitsOfSize /-
 /-- The category of R-algebras has all limits. -/
 irreducible_def hasLimitsOfSize : HasLimitsOfSize.{v, v} (AlgebraCat.{max v w} R) :=
   {
@@ -127,11 +144,15 @@ irreducible_def hasLimitsOfSize : HasLimitsOfSize.{v, v} (AlgebraCat.{max v w} R
             { Cone := limit_cone F
               IsLimit := limit_cone_is_limit F } } }
 #align Algebra.has_limits_of_size AlgebraCat.hasLimitsOfSize
+-/
 
+#print AlgebraCat.hasLimits /-
 instance hasLimits : HasLimits (AlgebraCat.{w} R) :=
   AlgebraCat.hasLimitsOfSize.{w, w, u}
 #align Algebra.has_limits AlgebraCat.hasLimits
+-/
 
+#print AlgebraCat.forget₂RingPreservesLimitsOfSize /-
 /-- The forgetful functor from R-algebras to rings preserves all limits.
 -/
 instance forget₂RingPreservesLimitsOfSize :
@@ -142,11 +163,15 @@ instance forget₂RingPreservesLimitsOfSize :
         preserves_limit_of_preserves_limit_cone (limit_cone_is_limit F)
           (by apply RingCat.limitConeIsLimit (F ⋙ forget₂ (AlgebraCat R) RingCat.{max v w})) }
 #align Algebra.forget₂_Ring_preserves_limits_of_size AlgebraCat.forget₂RingPreservesLimitsOfSize
+-/
 
+#print AlgebraCat.forget₂RingPreservesLimits /-
 instance forget₂RingPreservesLimits : PreservesLimits (forget₂ (AlgebraCat R) RingCat.{w}) :=
   AlgebraCat.forget₂RingPreservesLimitsOfSize.{w, w}
 #align Algebra.forget₂_Ring_preserves_limits AlgebraCat.forget₂RingPreservesLimits
+-/
 
+#print AlgebraCat.forget₂ModulePreservesLimitsOfSize /-
 /-- The forgetful functor from R-algebras to R-modules preserves all limits.
 -/
 instance forget₂ModulePreservesLimitsOfSize :
@@ -160,12 +185,16 @@ instance forget₂ModulePreservesLimitsOfSize :
               ModuleCat.HasLimits.limitConeIsLimit
                 (F ⋙ forget₂ (AlgebraCat R) (ModuleCat.{max v w} R))) }
 #align Algebra.forget₂_Module_preserves_limits_of_size AlgebraCat.forget₂ModulePreservesLimitsOfSize
+-/
 
+#print AlgebraCat.forget₂ModulePreservesLimits /-
 instance forget₂ModulePreservesLimits :
     PreservesLimits (forget₂ (AlgebraCat R) (ModuleCat.{w} R)) :=
   AlgebraCat.forget₂ModulePreservesLimitsOfSize.{w, w}
 #align Algebra.forget₂_Module_preserves_limits AlgebraCat.forget₂ModulePreservesLimits
+-/
 
+#print AlgebraCat.forgetPreservesLimitsOfSize /-
 /-- The forgetful functor from R-algebras to types preserves all limits.
 -/
 instance forgetPreservesLimitsOfSize :
@@ -176,10 +205,13 @@ instance forgetPreservesLimitsOfSize :
         preserves_limit_of_preserves_limit_cone (limit_cone_is_limit F)
           (types.limit_cone_is_limit (F ⋙ forget _)) }
 #align Algebra.forget_preserves_limits_of_size AlgebraCat.forgetPreservesLimitsOfSize
+-/
 
+#print AlgebraCat.forgetPreservesLimits /-
 instance forgetPreservesLimits : PreservesLimits (forget (AlgebraCat.{w} R)) :=
   AlgebraCat.forgetPreservesLimitsOfSize.{w, w}
 #align Algebra.forget_preserves_limits AlgebraCat.forgetPreservesLimits
+-/
 
 end AlgebraCat