bump to nightly-2023-07-05-07

mathlib commit leanprover-community/mathlib@5dc6092

Mathbin/Algebra/Category/Algebra/Basic.lean

@@ -30,12 +30,14 @@ universe v u
 
 variable (R : Type u) [CommRing R]
 
+#print AlgebraCat /-
 /-- The category of R-algebras and their morphisms. -/
 structure AlgebraCat where
   carrier : Type v
   [isRing : Ring carrier]
   [isAlgebra : Algebra R carrier]
 #align Algebra AlgebraCat
+-/
 
 attribute [instance] AlgebraCat.isRing AlgebraCat.isAlgebra
 
@@ -57,46 +59,59 @@ instance : ConcreteCategory.{v} (AlgebraCat.{v} R)
       map := fun R S f => (f : R → S) }
   forget_faithful := { }
 
+#print AlgebraCat.hasForgetToRing /-
 instance hasForgetToRing : HasForget₂ (AlgebraCat.{v} R) RingCat.{v}
     where forget₂ :=
     { obj := fun A => RingCat.of A
       map := fun A₁ A₂ f => AlgHom.toRingHom f }
 #align Algebra.has_forget_to_Ring AlgebraCat.hasForgetToRing
+-/
 
+#print AlgebraCat.hasForgetToModule /-
 instance hasForgetToModule : HasForget₂ (AlgebraCat.{v} R) (ModuleCat.{v} R)
     where forget₂ :=
     { obj := fun M => ModuleCat.of R M
       map := fun M₁ M₂ f => AlgHom.toLinearMap f }
 #align Algebra.has_forget_to_Module AlgebraCat.hasForgetToModule
+-/
 
+#print AlgebraCat.of /-
 /-- The object in the category of R-algebras associated to a type equipped with the appropriate
 typeclasses. -/
 def of (X : Type v) [Ring X] [Algebra R X] : AlgebraCat.{v} R :=
   ⟨X⟩
 #align Algebra.of AlgebraCat.of
+-/
 
+#print AlgebraCat.ofHom /-
 /-- Typecheck a `alg_hom` as a morphism in `Algebra R`. -/
 def ofHom {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Algebra R X] [Ring Y] [Algebra R Y]
     (f : X →ₐ[R] Y) : of R X ⟶ of R Y :=
   f
 #align Algebra.of_hom AlgebraCat.ofHom
+-/
 
+#print AlgebraCat.ofHom_apply /-
 @[simp]
 theorem ofHom_apply {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Algebra R X] [Ring Y]
     [Algebra R Y] (f : X →ₐ[R] Y) (x : X) : ofHom f x = f x :=
   rfl
 #align Algebra.of_hom_apply AlgebraCat.ofHom_apply
+-/
 
 instance : Inhabited (AlgebraCat R) :=
   ⟨of R R⟩
 
+#print AlgebraCat.coe_of /-
 @[simp]
 theorem coe_of (X : Type u) [Ring X] [Algebra R X] : (of R X : Type u) = X :=
   rfl
 #align Algebra.coe_of AlgebraCat.coe_of
+-/
 
 variable {R}
 
+#print AlgebraCat.ofSelfIso /-
 /-- Forgetting to the underlying type and then building the bundled object returns the original
 algebra. -/
 @[simps]
@@ -105,21 +120,27 @@ def ofSelfIso (M : AlgebraCat.{v} R) : AlgebraCat.of R M ≅ M
   hom := 𝟙 M
   inv := 𝟙 M
 #align Algebra.of_self_iso AlgebraCat.ofSelfIso
+-/
 
 variable {R} {M N U : ModuleCat.{v} R}
 
+#print AlgebraCat.id_apply /-
 @[simp]
 theorem id_apply (m : M) : (𝟙 M : M → M) m = m :=
   rfl
 #align Algebra.id_apply AlgebraCat.id_apply
+-/
 
+#print AlgebraCat.coe_comp /-
 @[simp]
 theorem coe_comp (f : M ⟶ N) (g : N ⟶ U) : (f ≫ g : M → U) = g ∘ f :=
   rfl
 #align Algebra.coe_comp AlgebraCat.coe_comp
+-/
 
 variable (R)
 
+#print AlgebraCat.free /-
 /-- The "free algebra" functor, sending a type `S` to the free algebra on `S`. -/
 @[simps]
 def free : Type u ⥤ AlgebraCat.{u} R
@@ -135,7 +156,9 @@ def free : Type u ⥤ AlgebraCat.{u} R
     simp only [FreeAlgebra.lift_ι_apply, CategoryTheory.coe_comp, Function.comp_apply,
       types_comp_apply]
 #align Algebra.free AlgebraCat.free
