Skip to content

Commit 72a0444

Browse files
ADedeckerADedecker
committed
chore: rename Pi.monoidHom to MonoidHom.pi (leanprover-community#40024)
Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Pi.2EfooHom.20or.20FooHom.2Epi/near/598538630
1 parent f6eb107 commit 72a0444

5 files changed

Lines changed: 45 additions & 21 deletions

File tree

‎Mathlib/Algebra/Category/Grp/Yoneda.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -52,5 +52,5 @@ This is also the coyoneda embedding of `Type` into `AddCommGrpCat`-valued preshe
5252
groups. -/]
5353
def CommGrpCat.coyonedaType : (Type u)ᵒᵖ ⥤ CommGrpCat.{u} ⥤ CommGrpCat.{u} where
5454
obj X := { obj G := of <| X.unop → G
55-
map f := ofHom <| Pi.monoidHom fun i ↦ f.hom.comp <| Pi.evalMonoidHom _ i }
56-
map f := { app G := ofHom <| Pi.monoidHom fun i ↦ Pi.evalMonoidHom _ <| f.unop i }
55+
map f := ofHom <| MonoidHom.pi fun i ↦ f.hom.comp <| Pi.evalMonoidHom _ i }
56+
map f := { app G := ofHom <| MonoidHom.pi fun i ↦ Pi.evalMonoidHom _ <| f.unop i }

‎Mathlib/Algebra/Category/MonCat/Yoneda.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -53,5 +53,5 @@ This is also the coyoneda embedding of `Type` into `AddCommMonCat`-valued preshe
5353
monoids. -/]
5454
def CommMonCat.coyonedaType : Type uᵒᵖ ⥤ CommMonCat.{u} ⥤ CommMonCat.{u} where
5555
obj X := { obj M := of <| X.unop → M
56-
map f := ofHom <| Pi.monoidHom fun i ↦ f.hom.comp <| Pi.evalMonoidHom _ i }
57-
map f := { app N := ofHom <| Pi.monoidHom fun i ↦ Pi.evalMonoidHom _ <| f.unop i }
56+
map f := ofHom <| MonoidHom.pi fun i ↦ f.hom.comp <| Pi.evalMonoidHom _ i }
57+
map f := { app N := ofHom <| MonoidHom.pi fun i ↦ Pi.evalMonoidHom _ <| f.unop i }

‎Mathlib/Algebra/Group/Pi/Lemmas.lean‎

Lines changed: 36 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -64,37 +64,61 @@ end MulHom
6464

6565
section MulHom
6666

67-
/-- A family of MulHom's `f a : γ →ₙ* β a` defines a MulHom `Pi.mulHom f : γ →ₙ* Π a, β a`
68-
given by `Pi.mulHom f x b = f b x`. -/
67+
/-- A family of MulHom's `f a : γ →ₙ* β a` defines a MulHom `MulHom.pi f : γ →ₙ* Π a, β a`
68+
given by `MulHom.pi f x b = f b x`. -/
6969
@[to_additive (attr := simps)
70-
/-- A family of AddHom's `f a : γ → β a` defines an AddHom `Pi.addHom f : γ → Π a, β a` given by
71-
`Pi.addHom f x b = f b x`. -/]
72-
def Pi.mulHom {γ : Type w} [∀ i, Mul (f i)] [Mul γ] (g : ∀ i, γ →ₙ* f i) : γ →ₙ* ∀ i, f i where
70+
/-- A family of AddHom's `f a : γ → β a` defines an AddHom `AddHom.pi f : γ → Π a, β a` given by
71+
`AddHom.pi f x b = f b x`. -/]
72+
def MulHom.pi {γ : Type w} [∀ i, Mul (f i)] [Mul γ] (g : ∀ i, γ →ₙ* f i) : γ →ₙ* ∀ i, f i where
7373
toFun x i := g i x
7474
map_mul' x y := funext fun i => (g i).map_mul x y
7575

