bump to nightly-2023-06-08-05

mathlib commit leanprover-community/mathlib@31c24aa

Mathbin/Algebra/Lie/Quotient.lean

@@ -86,37 +86,48 @@ theorem is_quotient_mk (m : M) : Quotient.mk'' m = (mk m : M ⧸ N) :=
   rfl
 #align lie_submodule.quotient.is_quotient_mk LieSubmodule.Quotient.is_quotient_mk
 
+#print LieSubmodule.Quotient.lieSubmoduleInvariant /-
 /-- Given a Lie module `M` over a Lie algebra `L`, together with a Lie submodule `N ⊆ M`, there
 is a natural linear map from `L` to the endomorphisms of `M` leaving `N` invariant. -/
 def lieSubmoduleInvariant : L →ₗ[R] Submodule.compatibleMaps N.toSubmodule N.toSubmodule :=
   LinearMap.codRestrict _ (LieModule.toEndomorphism R L M) fun _ _ => N.lie_mem
 #align lie_submodule.quotient.lie_submodule_invariant LieSubmodule.Quotient.lieSubmoduleInvariant
+-/
 
 variable (N)
 
+#print LieSubmodule.Quotient.actionAsEndoMap /-
 /-- Given a Lie module `M` over a Lie algebra `L`, together with a Lie submodule `N ⊆ M`, there
 is a natural Lie algebra morphism from `L` to the linear endomorphism of the quotient `M/N`. -/
 def actionAsEndoMap : L →ₗ⁅R⁆ Module.End R (M ⧸ N) :=
   { LinearMap.comp (Submodule.mapQLinear (N : Submodule R M) ↑N) lieSubmoduleInvariant with
     map_lie' := fun x y =>
       Submodule.linearMap_qext _ <| LinearMap.ext fun m => congr_arg mk <| lie_lie _ _ _ }
 #align lie_submodule.quotient.action_as_endo_map LieSubmodule.Quotient.actionAsEndoMap
+-/
 
+#print LieSubmodule.Quotient.actionAsEndoMapBracket /-
 /-- Given a Lie module `M` over a Lie algebra `L`, together with a Lie submodule `N ⊆ M`, there is
 a natural bracket action of `L` on the quotient `M/N`. -/
 instance actionAsEndoMapBracket : Bracket L (M ⧸ N) :=
   ⟨fun x n => actionAsEndoMap N x n⟩
 #align lie_submodule.quotient.action_as_endo_map_bracket LieSubmodule.Quotient.actionAsEndoMapBracket
+-/
 
+#print LieSubmodule.Quotient.lieQuotientLieRingModule /-
 instance lieQuotientLieRingModule : LieRingModule L (M ⧸ N) :=
   { LieRingModule.compLieHom _ (actionAsEndoMap N) with bracket := Bracket.bracket }
 #align lie_submodule.quotient.lie_quotient_lie_ring_module LieSubmodule.Quotient.lieQuotientLieRingModule
+-/
 
+#print LieSubmodule.Quotient.lieQuotientLieModule /-
 /-- The quotient of a Lie module by a Lie submodule, is a Lie module. -/
 instance lieQuotientLieModule : LieModule R L (M ⧸ N) :=
   LieModule.compLieHom _ (actionAsEndoMap N)
 #align lie_submodule.quotient.lie_quotient_lie_module LieSubmodule.Quotient.lieQuotientLieModule
+-/
 
+#print LieSubmodule.Quotient.lieQuotientHasBracket /-
 instance lieQuotientHasBracket : Bracket (L ⧸ I) (L ⧸ I) :=
   ⟨by
     intro x y
@@ -131,12 +142,16 @@ instance lieQuotientHasBracket : Bracket (L ⧸ I) (L ⧸ I) :=
     · apply lie_mem_right R L I x₁ (x₂ - y₂) h₂
     · apply lie_mem_left R L I (x₁ - y₁) y₂ h₁⟩
 #align lie_submodule.quotient.lie_quotient_has_bracket LieSubmodule.Quotient.lieQuotientHasBracket
+-/
 
+#print LieSubmodule.Quotient.mk_bracket /-
 @[simp]
 theorem mk_bracket (x y : L) : mk ⁅x, y⁆ = ⁅(mk x : L ⧸ I), (mk y : L ⧸ I)⁆ :=
   rfl
 #align lie_submodule.quotient.mk_bracket LieSubmodule.Quotient.mk_bracket
+-/
 
+#print LieSubmodule.Quotient.lieQuotientLieRing /-
 instance lieQuotientLieRing : LieRing (L ⧸ I)
     where
   add_lie := by
@@ -168,7 +183,9 @@ instance lieQuotientLieRing : LieRing (L ⧸ I)
       | rw [← Submodule.Quotient.mk_add]
     apply congr_arg; apply leibniz_lie
 #align lie_submodule.quotient.lie_quotient_lie_ring LieSubmodule.Quotient.lieQuotientLieRing
+-/
 
