From f3069f365a331fc1e4e18599be9b9e48032040eb Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 30 Mar 2024 05:31:37 +0900 Subject: [PATCH 1/3] update Lean version to v4.6.0 --- lake-manifest.json | 31 ++++++++++++++++++++----------- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 22 insertions(+), 13 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index d8ca4a8..bc9e5f6 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,28 +1,28 @@ {"version": 7, "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/Seasawher/mk-exercise", + [{"url": "https://github.com/Seasawher/mk-exercise.git", "type": "git", "subDir": null, "rev": "70102f2963f5bc19aac0339d9464b72a1de2e1cb", "name": "«mk-exercise»", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "70102f2963f5bc19aac0339d9464b72a1de2e1cb", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "0f6bc5b32bf5b0498902d3b5f0806c75530539d5", + "rev": "a7543d1a6934d52086971f510e482d743fe30cf3", "name": "std", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.6.0", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "1c88406514a636d241903e2e288d21dc6d861e01", + "rev": "fd760831487e6835944e7eeed505522c9dd47563", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -31,19 +31,19 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a", + "rev": "c51fa8ea4de8b203f64929cba19d139e555f9f6b", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.6.0", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35", + "rev": "16cae05860b208925f54e5581ec5fd264823440c", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.25", + "inputRev": "v0.0.29", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -55,13 +55,22 @@ "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/import-graph.git", + "type": "git", + "subDir": null, + "rev": "64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "afe6b29fd5ae8baf11db1d2c2921b9730d9f7ad0", + "rev": "7ca43cbd6aa34058a1afad8e47190af3ec1f9bdb", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "afe6b29fd5ae8baf11db1d2c2921b9730d9f7ad0", + "inputRev": "7ca43cbd6aa34058a1afad8e47190af3ec1f9bdb", "inherited": false, "configFile": "lakefile.lean"}], "name": "«lean-math-workshop»", diff --git a/lakefile.lean b/lakefile.lean index 4011b70..ec2c7c5 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -14,7 +14,7 @@ require «mk-exercise» from git "https://github.com/Seasawher/mk-exercise.git" @ "70102f2963f5bc19aac0339d9464b72a1de2e1cb" require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" @ "afe6b29fd5ae8baf11db1d2c2921b9730d9f7ad0" + "https://github.com/leanprover-community/mathlib4.git" @ "7ca43cbd6aa34058a1afad8e47190af3ec1f9bdb" @[default_target] lean_lib «Solution» where diff --git a/lean-toolchain b/lean-toolchain index 3f21e50..5026204 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.5.0-rc1 +leanprover/lean4:v4.6.0 From 33b6e72c5329859757be84139c1158ae610894ae Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 30 Mar 2024 06:09:13 +0900 Subject: [PATCH 2/3] =?UTF-8?q?FunLike=20=E3=81=AE=E4=BB=95=E6=A7=98?= =?UTF-8?q?=E5=A4=89=E6=9B=B4=E3=81=AB=E4=BC=B4=E3=81=86=E3=82=A8=E3=83=A9?= =?UTF-8?q?=E3=83=BC=E3=82=92=E8=A7=A3=E6=B6=88=E3=81=99=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Solution/Advanced/Algebra/Lecture2.lean | 2 +- Solution/Advanced/Algebra/Lecture3.lean | 4 ++-- Solution/Advanced/Category/Lecture1.lean | 8 ++++++++ 3 files changed, 11 insertions(+), 3 deletions(-) diff --git a/Solution/Advanced/Algebra/Lecture2.lean b/Solution/Advanced/Algebra/Lecture2.lean index 4ce65f1..22be2fa 100644 --- a/Solution/Advanced/Algebra/Lecture2.lean +++ b/Solution/Advanced/Algebra/Lecture2.lean @@ -31,7 +31,7 @@ variable [Group G₁] [Group G₂] {f : G₁ →* G₂} -- `f`と`a : G₁`に対して、いちいち`f.toFun a`と書く代わりに、`f a`と書くためのおまじない -- （`f`そのものは、写像`f.toFun`と、それが積を保つという事実`f.map_mul'`を束ねたもので、本来は写像でない） -- 右側のInfoviewには、`f a`の代わりに`↑f a`と表示されることもあるが、同じなので気にしないでください。 -instance : FunLike (G₁ →* G₂) G₁ (fun _ ↦ G₂) where +instance : DFunLike (G₁ →* G₂) G₁ (fun _ ↦ G₂) where coe := fun f ↦ f.toFun coe_injective' f₁ f₂ _ := by cases f₁; cases f₂; congr diff --git a/Solution/Advanced/Algebra/Lecture3.lean b/Solution/Advanced/Algebra/Lecture3.lean index 7f91fb6..2c5cc73 100644 --- a/Solution/Advanced/Algebra/Lecture3.lean +++ b/Solution/Advanced/Algebra/Lecture3.lean @@ -148,7 +148,7 @@ notation:25 X " →[" G:25 "] " Y:0 => GroupActionHom G X Y variable [Group G] [GroupAction G X] [GroupAction G Y] [GroupAction G Z] -- `f : X →[G] Y`に対して`f x`のように書くためのおまじない。 -instance : FunLike (GroupActionHom G X Y) X (fun _ ↦ Y) where +instance : DFunLike (GroupActionHom G X Y) X (fun _ ↦ Y) where coe f := f.toFun coe_injective' f₁ f₂ _ := by cases f₁; cases f₂; congr @@ -161,7 +161,7 @@ theorem GroupActionHom.coe_coe (f : X → Y) (h) : ((⟨f, h⟩ : X →[G] Y) : -- 定義からすぐ分かること @[ext] theorem GroupActionHom.ext {f₁ f₂ : X →[G] Y} : (∀ x, f₁ x = f₂ x) → f₁ = f₂ := - FunLike.ext f₁ f₂ + DFunLike.ext f₁ f₂ theorem map_smul (f : X →[G] Y) : ∀ (a : G) (x : X), f (a • x) = a • f x := f.map_smul' diff --git a/Solution/Advanced/Category/Lecture1.lean b/Solution/Advanced/Category/Lecture1.lean index abeb828..9a494bc 100644 --- a/Solution/Advanced/Category/Lecture1.lean +++ b/Solution/Advanced/Category/Lecture1.lean @@ -174,6 +174,14 @@ instance {R : CommRingCat} : Category (CommAlgCat R) where /- 定義の上の`@[simps]`はおまじないで、ここでは特に意味がない。`Lecture 2`で役に立つ。 -/ +-- おまじない +instance {A B : CommAlgCat R} : FunLike (Hom A B) A B where + coe f := f.toFun + coe_injective' f g h := by + rcases f with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩ + rcases g with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩ + congr + -- おまじない。`Lecture 2`で役に立つ。 instance {A B : CommAlgCat R} : AlgHomClass (Hom A B) R A B := inferInstanceAs <| AlgHomClass (A →ₐ[R] B) R A B From b4fa1e4f2c7a9cef584737bf7d407d3b0f817681 Mon Sep 17 00:00:00 2001 From: Kitamado <47292598+Seasawher@users.noreply.github.com> Date: Sat, 6 Apr 2024 12:13:39 +0900 Subject: [PATCH 3/3] Update Solution/Advanced/Category/Lecture1.lean Co-authored-by: Yuma Mizuno --- Solution/Advanced/Category/Lecture1.lean | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/Solution/Advanced/Category/Lecture1.lean b/Solution/Advanced/Category/Lecture1.lean index 9a494bc..85f5671 100644 --- a/Solution/Advanced/Category/Lecture1.lean +++ b/Solution/Advanced/Category/Lecture1.lean @@ -174,15 +174,9 @@ instance {R : CommRingCat} : Category (CommAlgCat R) where /- 定義の上の`@[simps]`はおまじないで、ここでは特に意味がない。`Lecture 2`で役に立つ。 -/ --- おまじない -instance {A B : CommAlgCat R} : FunLike (Hom A B) A B where - coe f := f.toFun - coe_injective' f g h := by - rcases f with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩ - rcases g with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩ - congr - -- おまじない。`Lecture 2`で役に立つ。 +instance {A B : CommAlgCat R} : FunLike (Hom A B) A B := + inferInstanceAs <| FunLike (A →ₐ[R] B) A B instance {A B : CommAlgCat R} : AlgHomClass (Hom A B) R A B := inferInstanceAs <| AlgHomClass (A →ₐ[R] B) R A B