76+
@[deprecated (since := "2026-05-29")] alias Pi.addHom := AddHom.pi
77+
@[to_additive existing (attr := deprecated "MulHom.pi" (since := "2026-05-29"))] alias
78+
Pi.mulHom := MulHom.pi
79+
80+
@[deprecated (since := "2026-05-29")] alias Pi.addHom_apply := AddHom.pi_apply
81+
@[to_additive existing (attr := deprecated "MulHom.pi_apply" (since := "2026-05-29"))] alias
82+
Pi.mulHom_apply := MulHom.pi_apply
83+
7684
@[to_additive]
77-
theorem Pi.mulHom_injective {γ : Type w} [Nonempty I] [∀ i, Mul (f i)] [Mul γ] (g : ∀ i, γ →ₙ* f i)
78-
(hg : ∀ i, Function.Injective (g i)) : Function.Injective (Pi.mulHom g) := fun _ _ h =>
85+
theorem MulHom.injective_pi {γ : Type w} [Nonempty I] [∀ i, Mul (f i)] [Mul γ] (g : ∀ i, γ →ₙ* f i)
86+
(hg : ∀ i, Function.Injective (g i)) : Function.Injective (MulHom.pi g) := fun _ _ h =>
7987
let ⟨i⟩ := ‹Nonempty I›
8088
hg i ((funext_iff.mp h :) i)
8189