+#print LieSubmodule.Quotient.lieQuotientLieAlgebra /-
 instance lieQuotientLieAlgebra : LieAlgebra R (L ⧸ I)
     where lie_smul := by
     intro t x' y'; apply Quotient.inductionOn₂' x' y'; intro x y
@@ -179,29 +196,39 @@ instance lieQuotientLieAlgebra : LieAlgebra R (L ⧸ I)
       | rw [← Submodule.Quotient.mk_smul]
     apply congr_arg; apply lie_smul
 #align lie_submodule.quotient.lie_quotient_lie_algebra LieSubmodule.Quotient.lieQuotientLieAlgebra
+-/
 
+#print LieSubmodule.Quotient.mk' /-
 /-- `lie_submodule.quotient.mk` as a `lie_module_hom`. -/
 @[simps]
 def mk' : M →ₗ⁅R,L⁆ M ⧸ N :=
   { N.toSubmodule.mkQ with
     toFun := mk
     map_lie' := fun r m => rfl }
 #align lie_submodule.quotient.mk' LieSubmodule.Quotient.mk'
+-/
 
+#print LieSubmodule.Quotient.mk_eq_zero /-
 @[simp]
 theorem mk_eq_zero {m : M} : mk' N m = 0 ↔ m ∈ N :=
   Submodule.Quotient.mk_eq_zero N.toSubmodule
 #align lie_submodule.quotient.mk_eq_zero LieSubmodule.Quotient.mk_eq_zero
+-/
 
+#print LieSubmodule.Quotient.mk'_ker /-
 @[simp]
 theorem mk'_ker : (mk' N).ker = N := by ext; simp
 #align lie_submodule.quotient.mk'_ker LieSubmodule.Quotient.mk'_ker
+-/
 
+#print LieSubmodule.Quotient.map_mk'_eq_bot_le /-
 @[simp]
 theorem map_mk'_eq_bot_le : map (mk' N) N' = ⊥ ↔ N' ≤ N := by
   rw [← LieModuleHom.le_ker_iff_map, mk'_ker]
 #align lie_submodule.quotient.map_mk'_eq_bot_le LieSubmodule.Quotient.map_mk'_eq_bot_le
+-/
 
+#print LieSubmodule.Quotient.lieModuleHom_ext /-
 /-- Two `lie_module_hom`s from a quotient lie module are equal if their compositions with
 `lie_submodule.quotient.mk'` are equal.
 
@@ -210,6 +237,7 @@ See note [partially-applied ext lemmas]. -/
 theorem lieModuleHom_ext ⦃f g : M ⧸ N →ₗ⁅R,L⁆ M⦄ (h : f.comp (mk' N) = g.comp (mk' N)) : f = g :=
   LieModuleHom.ext fun x => Quotient.inductionOn' x <| LieModuleHom.congr_fun h
 #align lie_submodule.quotient.lie_module_hom_ext LieSubmodule.Quotient.lieModuleHom_ext
+-/
 
 end Quotient
 
@@ -223,6 +251,7 @@ variable [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'
 
 variable (f : L →ₗ⁅R⁆ L')
 
+#print LieHom.quotKerEquivRange /-
 /-- The first isomorphism theorem for morphisms of Lie algebras. -/
 @[simps]
 noncomputable def quotKerEquivRange : (L ⧸ f.ker) ≃ₗ⁅R⁆ f.range :=
@@ -236,6 +265,7 @@ noncomputable def quotKerEquivRange : (L ⧸ f.ker) ≃ₗ⁅R⁆ f.range :=
       simp only [Submodule.Quotient.quot_mk_eq_mk, LinearMap.quotKerEquivRange_apply_mk, ←
         LieSubmodule.Quotient.mk_bracket, coe_to_linear_map, map_lie] }
 #align lie_hom.quot_ker_equiv_range LieHom.quotKerEquivRange
+-/
 
 end LieHom
 

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "4fb86430a7a0340b164edbe579d314b194f5691d",
+    "rev": "d4480b1aa230560cb7265e8cdec83c8f78a8af05",
     "name": "lean3port",
-    "inputRev?": "4fb86430a7a0340b164edbe579d314b194f5691d"}},
+    "inputRev?": "d4480b1aa230560cb7265e8cdec83c8f78a8af05"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "af771c7fc6ae9e53f72bdff452f6bb91716ef5a4",
+    "rev": "4a575544e498a7a3b649b51a710343cd5763048e",
     "name": "mathlib",
-    "inputRev?": "af771c7fc6ae9e53f72bdff452f6bb91716ef5a4"}},
+    "inputRev?": "4a575544e498a7a3b649b51a710343cd5763048e"}},
   {"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-06-08-03"
+def tag : String := "nightly-2023-06-08-05"
 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"@"4fb86430a7a0340b164edbe579d314b194f5691d"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"d4480b1aa230560cb7265e8cdec83c8f78a8af05"
 
 @[default_target]
 lean_lib Mathbin where