From 33b6e72c5329859757be84139c1158ae610894ae Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sat, 30 Mar 2024 06:09:13 +0900
Subject: [PATCH] =?UTF-8?q?FunLike=20=E3=81=AE=E4=BB=95=E6=A7=98=E5=A4=89?=
 =?UTF-8?q?=E6=9B=B4=E3=81=AB=E4=BC=B4=E3=81=86=E3=82=A8=E3=83=A9=E3=83=BC?=
 =?UTF-8?q?=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