Extra definitions about products of monoids and groups

This file defines various operations on products as bundled homomorphisms.

def MulHom.pi {I : Type u_3} {f : I → Type u_4} [(i : I) → Mul (f i)] {γ : Type u_7} [Mul γ] (g : (i : I) → γ →ₙ* f i) : γ →ₙ* (i : I) → f i

A family of MulHom's f a : γ →ₙ* β a defines a MulHom MulHom.pi f : γ →ₙ* Π a, β a given by MulHom.pi f x b = f b x.

Equations

• MulHom.pi g = { toFun := fun (x : γ) (i : I) => (g i) x, map_mul' := ⋯ }

def AddHom.pi {I : Type u_3} {f : I → Type u_4} [(i : I) → Add (f i)] {γ : Type u_7} [Add γ] (g : (i : I) → γ →ₙ+ f i) : γ →ₙ+ (i : I) → f i

A family of AddHom's f a : γ → β a defines an AddHom AddHom.pi f : γ → Π a, β a given by AddHom.pi f x b = f b x.

Equations

• AddHom.pi g = { toFun := fun (x : γ) (i : I) => (g i) x, map_add' := ⋯ }

@[simp]

theorem MulHom.pi_apply {I : Type u_3} {f : I → Type u_4} [(i : I) → Mul (f i)] {γ : Type u_7} [Mul γ] (g : (i : I) → γ →ₙ* f i) (x : γ) (i : I) : (pi g) x i = (g i) x

@[simp]

theorem AddHom.pi_apply {I : Type u_3} {f : I → Type u_4} [(i : I) → Add (f i)] {γ : Type u_7} [Add γ] (g : (i : I) → γ →ₙ+ f i) (x : γ) (i : I) : (pi g) x i = (g i) x

@[deprecated MulHom.pi (since := "2026-05-29")]

def Pi.mulHom {I : Type u_3} {f : I → Type u_4} [(i : I) → Mul (f i)] {γ : Type u_7} [Mul γ] (g : (i : I) → γ →ₙ* f i) : γ →ₙ* (i : I) → f i

Alias of MulHom.pi.

---

A family of MulHom's f a : γ →ₙ* β a defines a MulHom MulHom.pi f : γ →ₙ* Π a, β a given by MulHom.pi f x b = f b x.

Equations

• @Pi.mulHom = @MulHom.pi

@[deprecated AddHom.pi (since := "2026-05-29")]

def Pi.addHom {I : Type u_3} {f : I → Type u_4} [(i : I) → Add (f i)] {γ : Type u_7} [Add γ] (g : (i : I) → γ →ₙ+ f i) : γ →ₙ+ (i : I) → f i

Alias of AddHom.pi.

---

A family of AddHom's f a : γ → β a defines an AddHom AddHom.pi f : γ → Π a, β a given by AddHom.pi f x b = f b x.

Equations

• @Pi.addHom = @AddHom.pi

@[deprecated MulHom.pi_apply (since := "2026-05-29")]

theorem Pi.mulHom_apply {I : Type u_3} {f : I → Type u_4} [(i : I) → Mul (f i)] {γ : Type u_7} [Mul γ] (g : (i : I) → γ →ₙ* f i) (x : γ) (i : I) : (MulHom.pi g) x i = (g i) x

Alias of MulHom.pi_apply.

@[deprecated AddHom.pi_apply (since := "2026-05-29")]

theorem Pi.addHom_apply {I : Type u_3} {f : I → Type u_4} [(i : I) → Add (f i)] {γ : Type u_7} [Add γ] (g : (i : I) → γ →ₙ+ f i) (x : γ) (i : I) : (AddHom.pi g) x i = (g i) x

Alias of AddHom.pi_apply.

theorem MulHom.pi_injective {I : Type u_3} {f : I → Type u_4} [(i : I) → Mul (f i)] {γ : Type u_7} [Nonempty I] [Mul γ] (g : (i : I) → γ →ₙ* f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(pi g)

theorem AddHom.pi_injective {I : Type u_3} {f : I → Type u_4} [(i : I) → Add (f i)] {γ : Type u_7} [Nonempty I] [Add γ] (g : (i : I) → γ →ₙ+ f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(pi g)

@[deprecated MulHom.pi_injective (since := "2026-05-29")]

theorem MulHom.injective_pi {I : Type u_3} {f : I → Type u_4} [(i : I) → Mul (f i)] {γ : Type u_7} [Nonempty I] [Mul γ] (g : (i : I) → γ →ₙ* f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(pi g)

Alias of MulHom.pi_injective.

@[deprecated AddHom.pi_injective (since := "2026-05-29")]

theorem AddHom.injective_pi {I : Type u_3} {f : I → Type u_4} [(i : I) → Add (f i)] {γ : Type u_7} [Nonempty I] [Add γ] (g : (i : I) → γ →ₙ+ f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(pi g)

Alias of AddHom.pi_injective.

@[deprecated MulHom.pi_injective (since := "2026-05-29")]

theorem Pi.mulHom_injective {I : Type u_3} {f : I → Type u_4} [(i : I) → Mul (f i)] {γ : Type u_7} [Nonempty I] [Mul γ] (g : (i : I) → γ →ₙ* f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(MulHom.pi g)

Alias of MulHom.pi_injective.

@[deprecated AddHom.pi_injective (since := "2026-05-29")]

theorem Pi.addHom_injective {I : Type u_3} {f : I → Type u_4} [(i : I) → Add (f i)] {γ : Type u_7} [Nonempty I] [Add γ] (g : (i : I) → γ →ₙ+ f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(AddHom.pi g)

Alias of AddHom.pi_injective.

def Pi.evalMulHom {I : Type u_3} (f : I → Type u_4) [(i : I) → Mul (f i)] (i : I) : ((i : I) → f i) →ₙ* f i

Evaluation of functions into an indexed collection of semigroups at a point is a semigroup homomorphism. This is Function.eval i as a MulHom.

Equations

• Pi.evalMulHom f i = { toFun := fun (g : (i : I) → f i) => g i, map_mul' := ⋯ }

def Pi.evalAddHom {I : Type u_3} (f : I → Type u_4) [(i : I) → Add (f i)] (i : I) : ((i : I) → f i) →ₙ+ f i

Evaluation of functions into an indexed collection of additive semigroups at a point is an additive semigroup homomorphism. This is Function.eval i as an AddHom.

Equations

• Pi.evalAddHom f i = { toFun := fun (g : (i : I) → f i) => g i, map_add' := ⋯ }

@[simp]

theorem Pi.evalMulHom_apply {I : Type u_3} (f : I → Type u_4) [(i : I) → Mul (f i)] (i : I) (g : (i : I) → f i) : (evalMulHom f i) g = g i

@[simp]

theorem Pi.evalAddHom_apply {I : Type u_3} (f : I → Type u_4) [(i : I) → Add (f i)] (i : I) (g : (i : I) → f i) : (evalAddHom f i) g = g i

def MulHom.piMap {ι : Type u_1} {M : ι → Type u_5} {N : ι → Type u_6} [(i : ι) → Mul (M i)] [(i : ι) → Mul (N i)] (g : (i : ι) → M i →ₙ* N i) : ((i : ι) → M i) →ₙ* (i : ι) → N i

A family of MulHom's f i : M i →ₙ* N i defines a MulHom MulHom.piMap f : (Π i, M i) →ₙ* (Π i, N i) given by MulHom.piMap f x i = f i x. This is Pi.map for MulHoms.

Equations

• MulHom.piMap g = MulHom.pi fun (i : ι) => (g i).comp (Pi.evalMulHom M i)

def AddHom.piMap {ι : Type u_1} {M : ι → Type u_5} {N : ι → Type u_6} [(i : ι) → Add (M i)] [(i : ι) → Add (N i)] (g : (i : ι) → M i →ₙ+ N i) : ((i : ι) → M i) →ₙ+ (i : ι) → N i

A family of AddHom's f i : M i →ₙ+ N i defines an AddHom AddHom.piMap f : (Π i, M i) →ₙ+ (Π i, N i) given by AddHom.piMap f x i = f i x. This is Pi.map for AddHoms.

Equations

• AddHom.piMap g = AddHom.pi fun (i : ι) => (g i).comp (Pi.evalAddHom M i)

@[simp]

theorem AddHom.piMap_apply {ι : Type u_1} {M : ι → Type u_5} {N : ι → Type u_6} [(i : ι) → Add (M i)] [(i : ι) → Add (N i)] (g : (i : ι) → M i →ₙ+ N i) (x : (i : ι) → M i) (i : ι) : (piMap g) x i = (g i) (x i)

@[simp]

theorem MulHom.piMap_apply {ι : Type u_1} {M : ι → Type u_5} {N : ι → Type u_6} [(i : ι) → Mul (M i)] [(i : ι) → Mul (N i)] (g : (i : ι) → M i →ₙ* N i) (x : (i : ι) → M i) (i : ι) : (piMap g) x i = (g i) (x i)

def Pi.constMulHom (α : Type u_7) (β : Type u_8) [Mul β] : β →ₙ* α → β

Function.const as a MulHom.

Equations

• Pi.constMulHom α β = { toFun := Function.const α, map_mul' := ⋯ }

def Pi.constAddHom (α : Type u_7) (β : Type u_8) [Add β] : β →ₙ+ α → β

Function.const as an AddHom.

Equations

• Pi.constAddHom α β = { toFun := Function.const α, map_add' := ⋯ }

@[simp]

theorem Pi.constMulHom_apply (α : Type u_7) (β : Type u_8) [Mul β] (a : β) (a✝ : α) : (constMulHom α β) a a✝ = Function.const α a a✝

@[simp]

theorem Pi.constAddHom_apply (α : Type u_7) (β : Type u_8) [Add β] (a : β) (a✝ : α) : (constAddHom α β) a a✝ = Function.const α a a✝

def MulHom.compLeft {α : Type u_7} {β : Type u_8} [Mul α] [Mul β] (f : α →ₙ* β) (I : Type u_9) : (I → α) →ₙ* I → β

Semigroup homomorphism between the function spaces I → α and I → β, induced by a semigroup homomorphism f between α and β.

Equations

• f.compLeft I = { toFun := fun (h : I → α) => ⇑f ∘ h, map_mul' := ⋯ }

def AddHom.compLeft {α : Type u_7} {β : Type u_8} [Add α] [Add β] (f : α →ₙ+ β) (I : Type u_9) : (I → α) →ₙ+ I → β

Additive semigroup homomorphism between the function spaces I → α and I → β, induced by an additive semigroup homomorphism f between α and β

Equations

• f.compLeft I = { toFun := fun (h : I → α) => ⇑f ∘ h, map_add' := ⋯ }

@[simp]

theorem MulHom.compLeft_apply {α : Type u_7} {β : Type u_8} [Mul α] [Mul β] (f : α →ₙ* β) (I : Type u_9) (h : I → α) (a✝ : I) : (f.compLeft I) h a✝ = (⇑f ∘ h) a✝

@[simp]

theorem AddHom.compLeft_apply {α : Type u_7} {β : Type u_8} [Add α] [Add β] (f : α →ₙ+ β) (I : Type u_9) (h : I → α) (a✝ : I) : (f.compLeft I) h a✝ = (⇑f ∘ h) a✝

def MonoidHom.pi {I : Type u_3} {f : I → Type u_4} [(i : I) → MulOneClass (f i)] {γ : Type u_7} [MulOneClass γ] (g : (i : I) → γ →* f i) : γ →* (i : I) → f i

A family of monoid homomorphisms f a : γ →* β a defines a monoid homomorphism Pi.monoidHom f : γ →* Π a, β a given by Pi.monoidHom f x b = f b x.

Equations

• MonoidHom.pi g = { toFun := fun (x : γ) (i : I) => (g i) x, map_one' := ⋯, map_mul' := ⋯ }

def AddMonoidHom.pi {I : Type u_3} {f : I → Type u_4} [(i : I) → AddZeroClass (f i)] {γ : Type u_7} [AddZeroClass γ] (g : (i : I) → γ →+ f i) : γ →+ (i : I) → f i

A family of additive monoid homomorphisms f a : γ →+ β a defines a monoid homomorphism Pi.addMonoidHom f : γ →+ Π a, β a given by Pi.addMonoidHom f x b = f b x.

Equations

• AddMonoidHom.pi g = { toFun := fun (x : γ) (i : I) => (g i) x, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidHom.pi_apply {I : Type u_3} {f : I → Type u_4} [(i : I) → AddZeroClass (f i)] {γ : Type u_7} [AddZeroClass γ] (g : (i : I) → γ →+ f i) (x : γ) (i : I) : (pi g) x i = (g i) x

@[simp]

theorem MonoidHom.pi_apply {I : Type u_3} {f : I → Type u_4} [(i : I) → MulOneClass (f i)] {γ : Type u_7} [MulOneClass γ] (g : (i : I) → γ →* f i) (x : γ) (i : I) : (pi g) x i = (g i) x

@[deprecated MonoidHom.pi (since := "2026-05-29")]

def Pi.monoidHom {I : Type u_3} {f : I → Type u_4} [(i : I) → MulOneClass (f i)] {γ : Type u_7} [MulOneClass γ] (g : (i : I) → γ →* f i) : γ →* (i : I) → f i

Alias of MonoidHom.pi.

---

A family of monoid homomorphisms f a : γ →* β a defines a monoid homomorphism Pi.monoidHom f : γ →* Π a, β a given by Pi.monoidHom f x b = f b x.

Equations

• @Pi.monoidHom = @MonoidHom.pi

@[deprecated AddMonoidHom.pi (since := "2026-05-29")]

def Pi.addMonoidHom {I : Type u_3} {f : I → Type u_4} [(i : I) → AddZeroClass (f i)] {γ : Type u_7} [AddZeroClass γ] (g : (i : I) → γ →+ f i) : γ →+ (i : I) → f i

Alias of AddMonoidHom.pi.

---

A family of additive monoid homomorphisms f a : γ →+ β a defines a monoid homomorphism Pi.addMonoidHom f : γ →+ Π a, β a given by Pi.addMonoidHom f x b = f b x.

Equations

• @Pi.addMonoidHom = @AddMonoidHom.pi

@[deprecated MonoidHom.pi_apply (since := "2026-05-29")]

theorem Pi.monoidHom_apply {I : Type u_3} {f : I → Type u_4} [(i : I) → MulOneClass (f i)] {γ : Type u_7} [MulOneClass γ] (g : (i : I) → γ →* f i) (x : γ) (i : I) : (MonoidHom.pi g) x i = (g i) x

Alias of MonoidHom.pi_apply.

@[deprecated AddMonoidHom.pi_apply (since := "2026-05-29")]

theorem Pi.addMonoidHom_apply {I : Type u_3} {f : I → Type u_4} [(i : I) → AddZeroClass (f i)] {γ : Type u_7} [AddZeroClass γ] (g : (i : I) → γ →+ f i) (x : γ) (i : I) : (AddMonoidHom.pi g) x i = (g i) x

Alias of AddMonoidHom.pi_apply.

theorem MonoidHom.pi_injective {I : Type u_3} {f : I → Type u_4} [(i : I) → MulOneClass (f i)] {γ : Type u_7} [Nonempty I] [MulOneClass γ] (g : (i : I) → γ →* f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(pi g)

theorem AddMonoidHom.pi_injective {I : Type u_3} {f : I → Type u_4} [(i : I) → AddZeroClass (f i)] {γ : Type u_7} [Nonempty I] [AddZeroClass γ] (g : (i : I) → γ →+ f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(pi g)

@[deprecated MonoidHom.pi_injective (since := "2026-05-29")]

theorem MonoidHom.injective_pi {I : Type u_3} {f : I → Type u_4} [(i : I) → MulOneClass (f i)] {γ : Type u_7} [Nonempty I] [MulOneClass γ] (g : (i : I) → γ →* f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(pi g)

Alias of MonoidHom.pi_injective.

@[deprecated AddMonoidHom.pi_injective (since := "2026-05-29")]

theorem AddMonoidHom.injective_pi {I : Type u_3} {f : I → Type u_4} [(i : I) → AddZeroClass (f i)] {γ : Type u_7} [Nonempty I] [AddZeroClass γ] (g : (i : I) → γ →+ f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(pi g)

Alias of AddMonoidHom.pi_injective.

@[deprecated MonoidHom.pi_injective (since := "2026-05-29")]

theorem Pi.monoidHom_injective {I : Type u_3} {f : I → Type u_4} [(i : I) → MulOneClass (f i)] {γ : Type u_7} [Nonempty I] [MulOneClass γ] (g : (i : I) → γ →* f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(MonoidHom.pi g)

Alias of MonoidHom.pi_injective.

@[deprecated AddMonoidHom.pi_injective (since := "2026-05-29")]

theorem Pi.addMonoidHom_injective {I : Type u_3} {f : I → Type u_4} [(i : I) → AddZeroClass (f i)] {γ : Type u_7} [Nonempty I] [AddZeroClass γ] (g : (i : I) → γ →+ f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(AddMonoidHom.pi g)

Alias of AddMonoidHom.pi_injective.

def Pi.evalMonoidHom {I : Type u_3} (f : I → Type u_4) [(i : I) → MulOneClass (f i)] (i : I) : ((i : I) → f i) →* f i

Evaluation of functions into an indexed collection of monoids at a point is a monoid homomorphism. This is Function.eval i as a MonoidHom.

Equations

• Pi.evalMonoidHom f i = { toFun := fun (g : (i : I) → f i) => g i, map_one' := ⋯, map_mul' := ⋯ }

def Pi.evalAddMonoidHom {I : Type u_3} (f : I → Type u_4) [(i : I) → AddZeroClass (f i)] (i : I) : ((i : I) → f i) →+ f i

Evaluation of functions into an indexed collection of additive monoids at a point is an additive monoid homomorphism. This is Function.eval i as an AddMonoidHom.

Equations

• Pi.evalAddMonoidHom f i = { toFun := fun (g : (i : I) → f i) => g i, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Pi.evalAddMonoidHom_apply {I : Type u_3} (f : I → Type u_4) [(i : I) → AddZeroClass (f i)] (i : I) (g : (i : I) → f i) : (evalAddMonoidHom f i) g = g i

@[simp]

theorem Pi.evalMonoidHom_apply {I : Type u_3} (f : I → Type u_4) [(i : I) → MulOneClass (f i)] (i : I) (g : (i : I) → f i) : (evalMonoidHom f i) g = g i

@[simp]

theorem Pi.coe_evalMonoidHom {I : Type u_3} (f : I → Type u_4) [(i : I) → MulOneClass (f i)] (i : I) : ⇑(evalMonoidHom f i) = Function.eval i

def MonoidHom.piMap {ι : Type u_1} {M : ι → Type u_5} {N : ι → Type u_6} [(i : ι) → MulOneClass (M i)] [(i : ι) → MulOneClass (N i)] (g : (i : ι) → M i →* N i) : ((i : ι) → M i) →* (i : ι) → N i

A family of monoid homomorphisms f i : M i →* N i defines a monoid homomorphism MonoidHom.piMap f : (Π i, M i) →* (Π i, N i) given by MonoidHom.piMap f x i = f i x. This is Pi.map for MonoidHoms.

Equations

• MonoidHom.piMap g = MonoidHom.pi fun (i : ι) => (g i).comp (Pi.evalMonoidHom M i)

def AddMonoidHom.piMap {ι : Type u_1} {M : ι → Type u_5} {N : ι → Type u_6} [(i : ι) → AddZeroClass (M i)] [(i : ι) → AddZeroClass (N i)] (g : (i : ι) → M i →+ N i) : ((i : ι) → M i) →+ (i : ι) → N i

A family of additive monoid homomorphisms f i : M i →+ N i defines an additive monoid homomorphism AddMonoidHom.piMap f : (Π i, M i) →+ (Π i, N i) given by AddMonoidHom.piMap f x i = f i x. This is Pi.map for AddMonoidHoms.

Equations

• AddMonoidHom.piMap g = AddMonoidHom.pi fun (i : ι) => (g i).comp (Pi.evalAddMonoidHom M i)

@[simp]

theorem MonoidHom.piMap_apply {ι : Type u_1} {M : ι → Type u_5} {N : ι → Type u_6} [(i : ι) → MulOneClass (M i)] [(i : ι) → MulOneClass (N i)] (g : (i : ι) → M i →* N i) (x : (i : ι) → M i) (i : ι) : (piMap g) x i = (g i) (x i)

@[simp]

theorem AddMonoidHom.piMap_apply {ι : Type u_1} {M : ι → Type u_5} {N : ι → Type u_6} [(i : ι) → AddZeroClass (M i)] [(i : ι) → AddZeroClass (N i)] (g : (i : ι) → M i →+ N i) (x : (i : ι) → M i) (i : ι) : (piMap g) x i = (g i) (x i)

def Pi.constMonoidHom (α : Type u_7) (β : Type u_8) [MulOneClass β] : β →* α → β

Function.const as a MonoidHom.

Equations

• Pi.constMonoidHom α β = { toFun := Function.const α, map_one' := ⋯, map_mul' := ⋯ }

def Pi.constAddMonoidHom (α : Type u_7) (β : Type u_8) [AddZeroClass β] : β →+ α → β

Function.const as an AddMonoidHom.

Equations

• Pi.constAddMonoidHom α β = { toFun := Function.const α, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Pi.constAddMonoidHom_apply (α : Type u_7) (β : Type u_8) [AddZeroClass β] (a : β) (a✝ : α) : (constAddMonoidHom α β) a a✝ = Function.const α a a✝

@[simp]

theorem Pi.constMonoidHom_apply (α : Type u_7) (β : Type u_8) [MulOneClass β] (a : β) (a✝ : α) : (constMonoidHom α β) a a✝ = Function.const α a a✝

def MonoidHom.compLeft {α : Type u_7} {β : Type u_8} [MulOneClass α] [MulOneClass β] (f : α →* β) (I : Type u_9) : (I → α) →* I → β

Monoid homomorphism between the function spaces I → α and I → β, induced by a monoid homomorphism f between α and β.

Equations

• f.compLeft I = { toFun := fun (h : I → α) => ⇑f ∘ h, map_one' := ⋯, map_mul' := ⋯ }

def AddMonoidHom.compLeft {α : Type u_7} {β : Type u_8} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (I : Type u_9) : (I → α) →+ I → β

Additive monoid homomorphism between the function spaces I → α and I → β, induced by an additive monoid homomorphism f between α and β

Equations

• f.compLeft I = { toFun := fun (h : I → α) => ⇑f ∘ h, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidHom.compLeft_apply {α : Type u_7} {β : Type u_8} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (I : Type u_9) (h : I → α) (a✝ : I) : (f.compLeft I) h a✝ = (⇑f ∘ h) a✝

@[simp]

theorem MonoidHom.compLeft_apply {α : Type u_7} {β : Type u_8} [MulOneClass α] [MulOneClass β] (f : α →* β) (I : Type u_9) (h : I → α) (a✝ : I) : (f.compLeft I) h a✝ = (⇑f ∘ h) a✝