Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

refactor: review the simps projections of OneHom, MulHom, MonoidHom #19860

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
+103 −122
Open

refactor: review the simps projections of OneHom, MulHom, MonoidHom #19860

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -194,7 +194,7 @@ theorem prod_map_div : (m.map fun i => f i / g i).prod = (m.map f).prod / (m.map
@[to_additive]
theorem prod_map_zpow {n : ℤ} : (m.map fun i => f i ^ n).prod = (m.map f).prod ^ n := by
convert (m.map f).prod_hom (zpowGroupHom n : α →* α)
simp only [map_map, Function.comp_apply, zpowGroupHom_apply]
simp [map_map, Function.comp_apply]

end DivisionCommMonoid

Expand Down
193 changes: 90 additions & 103 deletions Mathlib/Algebra/Group/Hom/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -489,68 +489,94 @@ section Coes

/-! Bundled morphisms can be down-cast to weaker bundlings -/

attribute [coe] MonoidHom.toOneHom
attribute [coe] AddMonoidHom.toZeroHom
namespace OneHom
variable [One M] [One N]

/-- `MonoidHom` down-cast to a `OneHom`, forgetting the multiplicative property. -/
@[to_additive "`AddMonoidHom` down-cast to a `ZeroHom`, forgetting the additive property"]
instance MonoidHom.coeToOneHom [MulOneClass M] [MulOneClass N] :
Coe (M →* N) (OneHom M N) := ⟨MonoidHom.toOneHom⟩
/-- See Note [custom simps projection]. We want to generate
`coe_concreteHom : ⇑concreteHom = unbundledFun` rather than
`concreteHom_apply a : ⇑concreteHom a = unbundledFun a`. -/
@[to_additive
"/-- See Note [custom simps projection]. We want to generate
`coe_concreteHom : ⇑concreteHom = unbundledFun` rather than
`concreteHom_apply a : ⇑concreteHom a = unbundledFun a`. -/"]
def Simps.coe (f : OneHom M N) : M → N := f

attribute [coe] MonoidHom.toMulHom
attribute [coe] AddMonoidHom.toAddHom
initialize_simps_projections OneHom (toFun → coe, as_prefix coe)
initialize_simps_projections ZeroHom (toFun → coe, as_prefix coe)

/-- `MonoidHom` down-cast to a `MulHom`, forgetting the 1-preserving property. -/
@[to_additive "`AddMonoidHom` down-cast to an `AddHom`, forgetting the 0-preserving property."]
instance MonoidHom.coeToMulHom [MulOneClass M] [MulOneClass N] :
Coe (M →* N) (M →ₙ* N) := ⟨MonoidHom.toMulHom⟩
@[to_additive (attr := simp)] lemma toFun_eq_coe (f : OneHom M N) : f.toFun = f := rfl
@[to_additive (attr := simp)] lemma coe_mk (f : M → N) (hone) : (mk f hone : M → N) = f := rfl
@[to_additive (attr := simp)] lemma mk_coe (f : OneHom M N) : mk f f.map_one' = f := rfl

-- these must come after the coe_toFun definitions
initialize_simps_projections ZeroHom (toFun → apply)
initialize_simps_projections AddHom (toFun → apply)
initialize_simps_projections AddMonoidHom (toFun → apply)
initialize_simps_projections OneHom (toFun → apply)
initialize_simps_projections MulHom (toFun → apply)
initialize_simps_projections MonoidHom (toFun → apply)
@[to_additive (attr := ext)]
lemma ext ⦃f g : OneHom M N⦄ (h : ∀ x, f x = g x) : f = g := DFunLike.ext _ _ h

@[to_additive (attr := simp)]
theorem OneHom.coe_mk [One M] [One N] (f : M → N) (h1) : (OneHom.mk f h1 : M → N) = f := rfl
end OneHom

@[to_additive (attr := simp)]
theorem OneHom.toFun_eq_coe [One M] [One N] (f : OneHom M N) : f.toFun = f := rfl
namespace MulHom
variable [Mul M] [Mul N]

@[to_additive (attr := simp)]
theorem MulHom.coe_mk [Mul M] [Mul N] (f : M → N) (hmul) : (MulHom.mk f hmul : M → N) = f := rfl
/-- See Note [custom simps projection]. We want to generate
`coe_concreteHom : ⇑concreteHom = unbundledFun` rather than
`concreteHom_apply a : ⇑concreteHom a = unbundledFun a`. -/
@[to_additive
"/-- See Note [custom simps projection]. We want to generate
`coe_concreteHom : ⇑concreteHom = unbundledFun` rather than
`concreteHom_apply a : ⇑concreteHom a = unbundledFun a`. -/"]
def Simps.coe (f : M →ₙ* N) : M → N := f

@[to_additive (attr := simp)]
theorem MulHom.toFun_eq_coe [Mul M] [Mul N] (f : M →ₙ* N) : f.toFun = f := rfl
initialize_simps_projections MulHom (toFun → coe, as_prefix coe)
initialize_simps_projections AddHom (toFun → coe, as_prefix coe)

@[to_additive (attr := simp)]
theorem MonoidHom.coe_mk [MulOneClass M] [MulOneClass N] (f hmul) :
(MonoidHom.mk f hmul : M → N) = f := rfl
@[to_additive (attr := simp)] lemma toFun_eq_coe (f : M →ₙ* N) : f.toFun = f := rfl
@[to_additive (attr := simp)] lemma coe_mk (f : M → N) (hmul) : (mk f hmul : M → N) = f := rfl
@[to_additive (attr := simp)] lemma mk_coe (f : M →ₙ* N) : mk f f.map_mul' = f := rfl

@[to_additive (attr := simp)]
theorem MonoidHom.toOneHom_coe [MulOneClass M] [MulOneClass N] (f : M →* N) :
(f.toOneHom : M → N) = f := rfl
@[to_additive (attr := ext)]
lemma ext ⦃f g : M →ₙ* N⦄ (h : ∀ x, f x = g x) : f = g := DFunLike.ext _ _ h

@[to_additive (attr := simp)]
theorem MonoidHom.toMulHom_coe [MulOneClass M] [MulOneClass N] (f : M →* N) :
f.toMulHom.toFun = f := rfl
end MulHom

@[to_additive]
theorem MonoidHom.toFun_eq_coe [MulOneClass M] [MulOneClass N] (f : M →* N) : f.toFun = f := rfl
namespace MonoidHom
variable [MulOneClass M] [MulOneClass N]

@[to_additive (attr := ext)]
theorem OneHom.ext [One M] [One N] ⦃f g : OneHom M N⦄ (h : ∀ x, f x = g x) : f = g :=
DFunLike.ext _ _ h
attribute [coe] MonoidHom.toOneHom
attribute [coe] AddMonoidHom.toZeroHom
attribute [coe] MonoidHom.toMulHom
attribute [coe] AddMonoidHom.toAddHom

@[to_additive (attr := ext)]
theorem MulHom.ext [Mul M] [Mul N] ⦃f g : M →ₙ* N⦄ (h : ∀ x, f x = g x) : f = g :=
DFunLike.ext _ _ h
/-- `MonoidHom` down-cast to a `OneHom`, forgetting the multiplicative property. -/
@[to_additive "`AddMonoidHom` down-cast to a `ZeroHom`, forgetting the additive property"]
instance coeToOneHom : Coe (M →* N) (OneHom M N) := ⟨MonoidHom.toOneHom⟩

/-- `MonoidHom` down-cast to a `MulHom`, forgetting the 1-preserving property. -/
@[to_additive "`AddMonoidHom` down-cast to an `AddHom`, forgetting the 0-preserving property."]
instance coeToMulHom : Coe (M →* N) (M →ₙ* N) := ⟨MonoidHom.toMulHom⟩

/-- See Note [custom simps projection]. We want to generate
`coe_concreteHom : ⇑concreteHom = unbundledFun` rather than
`concreteHom_apply a : ⇑concreteHom a = unbundledFun a`. -/
@[to_additive
"/-- See Note [custom simps projection]. We want to generate
`coe_concreteHom : ⇑concreteHom = unbundledFun` rather than
`concreteHom_apply a : ⇑concreteHom a = unbundledFun a`. -/"]
def Simps.coe (f : M →* N) : M → N := f

initialize_simps_projections MonoidHom (toFun → coe, as_prefix coe)
initialize_simps_projections AddMonoidHom (toFun → coe, as_prefix coe)

@[to_additive (attr := simp)] lemma coe_toOneHom (f : M →* N) : f.toOneHom = f := rfl
@[to_additive (attr := simp)] lemma coe_toMulHom (f : M →* N) : f.toMulHom = f := rfl
@[to_additive (attr := simp)] lemma coe_mk (f hmul) : (mk f hmul : M → N) = f := rfl
@[to_additive (attr := simp)] lemma mk_coe (f : M →* N) : mk f f.map_mul' = f := rfl

@[to_additive] lemma toFun_eq_coe (f : M →* N) : f.toFun = f := rfl

@[to_additive (attr := ext)]
theorem MonoidHom.ext [MulOneClass M] [MulOneClass N] ⦃f g : M →* N⦄ (h : ∀ x, f x = g x) : f = g :=
DFunLike.ext _ _ h
lemma ext ⦃f g : M →* N⦄ (h : ∀ x, f x = g x) : f = g := DFunLike.ext _ _ h

end MonoidHom
end Coes

namespace MonoidHom

Expand All @@ -567,78 +593,45 @@ def mk' (f : M → G) (map_mul : ∀ a b : M, f (a * b) = f a * f b) : M →* G

end MonoidHom

section Deprecated

end Deprecated

@[to_additive (attr := simp)]
theorem OneHom.mk_coe [One M] [One N] (f : OneHom M N) (h1) : OneHom.mk f h1 = f :=
OneHom.ext fun _ => rfl

@[to_additive (attr := simp)]
theorem MulHom.mk_coe [Mul M] [Mul N] (f : M →ₙ* N) (hmul) : MulHom.mk f hmul = f :=
MulHom.ext fun _ => rfl

@[to_additive (attr := simp)]
theorem MonoidHom.mk_coe [MulOneClass M] [MulOneClass N] (f : M →* N) (hmul) :
MonoidHom.mk f hmul = f := MonoidHom.ext fun _ => rfl

end Coes

/-- Copy of a `OneHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
@[to_additive
@[to_additive (attr := simps (config := .asFn))
"Copy of a `ZeroHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities."]
protected def OneHom.copy [One M] [One N] (f : OneHom M N) (f' : M → N) (h : f' = f) :
OneHom M N where
toFun := f'
map_one' := h.symm ▸ f.map_one'

@[to_additive (attr := simp)]
theorem OneHom.coe_copy {_ : One M} {_ : One N} (f : OneHom M N) (f' : M → N) (h : f' = f) :
(f.copy f' h) = f' :=
rfl

@[to_additive]
theorem OneHom.coe_copy_eq {_ : One M} {_ : One N} (f : OneHom M N) (f' : M → N) (h : f' = f) :
f.copy f' h = f :=
DFunLike.ext' h

/-- Copy of a `MulHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
@[to_additive
@[to_additive (attr := simps (config := .asFn))
"Copy of an `AddHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities."]
protected def MulHom.copy [Mul M] [Mul N] (f : M →ₙ* N) (f' : M → N) (h : f' = f) :
M →ₙ* N where
toFun := f'
map_mul' := h.symm ▸ f.map_mul'

@[to_additive (attr := simp)]
theorem MulHom.coe_copy {_ : Mul M} {_ : Mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = f) :
(f.copy f' h) = f' :=
rfl

@[to_additive]
theorem MulHom.coe_copy_eq {_ : Mul M} {_ : Mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = f) :
f.copy f' h = f :=
DFunLike.ext' h

/-- Copy of a `MonoidHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities. -/
@[to_additive
@[to_additive (attr := simps! (config := .asFn))
"Copy of an `AddMonoidHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities."]
protected def MonoidHom.copy [MulOneClass M] [MulOneClass N] (f : M →* N) (f' : M → N)
(h : f' = f) : M →* N :=
{ f.toOneHom.copy f' h, f.toMulHom.copy f' h with }

@[to_additive (attr := simp)]
theorem MonoidHom.coe_copy {_ : MulOneClass M} {_ : MulOneClass N} (f : M →* N) (f' : M → N)
(h : f' = f) : (f.copy f' h) = f' :=
rfl

@[to_additive]
theorem MonoidHom.copy_eq {_ : MulOneClass M} {_ : MulOneClass N} (f : M →* N) (f' : M → N)
(h : f' = f) : f.copy f' h = f :=
Expand Down Expand Up @@ -688,19 +681,22 @@ theorem map_exists_left_inv (f : F) {x : M} (hx : ∃ y, y * x = 1) : ∃ y, y *
end MonoidHom

/-- The identity map from a type with 1 to itself. -/
@[to_additive (attr := simps) "The identity map from a type with zero to itself."]
@[to_additive (attr := simps (config := .asFn))
"The identity map from a type with zero to itself."]
def OneHom.id (M : Type*) [One M] : OneHom M M where
toFun x := x
map_one' := rfl

/-- The identity map from a type with multiplication to itself. -/
@[to_additive (attr := simps) "The identity map from a type with addition to itself."]
@[to_additive (attr := simps (config := .asFn))
"The identity map from a type with addition to itself."]
def MulHom.id (M : Type*) [Mul M] : M →ₙ* M where
toFun x := x
map_mul' _ _ := rfl

/-- The identity map from a monoid to itself. -/
@[to_additive (attr := simps) "The identity map from an additive monoid to itself."]
@[to_additive (attr := simps (config := .asFn))
"The identity map from an additive monoid to itself."]
def MonoidHom.id (M : Type*) [MulOneClass M] : M →* M where
toFun x := x
map_one' := rfl
Expand All @@ -716,37 +712,28 @@ lemma MulHom.coe_id {M : Type*} [Mul M] : (MulHom.id M : M → M) = _root_.id :=
lemma MonoidHom.coe_id {M : Type*} [MulOneClass M] : (MonoidHom.id M : M → M) = _root_.id := rfl

/-- Composition of `OneHom`s as a `OneHom`. -/
@[to_additive "Composition of `ZeroHom`s as a `ZeroHom`."]
@[to_additive (attr := simps (config := .asFn))
"Composition of `ZeroHom`s as a `ZeroHom`."]
def OneHom.comp [One M] [One N] [One P] (hnp : OneHom N P) (hmn : OneHom M N) : OneHom M P where
toFun := hnp ∘ hmn
map_one' := by simp

/-- Composition of `MulHom`s as a `MulHom`. -/
@[to_additive "Composition of `AddHom`s as an `AddHom`."]
@[to_additive (attr := simps (config := .asFn))
"Composition of `AddHom`s as an `AddHom`."]
def MulHom.comp [Mul M] [Mul N] [Mul P] (hnp : N →ₙ* P) (hmn : M →ₙ* N) : M →ₙ* P where
toFun := hnp ∘ hmn
map_mul' x y := by simp

/-- Composition of monoid morphisms as a monoid morphism. -/
@[to_additive "Composition of additive monoid morphisms as an additive monoid morphism."]
@[to_additive (attr := simps (config := .asFn))
"Composition of additive monoid morphisms as an additive monoid morphism."]
def MonoidHom.comp [MulOneClass M] [MulOneClass N] [MulOneClass P] (hnp : N →* P) (hmn : M →* N) :
M →* P where
toFun := hnp ∘ hmn
map_one' := by simp
map_mul' := by simp

@[to_additive (attr := simp)]
theorem OneHom.coe_comp [One M] [One N] [One P] (g : OneHom N P) (f : OneHom M N) :
↑(g.comp f) = g ∘ f := rfl

@[to_additive (attr := simp)]
theorem MulHom.coe_comp [Mul M] [Mul N] [Mul P] (g : N →ₙ* P) (f : M →ₙ* N) :
↑(g.comp f) = g ∘ f := rfl

@[to_additive (attr := simp)]
theorem MonoidHom.coe_comp [MulOneClass M] [MulOneClass N] [MulOneClass P]
(g : N →* P) (f : M →* N) : ↑(g.comp f) = g ∘ f := rfl

@[to_additive]
theorem OneHom.comp_apply [One M] [One N] [One P] (g : OneHom N P) (f : OneHom M N) (x : M) :
g.comp f x = g (f x) := rfl
Expand Down Expand Up @@ -856,7 +843,7 @@ protected theorem MonoidHom.map_zpow' [DivInvMonoid M] [DivInvMonoid N] (f : M
f (a ^ n) = f a ^ n := map_zpow' f hf a n

/-- Makes a `OneHom` inverse from the bijective inverse of a `OneHom` -/
@[to_additive (attr := simps)
@[to_additive (attr := simps (config := .asFn))
"Make a `ZeroHom` inverse from the bijective inverse of a `ZeroHom`"]
def OneHom.inverse [One M] [One N]
(f : OneHom M N) (g : N → M)
Expand All @@ -866,7 +853,7 @@ def OneHom.inverse [One M] [One N]
map_one' := by rw [← f.map_one, h₁] }

/-- Makes a multiplicative inverse from a bijection which preserves multiplication. -/
@[to_additive (attr := simps)
@[to_additive (attr := simps (config := .asFn))
"Makes an additive inverse from a bijection which preserves addition."]
def MulHom.inverse [Mul M] [Mul N] (f : M →ₙ* N) (g : N → M)
(h₁ : Function.LeftInverse g f)
Expand All @@ -879,7 +866,7 @@ def MulHom.inverse [Mul M] [Mul N] (f : M →ₙ* N) (g : N → M)
_ = g x * g y := h₁ _

/-- The inverse of a bijective `MonoidHom` is a `MonoidHom`. -/
@[to_additive (attr := simps)
@[to_additive (attr := simps (config := .asFn))
"The inverse of a bijective `AddMonoidHom` is an `AddMonoidHom`."]
def MonoidHom.inverse {A B : Type*} [Monoid A] [Monoid B] (f : A →* B) (g : B → A)
(h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : B →* A :=
Expand Down
17 changes: 6 additions & 11 deletions Mathlib/Algebra/Group/Subgroup/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -189,14 +189,13 @@ instance (priority := 75) toCommGroup {G : Type*} [CommGroup G] [SetLike S G] [S
(fun _ _ => rfl) fun _ _ => rfl

/-- The natural group hom from a subgroup of group `G` to `G`. -/
@[to_additive (attr := coe)
@[to_additive (attr := simps (config := .asFn))
"The natural group hom from an additive subgroup of `AddGroup` `G` to `G`."]
protected def subtype : H →* G where
toFun := ((↑) : H → G); map_one' := rfl; map_mul' := fun _ _ => rfl

@[to_additive (attr := simp)]
theorem coeSubtype : (SubgroupClass.subtype H : H → G) = ((↑) : H → G) := by
rfl
@[to_additive (attr := deprecated coe_subtype (since := "2024-12-10"))]
alias coeSubtype := coe_subtype

variable {H}

Expand Down Expand Up @@ -234,15 +233,13 @@ theorem inclusion_inclusion {L : S} (hHK : H ≤ K) (hKL : K ≤ L) (x : H) :
rfl

@[to_additive (attr := simp)]
theorem coe_inclusion {H K : S} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := by
cases a
simp only [inclusion, MonoidHom.mk'_apply]
theorem coe_inclusion {H K : S} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := rfl

@[to_additive (attr := simp)]
theorem subtype_comp_inclusion {H K : S} (hH : H ≤ K) :
(SubgroupClass.subtype K).comp (inclusion hH) = SubgroupClass.subtype H := by
ext
simp only [MonoidHom.comp_apply, coeSubtype, coe_inclusion]
simp only [MonoidHom.comp_apply, coe_subtype, coe_inclusion]

end SubgroupClass

Expand Down Expand Up @@ -534,9 +531,7 @@ def inclusion {H K : Subgroup G} (h : H ≤ K) : H →* K :=
MonoidHom.mk' (fun x => ⟨x, h x.2⟩) fun _ _ => rfl

@[to_additive (attr := simp)]
theorem coe_inclusion {H K : Subgroup G} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := by
cases a
simp only [inclusion, coe_mk, MonoidHom.mk'_apply]
theorem coe_inclusion {H K : Subgroup G} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := rfl

@[to_additive]
theorem inclusion_injective {H K : Subgroup G} (h : H ≤ K) : Function.Injective <| inclusion h :=
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Group/Submonoid/Operations.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -694,7 +694,7 @@ theorem restrict_mrange (f : M →* N) : mrange (f.restrict S) = S.map f := by
simp [SetLike.ext_iff]

/-- Restriction of a monoid hom to a submonoid of the codomain. -/
@[to_additive (attr := simps apply)
@[to_additive (attr := simps (config := .asFn))
"Restriction of an `AddMonoid` hom to an `AddSubmonoid` of the codomain."]
def codRestrict {S} [SetLike S N] [SubmonoidClass S N] (f : M →* N) (s : S) (h : ∀ x, f x ∈ s) :
M →* s where
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Group/WithOne/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ section
-- workaround: we make `WithOne`/`WithZero` irreducible for this definition, otherwise `simps`
-- will unfold it in the statement of the lemma it generates.
/-- `WithOne.coe` as a bundled morphism -/
@[to_additive (attr := simps apply) "`WithZero.coe` as a bundled morphism"]
@[to_additive (attr := simps) "`WithZero.coe` as a bundled morphism"]
def coeMulHom [Mul α] : α →ₙ* WithOne α where
toFun := coe
map_mul' _ _ := rfl
Expand Down
Loading
Loading