90+
@[deprecated (since := "2026-05-29")] alias Pi.addHom_injective := AddHom.injective_pi
91+
@[to_additive existing (attr := deprecated "MulHom.injective_pi" (since := "2026-05-29"))] alias
92+
Pi.mulHom_injective := MulHom.injective_pi
93+
8294
/-- A family of monoid homomorphisms `f a : γ →* β a` defines a monoid homomorphism
8395
`Pi.monoidHom f : γ →* Π a, β a` given by `Pi.monoidHom f x b = f b x`. -/
8496
@[to_additive (attr := simps)
8597
/-- A family of additive monoid homomorphisms `f a : γ →+ β a` defines a monoid homomorphism
8698
`Pi.addMonoidHom f : γ →+ Π a, β a` given by `Pi.addMonoidHom f x b = f b x`. -/]
87-
def Pi.monoidHom {γ : Type w} [∀ i, MulOneClass (f i)] [MulOneClass γ] (g : ∀ i, γ →* f i) :
99+
def MonoidHom.pi {γ : Type w} [∀ i, MulOneClass (f i)] [MulOneClass γ] (g : ∀ i, γ →* f i) :
88100
γ →* ∀ i, f i :=
89-
{ Pi.mulHom fun i => (g i).toMulHom with
101+
{ MulHom.pi fun i => (g i).toMulHom with
90102
toFun := fun x i => g i x
91103
map_one' := funext fun i => (g i).map_one }
92104

105+
@[deprecated (since := "2026-05-29")] alias Pi.addMonoidHom := AddMonoidHom.pi
106+
@[to_additive existing (attr := deprecated "MonoidHom.pi" (since := "2026-05-29"))] alias
107+
Pi.monoidHom := MonoidHom.pi
108+
109+
@[deprecated (since := "2026-05-29")] alias Pi.addMonoidHom_apply := AddMonoidHom.pi_apply
110+
@[to_additive existing (attr := deprecated "MonoidHom.pi_apply" (since := "2026-05-29"))] alias
111+
Pi.monoidHom_apply := MonoidHom.pi_apply
112+
93113
@[to_additive]
94-
theorem Pi.monoidHom_injective {γ : Type w} [Nonempty I] [∀ i, MulOneClass (f i)] [MulOneClass γ]
114+
theorem MonoidHom.injective_pi {γ : Type w} [Nonempty I] [∀ i, MulOneClass (f i)] [MulOneClass γ]
95115
(g : ∀ i, γ →* f i) (hg : ∀ i, Function.Injective (g i)) :
96-
Function.Injective (Pi.monoidHom g) :=
97-
Pi.mulHom_injective (fun i => (g i).toMulHom) hg
116+
Function.Injective (MonoidHom.pi g) :=
117+
MulHom.injective_pi (fun i => (g i).toMulHom) hg
118+
119+
@[deprecated (since := "2026-05-29")] alias Pi.addMonoidHom_injective := AddMonoidHom.injective_pi
120+
@[to_additive existing (attr := deprecated "MonoidHom.injective_pi" (since := "2026-05-29"))] alias
121+
Pi.monoidHom_injective := MonoidHom.injective_pi
98122

99123
variable (f)
100124
variable [(i : I) → Mul (f i)]

‎Mathlib/Algebra/Ring/Pi.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -96,26 +96,26 @@ homomorphism `Pi.nonUnitalRingHom f : γ →+* Π a, β a` given by
9696
@[simps]
9797
protected def nonUnitalRingHom {γ : Type w} [∀ i, NonUnitalNonAssocSemiring (f i)]
9898
[NonUnitalNonAssocSemiring γ] (g : ∀ i, γ →ₙ+* f i) : γ →ₙ+* ∀ i, f i :=
99-
{ Pi.mulHom fun i => (g i).toMulHom, Pi.addMonoidHom fun i => (g i).toAddMonoidHom with
99+
{ MulHom.pi fun i => (g i).toMulHom, AddMonoidHom.pi fun i => (g i).toAddMonoidHom with
100100
toFun := fun x b => g b x }
101101

102102
theorem nonUnitalRingHom_injective {γ : Type w} [Nonempty I]
103103
[∀ i, NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : ∀ i, γ →ₙ+* f i)
104104
(hg : ∀ i, Function.Injective (g i)) : Function.Injective (Pi.nonUnitalRingHom g) :=
105-
mulHom_injective (fun i => (g i).toMulHom) hg
105+
MulHom.injective_pi (fun i => (g i).toMulHom) hg
106106

107107
/-- A family of ring homomorphisms `f a : γ →+* β a` defines a ring homomorphism
108108
`Pi.ringHom f : γ →+* Π a, β a` given by `Pi.ringHom f x b = f b x`. -/
109109
@[simps]
110110
protected def ringHom {γ : Type w} [∀ i, NonAssocSemiring (f i)] [NonAssocSemiring γ]
111111
(g : ∀ i, γ →+* f i) : γ →+* ∀ i, f i :=
112-
{ Pi.monoidHom fun i => (g i).toMonoidHom, Pi.addMonoidHom fun i => (g i).toAddMonoidHom with
112+
{ MonoidHom.pi fun i => (g i).toMonoidHom, AddMonoidHom.pi fun i => (g i).toAddMonoidHom with
113113
toFun := fun x b => g b x }
114114

115115
theorem ringHom_injective {γ : Type w} [Nonempty I] [∀ i, NonAssocSemiring (f i)]
116116
[NonAssocSemiring γ] (g : ∀ i, γ →+* f i) (hg : ∀ i, Function.Injective (g i)) :
117117
Function.Injective (Pi.ringHom g) :=
118-
monoidHom_injective (fun i => (g i).toMonoidHom) hg
118+
MonoidHom.injective_pi (fun i => (g i).toMonoidHom) hg
119119

120120
end Pi
121121

‎Mathlib/LinearAlgebra/Pi.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ variable [Semiring R] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃]
5454
/-- `pi` construction for linear functions. From a family of linear functions it produces a linear
5555
function into a family of modules. -/
5656
def pi (f : (i : ι) → M₂ →ₗ[R] φ i) : M₂ →ₗ[R] (i : ι) → φ i :=
57-
{ Pi.addHom fun i => (f i).toAddHom with
57+
{ AddHom.pi fun i => (f i).toAddHom with
5858
toFun := fun c i => f i c
5959
map_smul' := fun _ _ => funext fun i => (f i).map_smul _ _ }
6060

0 commit comments

Comments
 (0)