Skip to content

Commit c03f676

Browse files
YaelDilliesYaelDillies
committed
chore: get rid of generic hom coercions
1 parent efeadfb commit c03f676

File tree

10 files changed

+483
-126
lines changed

10 files changed

+483
-126
lines changed

‎Mathlib/Algebra/Group/Equiv/Basic.lean‎

Lines changed: 354 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,15 +29,296 @@ end EmbeddingLike
2929

3030
variable [EquivLike F α β]
3131

32+
/-- Turn an element of a type `F` satisfying `MulEquivClass F α β` into an actual
33+
`MulEquiv`. This is declared as the default coercion from `F` to `α ≃* β`. -/
34+
@[to_additive (attr := simps!)
35+
"Turn an element of a type `F` satisfying `AddEquivClass F α β` into an actual
36+
`AddEquiv`. This is declared as the default coercion from `F` to `α ≃+ β`."]
37+
def MulEquiv.ofClass [Mul α] [Mul β] [MulEquivClass F α β] (f : F) : α ≃* β where
38+
__ : α ≃ β := .ofClass f
39+
__ : α →ₙ* β := .ofClass f
40+
3241
@[to_additive]
33-
theorem MulEquivClass.toMulEquiv_injective [Mul α] [Mul β] [MulEquivClass F α β] :
34-
Function.Injective ((↑) : F → α ≃* β) :=
42+
theorem MulEquiv.ofClass_injective [Mul α] [Mul β] [MulEquivClass F α β] :
43+
Function.Injective (.ofClass : F → α ≃* β) :=
3544
fun _ _ e ↦ DFunLike.ext _ _ fun a ↦ congr_arg (fun e : α ≃* β ↦ e.toFun a) e
3645

3746
namespace MulEquiv
3847
section Mul
3948
variable [Mul M] [Mul N] [Mul P]
4049

50+
section coe
51+
52+
@[to_additive]
53+
instance : EquivLike (M ≃* N) M N where
54+
coe f := f.toFun
55+
inv f := f.invFun
56+
left_inv f := f.left_inv
57+
right_inv f := f.right_inv
58+
coe_injective' f g h₁ h₂ := by
59+
cases f
60+
cases g
61+
congr
62+
apply Equiv.coe_fn_injective h₁
63+
64+
@[to_additive] -- shortcut instance that doesn't generate any subgoals
65+
instance : FunLike (M ≃* N) M N := inferInstance
66+
67+
@[to_additive]
68+
instance : MulEquivClass (M ≃* N) M N where
69+
map_mul f := f.map_mul'
70+
71+
attribute [coe] toEquiv
72+
attribute [coe] toMulHom
73+
74+
@[to_additive] instance : Coe (M ≃* N) (M ≃ N) where coe := toEquiv
75+
@[to_additive] instance : Coe (M ≃* N) (M →ₙ* N) where coe := toMulHom
76+
77+
/-- Two multiplicative isomorphisms agree if they are defined by the
78+
same underlying function. -/
79+
@[to_additive (attr := ext)
80+
"Two additive isomorphisms agree if they are defined by the same underlying function."]
81+
theorem ext {f g : MulEquiv M N} (h : ∀ x, f x = g x) : f = g :=
82+
DFunLike.ext f g h
83+
84+
@[to_additive]
85+
protected theorem congr_arg {f : MulEquiv M N} {x x' : M} : x = x' → f x = f x' :=
86+
DFunLike.congr_arg f
87+
88+
@[to_additive]
89+
protected theorem congr_fun {f g : MulEquiv M N} (h : f = g) (x : M) : f x = g x :=
90+
DFunLike.congr_fun h x
91+
92+
@[to_additive (attr := simp)]
93+
theorem coe_mk (f : M ≃ N) (hf : ∀ x y, f (x * y) = f x * f y) : (mk f hf : M → N) = f := rfl
94+
95+
@[to_additive (attr := simp)]
96+
theorem mk_coe (e : M ≃* N) (e' h₁ h₂ h₃) : (⟨⟨e, e', h₁, h₂⟩, h₃⟩ : M ≃* N) = e :=
97+
ext fun _ => rfl
98+
99+
@[to_additive (attr := simp)]
100+
lemma toFun_eq_coe (f : M ≃* N) : f.toFun = f := rfl
101+
102+
-- Porting note: `to_fun_eq_coe` no longer needed in Lean4
103+
104+
@[to_additive (attr := simp)]
105+
theorem coe_toEquiv (f : M ≃* N) : ⇑f.toEquiv = f := rfl
106+
107+
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: `MulHom.coe_mk` simplifies `↑f.toMulHom` to `f.toMulHom.toFun`,
108+
-- not `f.toEquiv.toFun`; use higher priority as a workaround
109+
@[to_additive (attr := simp 1100)]
110+
theorem coe_toMulHom {f : M ≃* N} : ⇑f.toMulHom = f := rfl
111+
112+
/-- Makes a multiplicative isomorphism from a bijection which preserves multiplication. -/
113+
@[to_additive "Makes an additive isomorphism from a bijection which preserves addition."]
114+
def mk' (f : M ≃ N) (h : ∀ x y, f (x * y) = f x * f y) : M ≃* N := ⟨f, h⟩
115+
116+
end coe
117+
118+
section map
119+
120+
/-- A multiplicative isomorphism preserves multiplication. -/
121+
@[to_additive "An additive isomorphism preserves addition."]
122+
protected theorem map_mul (f : M ≃* N) : ∀ x y, f (x * y) = f x * f y :=
123+
map_mul f
124+
125+
attribute [deprecated map_mul (since := "2024-08-08")] MulEquiv.map_mul
126+
attribute [deprecated map_add (since := "2024-08-08")] AddEquiv.map_add
127+
128+
end map
129+
130+
section bijective
131+
132+
@[to_additive]
133+
protected theorem bijective (e : M ≃* N) : Function.Bijective e :=
134+
EquivLike.bijective e
135+
136+
@[to_additive]
137+
protected theorem injective (e : M ≃* N) : Function.Injective e :=
138+
EquivLike.injective e
139+
140+
@[to_additive]
141+
protected theorem surjective (e : M ≃* N) : Function.Surjective e :=
142+
EquivLike.surjective e
143+
144+
@[to_additive]
145+
theorem apply_eq_iff_eq (e : M ≃* N) {x y : M} : e x = e y ↔ x = y :=
146+
e.injective.eq_iff
147+
148+
end bijective
149+
150+
section refl
151+
152+
/-- The identity map is a multiplicative isomorphism. -/
153+
@[to_additive (attr := refl) "The identity map is an additive isomorphism."]
154+
def refl (M : Type*) [Mul M] : M ≃* M :=
155+
{ Equiv.refl _ with map_mul' := fun _ _ => rfl }
156+
157+
@[to_additive]
158+
instance : Inhabited (M ≃* M) := ⟨refl M⟩
159+
160+
@[to_additive (attr := simp)]
161+
theorem coe_refl : ↑(refl M) = id := rfl
162+
163+
@[to_additive (attr := simp)]
164+
theorem refl_apply (m : M) : refl M m = m := rfl
165+
166+
end refl
167+
168+
section symm
169+
170+
/-- An alias for `h.symm.map_mul`. Introduced to fix the issue in
171+
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234183.20.60simps.60.20maximum.20recursion.20depth
172+
-/
173+
@[to_additive]
174+
lemma symm_map_mul {M N : Type*} [Mul M] [Mul N] (h : M ≃* N) (x y : N) :
175+
h.symm (x * y) = h.symm x * h.symm y :=
176+
map_mul (h.toMulHom.inverse h.toEquiv.symm h.left_inv h.right_inv) x y
177+
178+
/-- The inverse of an isomorphism is an isomorphism. -/
179+
@[to_additive (attr := symm) "The inverse of an isomorphism is an isomorphism."]
180+
def symm {M N : Type*} [Mul M] [Mul N] (h : M ≃* N) : N ≃* M :=
181+
⟨h.toEquiv.symm, h.symm_map_mul⟩
182+
183+
@[to_additive] -- Porting note: no longer a `simp`, see below
184+
theorem invFun_eq_symm {f : M ≃* N} : f.invFun = f.symm := rfl
185+
-- Porting note: to_additive translated the name incorrectly in mathlib 3.
186+
187+
@[to_additive (attr := simp)]
188+
theorem coe_toEquiv_symm (f : M ≃* N) : ((f : M ≃ N).symm : N → M) = f.symm := rfl
189+
190+
@[to_additive (attr := simp)]
191+
theorem equivLike_inv_eq_symm (f : M ≃* N) : EquivLike.inv f = f.symm := rfl
192+
193+
@[to_additive (attr := simp)]
194+
theorem toEquiv_symm (f : M ≃* N) : (f.symm : N ≃ M) = (f : M ≃ N).symm := rfl
195+
196+
-- Porting note: `toEquiv_mk` no longer needed in Lean4
197+
198+
@[to_additive (attr := simp)]
199+
theorem symm_symm (f : M ≃* N) : f.symm.symm = f := rfl
200+
201+
@[to_additive]
202+
theorem symm_bijective : Function.Bijective (symm : (M ≃* N) → N ≃* M) :=
203+
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
204+
205+
@[to_additive (attr := simp)]
206+
theorem mk_coe' (e : M ≃* N) (f h₁ h₂ h₃) : (MulEquiv.mk ⟨f, e, h₁, h₂⟩ h₃ : N ≃* M) = e.symm :=
207+
symm_bijective.injective <| ext fun _ => rfl
208+
209+
@[to_additive (attr := simp)]
210+
theorem symm_mk (f : M ≃ N) (h) :
211+
(MulEquiv.mk f h).symm = ⟨f.symm, (MulEquiv.mk f h).symm_map_mul⟩ := rfl
212+
213+
@[to_additive (attr := simp)]
214+
theorem refl_symm : (refl M).symm = refl M := rfl
215+
216+
/-- `e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`. -/
217+
@[to_additive (attr := simp) "`e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`."]
218+
theorem apply_symm_apply (e : M ≃* N) (y : N) : e (e.symm y) = y :=
219+
e.toEquiv.apply_symm_apply y
220+
221+
/-- `e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`. -/
222+
@[to_additive (attr := simp) "`e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`."]
223+
theorem symm_apply_apply (e : M ≃* N) (x : M) : e.symm (e x) = x :=
224+
e.toEquiv.symm_apply_apply x
225+
226+
@[to_additive (attr := simp)]
227+
theorem symm_comp_self (e : M ≃* N) : e.symm ∘ e = id :=
228+
funext e.symm_apply_apply
229+
230+
@[to_additive (attr := simp)]
231+
theorem self_comp_symm (e : M ≃* N) : e ∘ e.symm = id :=
232+
funext e.apply_symm_apply
233+
234+
@[to_additive]
235+
theorem apply_eq_iff_symm_apply (e : M ≃* N) {x : M} {y : N} : e x = y ↔ x = e.symm y :=
236+
e.toEquiv.apply_eq_iff_eq_symm_apply
237+
238+
@[to_additive]
239+
theorem symm_apply_eq (e : M ≃* N) {x y} : e.symm x = y ↔ x = e y :=
240+
e.toEquiv.symm_apply_eq
241+
242+
@[to_additive]
243+
theorem eq_symm_apply (e : M ≃* N) {x y} : y = e.symm x ↔ e y = x :=
244+
e.toEquiv.eq_symm_apply
245+
246+
@[to_additive]
247+
theorem eq_comp_symm {α : Type*} (e : M ≃* N) (f : N → α) (g : M → α) :
248+
f = g ∘ e.symm ↔ f ∘ e = g :=
249+
e.toEquiv.eq_comp_symm f g
250+
251+
@[to_additive]
252+
theorem comp_symm_eq {α : Type*} (e : M ≃* N) (f : N → α) (g : M → α) :
253+
g ∘ e.symm = f ↔ g = f ∘ e :=
254+
e.toEquiv.comp_symm_eq f g
255+
256+
@[to_additive]
257+
theorem eq_symm_comp {α : Type*} (e : M ≃* N) (f : α → M) (g : α → N) :
258+
f = e.symm ∘ g ↔ e ∘ f = g :=
259+
e.toEquiv.eq_symm_comp f g
260+
261+
@[to_additive]
262+
theorem symm_comp_eq {α : Type*} (e : M ≃* N) (f : α → M) (g : α → N) :
263+
e.symm ∘ g = f ↔ g = e ∘ f :=
264+
e.toEquiv.symm_comp_eq f g
265+
266+
@[to_additive (attr := simp)]
267+
theorem apply_ofClass_symm_apply {α β} [Mul α] [Mul β] {F} [EquivLike F α β]
268+
[MulEquivClass F α β] (e : F) (x : β) :
269+
e ((.ofClass e : α ≃* β).symm x) = x :=
270+
(.ofClass e : α ≃* β).right_inv x
271+
272+
@[to_additive (attr := simp)]
273+
theorem ofClass_symm_apply_apply {α β} [Mul α] [Mul β] {F} [EquivLike F α β]
274+
[MulEquivClass F α β] (e : F) (x : α) :
275+
(.ofClass e : α ≃* β).symm (e x) = x :=
276+
(.ofClass e : α ≃* β).left_inv x
277+
278+
end symm
279+
280+
section simps
281+
282+
/-- See Note [custom simps projection] -/
283+
@[to_additive "See Note [custom simps projection]"] -- this comment fixes the syntax highlighting "
284+
def Simps.symm_apply (e : M ≃* N) : N → M :=
285+
e.symm
286+
287+
initialize_simps_projections AddEquiv (toFun → apply, invFun → symm_apply)
288+
289+
initialize_simps_projections MulEquiv (toFun → apply, invFun → symm_apply)
290+
291+
end simps
292+
293+
section trans
294+
295+
/-- Transitivity of multiplication-preserving isomorphisms -/
296+
@[to_additive (attr := trans) "Transitivity of addition-preserving isomorphisms"]
297+
def trans (h1 : M ≃* N) (h2 : N ≃* P) : M ≃* P :=
298+
{ h1.toEquiv.trans h2.toEquiv with
299+
map_mul' := fun x y => show h2 (h1 (x * y)) = h2 (h1 x) * h2 (h1 y) by
300+
rw [map_mul, map_mul] }
301+
302+
@[to_additive (attr := simp)]
303+
theorem coe_trans (e₁ : M ≃* N) (e₂ : N ≃* P) : ↑(e₁.trans e₂) = e₂ ∘ e₁ := rfl
304+
305+
@[to_additive (attr := simp)]
306+
theorem trans_apply (e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) : e₁.trans e₂ m = e₂ (e₁ m) := rfl
307+
308+
@[to_additive (attr := simp)]
309+
theorem symm_trans_apply (e₁ : M ≃* N) (e₂ : N ≃* P) (p : P) :
310+
(e₁.trans e₂).symm p = e₁.symm (e₂.symm p) := rfl
311+
312+
@[to_additive (attr := simp)]
313+
theorem symm_trans_self (e : M ≃* N) : e.symm.trans e = refl N :=
314+
DFunLike.ext _ _ e.apply_symm_apply
315+
316+
@[to_additive (attr := simp)]
317+
theorem self_trans_symm (e : M ≃* N) : e.trans e.symm = refl M :=
318+
DFunLike.ext _ _ e.symm_apply_apply
319+
320+
end trans
321+
41322
section unique
42323

43324
/-- The `MulEquiv` between two monoids with a unique element. -/
@@ -66,6 +347,77 @@ end Mul
66347
## Monoids
67348
-/
68349

350+
section MulOneClass
351+
variable [MulOneClass M] [MulOneClass N] [MulOneClass P]
352+
353+
/-- A multiplicative isomorphism of monoids sends `1` to `1` (and is hence a monoid isomorphism). -/
354+
@[to_additive
355+
"An additive isomorphism of additive monoids sends `0` to `0`
356+
(and is hence an additive monoid isomorphism)."]
357+
protected lemma map_one (h : M ≃* N) : h 1 = 1 := map_one h
358+
359+
-- TODO: Why does this generate `h.toMonoidHom a = h.toFun a` rather than `h.toMonoidHom a = ⇑h a`?
360+
/-- Extract the forward direction of a multiplicative equivalence
361+
as a multiplication-preserving function. -/
362+
@[to_additive (attr := simps) "Extract the forward direction of an additive equivalence
363+
as an addition-preserving function."]
364+
def toMonoidHom (h : M ≃* N) : M →* N :=
365+
{ h with map_one' := h.map_one }
366+
367+
@[to_additive] instance : Coe (M ≃* N) (M →* N) := ⟨MulEquiv.toMonoidHom⟩
368+
369+
@[to_additive (attr := simp)]
370+
lemma coe_toMonoidHom (e : M ≃* N) : ⇑e.toMonoidHom = e := rfl
371+
372+
@[to_additive]
373+
lemma toMonoidHom_injective : Injective (toMonoidHom : M ≃* N → M →* N) :=
374+
.of_comp (f := DFunLike.coe) DFunLike.coe_injective
375+
376+
@[to_additive] lemma toMonoidHom_refl : (refl M : M →* M) = .id M := rfl
377+
378+
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/10618): `simp` can prove this but it is a valid `dsimp` lemma.
379+
-- However, we would need to redesign the `dsimp` set to make this `@[simp]`.
380+
@[to_additive]
381+
lemma toMonoidHom_trans (e₁ : M ≃* N) (e₂ : N ≃* P) :
382+
(e₁.trans e₂ : M →* P) = (e₂ : N →* P).comp ↑e₁ := rfl
383+
384+
@[to_additive (attr := simp)]
385+
lemma toMonoidHom_comp_toMonoidHom_symm (e : M ≃* N) :
386+
(e : M →* N).comp e.symm = MonoidHom.id _ := by ext; simp
387+
388+
@[to_additive (attr := simp)]
389+
lemma toMonoidHom_symm_comp_toMonoidHom (e : M ≃* N) :
390+
(e.symm : N →* M).comp e = MonoidHom.id _ := by ext; simp
391+
392+
@[to_additive]
393+
lemma comp_left_injective (e : M ≃* N) : Injective fun f : N →* P ↦ f.comp (e : M →* N) :=
394+
LeftInverse.injective (g := fun f ↦ f.comp e.symm) fun f ↦ by simp [MonoidHom.comp_assoc]
395+
396+
@[to_additive]
397+
lemma comp_right_injective (e : M ≃* N) : Injective fun f : P →* M ↦ (e : M →* N).comp f :=
398+
LeftInverse.injective (g := (e.symm : N →* M).comp) fun f ↦ by simp [← MonoidHom.comp_assoc]
399+
400+
@[to_additive]
401+
protected theorem map_eq_one_iff (h : M ≃* N) {x : M} : h x = 1 ↔ x = 1 :=
402+
EmbeddingLike.map_eq_one_iff
403+
404+
@[to_additive]
405+
theorem map_ne_one_iff (h : M ≃* N) {x : M} : h x ≠ 1 ↔ x ≠ 1 :=
406+
EmbeddingLike.map_ne_one_iff
407+
408+
/-- A bijective `Semigroup` homomorphism is an isomorphism -/
409+
@[to_additive (attr := simps! apply) "A bijective `AddSemigroup` homomorphism is an isomorphism"]
410+
noncomputable def ofBijective {M N F} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N]
411+
(f : F) (hf : Bijective f) : M ≃* N :=
412+
{ Equiv.ofBijective f hf with map_mul' := map_mul f }
413+
414+
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: simplify `symm_apply` to `surjInv`?
415+
@[to_additive (attr := simp)]
416+
theorem ofBijective_apply_symm_apply {n : N} (f : M →* N) (hf : Bijective f) :
417+
f ((ofBijective f hf).symm n) = n := (ofBijective f hf).apply_symm_apply n
418+
419+
end MulOneClass
420+
69421
/-- A multiplicative analogue of `Equiv.arrowCongr`,
70422
where the equivalence between the targets is multiplicative.
71423
-/

0 commit comments

Comments
 (0)