+-/
 
+#print AlgebraCat.adj /-
 /-- The free/forget adjunction for `R`-algebras. -/
 def adj : free.{u} R ⊣ forget (AlgebraCat.{u} R) :=
   Adjunction.mkOfHomEquiv
@@ -150,6 +173,7 @@ def adj : free.{u} R ⊣ forget (AlgebraCat.{u} R) :=
         simp only [forget_map_eq_coe, CategoryTheory.coe_comp, Function.comp_apply,
           FreeAlgebra.lift_symm_apply, types_comp_apply] }
 #align Algebra.adj AlgebraCat.adj
+-/
 
 instance : IsRightAdjoint (forget (AlgebraCat.{u} R)) :=
   ⟨_, adj R⟩
@@ -160,6 +184,7 @@ variable {R}
 
 variable {X₁ X₂ : Type u}
 
+#print AlgEquiv.toAlgebraIso /-
 /-- Build an isomorphism in the category `Algebra R` from a `alg_equiv` between `algebra`s. -/
 @[simps]
 def AlgEquiv.toAlgebraIso {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra R X₁} {m₂ : Algebra R X₂}
@@ -170,9 +195,11 @@ def AlgEquiv.toAlgebraIso {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra
   hom_inv_id' := by ext; exact e.left_inv x
   inv_hom_id' := by ext; exact e.right_inv x
 #align alg_equiv.to_Algebra_iso AlgEquiv.toAlgebraIso
+-/
 
 namespace CategoryTheory.Iso
 
+#print CategoryTheory.Iso.toAlgEquiv /-
 /-- Build a `alg_equiv` from an isomorphism in the category `Algebra R`. -/
 @[simps]
 def toAlgEquiv {X Y : AlgebraCat R} (i : X ≅ Y) : X ≃ₐ[R] Y
@@ -185,9 +212,11 @@ def toAlgEquiv {X Y : AlgebraCat R} (i : X ≅ Y) : X ≃ₐ[R] Y
   map_mul' := by tidy
   commutes' := by tidy
 #align category_theory.iso.to_alg_equiv CategoryTheory.Iso.toAlgEquiv
+-/
 
 end CategoryTheory.Iso
 
+#print algEquivIsoAlgebraIso /-
 /-- Algebra equivalences between `algebras`s are the same as (isomorphic to) isomorphisms in
 `Algebra`. -/
 @[simps]
@@ -197,15 +226,18 @@ def algEquivIsoAlgebraIso {X Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebr
   hom e := e.toAlgebraIso
   inv i := i.toAlgEquiv
 #align alg_equiv_iso_Algebra_iso algEquivIsoAlgebraIso
+-/
 
 instance (X : Type u) [Ring X] [Algebra R X] : Coe (Subalgebra R X) (AlgebraCat R) :=
   ⟨fun N => AlgebraCat.of R N⟩
 
+#print AlgebraCat.forget_reflects_isos /-
 instance AlgebraCat.forget_reflects_isos : ReflectsIsomorphisms (forget (AlgebraCat.{u} R))
     where reflects X Y f _ := by
     skip
     let i := as_iso ((forget (AlgebraCat.{u} R)).map f)
     let e : X ≃ₐ[R] Y := { f, i.to_equiv with }
     exact ⟨(is_iso.of_iso e.to_Algebra_iso).1⟩
 #align Algebra.forget_reflects_isos AlgebraCat.forget_reflects_isos
+-/
 

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "bd737a2a91ed4c0cf98b841ee7eae56914387979",
+    "rev": "a83d1a64832b4472aba91a339effa5987bfb0c4d",
     "name": "lean3port",
-    "inputRev?": "bd737a2a91ed4c0cf98b841ee7eae56914387979"}},
+    "inputRev?": "a83d1a64832b4472aba91a339effa5987bfb0c4d"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "24d17585e764e2fe4c70e5e0ba1b7a06473767e7",
+    "rev": "d6a451659641c1fe41fd38aa0a281af9d1ccfb5d",
     "name": "mathlib",
-    "inputRev?": "24d17585e764e2fe4c70e5e0ba1b7a06473767e7"}},
+    "inputRev?": "d6a451659641c1fe41fd38aa0a281af9d1ccfb5d"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

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-07-05-05"
+def tag : String := "nightly-2023-07-05-07"
 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"@"bd737a2a91ed4c0cf98b841ee7eae56914387979"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"a83d1a64832b4472aba91a339effa5987bfb0c4d"
 
 @[default_target]
 lean_lib Mathbin where