Extra lemmas about products of monoids and groups #
This file proves lemmas about the instances defined in Algebra.Group.Pi.Basic
that require more
imports.
Equations
- Pi.addMonoidWithOne = let __src := Pi.addMonoid; AddMonoidWithOne.mk ⋯ ⋯
Equations
- Pi.addGroupWithOne = let __src := Pi.addGroup; let __src_1 := Pi.addMonoidWithOne; AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- Pi.mulZeroClass = MulZeroClass.mk ⋯ ⋯
Equations
- Pi.mulZeroOneClass = let __src := Pi.mulZeroClass; let __src_1 := Pi.mulOneClass; MulZeroOneClass.mk ⋯ ⋯
Equations
- Pi.monoidWithZero = let __src := Pi.monoid; let __src_1 := Pi.mulZeroClass; MonoidWithZero.mk ⋯ ⋯
Equations
- Pi.commMonoidWithZero = let __src := Pi.monoidWithZero; let __src_1 := Pi.commMonoid; CommMonoidWithZero.mk ⋯ ⋯
Equations
- Pi.semigroupWithZero = let __src := Pi.semigroup; let __src_1 := Pi.mulZeroClass; SemigroupWithZero.mk ⋯ ⋯
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 g = let __src := Pi.addHom fun (i : I) => ↑(g i); { toZeroHom := { toFun := fun (x : γ) (i : I) => (g i) x, map_zero' := ⋯ }, map_add' := ⋯ }
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 g = let __src := Pi.mulHom fun (i : I) => ↑(g i); { toOneHom := { toFun := fun (x : γ) (i : I) => (g i) x, map_one' := ⋯ }, map_mul' := ⋯ }
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' := ⋯ }
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' := ⋯ }
Function.const
as an AddHom
.
Equations
- Pi.constAddHom α β = { toFun := Function.const α, map_add' := ⋯ }
Function.const
as a MulHom
.
Equations
- Pi.constMulHom α β = { toFun := Function.const α, map_mul' := ⋯ }
Coercion of an AddHom
into a function is itself an AddHom
.
See also AddHom.eval
.
Equations
- AddHom.coeFn α β = { toFun := fun (g : AddHom α β) => ⇑g, map_add' := ⋯ }
Coercion of a MulHom
into a function is itself a MulHom
.
See also MulHom.eval
.
Equations
- MulHom.coeFn α β = { toFun := fun (g : α →ₙ* β) => ⇑g, map_mul' := ⋯ }
Additive semigroup homomorphism between the function spaces I → α
and I → β
, induced by an additive semigroup homomorphism f
between α
and β
Equations
- AddHom.compLeft f I = { toFun := fun (h : I → α) => ⇑f ∘ h, map_add' := ⋯ }
Semigroup homomorphism between the function spaces I → α
and I → β
, induced by a semigroup
homomorphism f
between α
and β
.
Equations
- MulHom.compLeft f I = { toFun := fun (h : I → α) => ⇑f ∘ h, map_mul' := ⋯ }
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 = { toZeroHom := { toFun := fun (g : (i : I) → f i) => g i, map_zero' := ⋯ }, map_add' := ⋯ }
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 = { toOneHom := { toFun := fun (g : (i : I) → f i) => g i, map_one' := ⋯ }, map_mul' := ⋯ }
Function.const
as an AddMonoidHom
.
Equations
- Pi.constAddMonoidHom α β = { toZeroHom := { toFun := Function.const α, map_zero' := ⋯ }, map_add' := ⋯ }
Function.const
as a MonoidHom
.
Equations
- Pi.constMonoidHom α β = { toOneHom := { toFun := Function.const α, map_one' := ⋯ }, map_mul' := ⋯ }
Coercion of an AddMonoidHom
into a function is itself
an AddMonoidHom
.
See also AddMonoidHom.eval
.
Equations
- AddMonoidHom.coeFn α β = { toZeroHom := { toFun := fun (g : α →+ β) => ⇑g, map_zero' := ⋯ }, map_add' := ⋯ }
Coercion of a MonoidHom
into a function is itself a MonoidHom
.
See also MonoidHom.eval
.
Equations
- MonoidHom.coeFn α β = { toOneHom := { toFun := fun (g : α →* β) => ⇑g, map_one' := ⋯ }, map_mul' := ⋯ }
Additive monoid homomorphism between the function spaces I → α
and I → β
, induced by an
additive monoid homomorphism f
between α
and β
Equations
- AddMonoidHom.compLeft f I = { toZeroHom := { toFun := fun (h : I → α) => ⇑f ∘ h, map_zero' := ⋯ }, map_add' := ⋯ }
Monoid homomorphism between the function spaces I → α
and I → β
, induced by a monoid
homomorphism f
between α
and β
.
Equations
- MonoidHom.compLeft f I = { toOneHom := { toFun := fun (h : I → α) => ⇑f ∘ h, map_one' := ⋯ }, map_mul' := ⋯ }
The zero-preserving homomorphism including a single value into a dependent family of values, as functions supported at a point.
This is the ZeroHom
version of Pi.single
.
Equations
- ZeroHom.single f i = { toFun := Pi.single i, map_zero' := ⋯ }
The one-preserving homomorphism including a single value into a dependent family of values, as functions supported at a point.
This is the OneHom
version of Pi.mulSingle
.
Equations
- OneHom.single f i = { toFun := Pi.mulSingle i, map_one' := ⋯ }
The additive monoid homomorphism including a single additive monoid into a dependent family of additive monoids, as functions supported at a point.
This is the AddMonoidHom
version of Pi.single
.
Equations
- AddMonoidHom.single f i = let __src := ZeroHom.single f i; { toZeroHom := __src, map_add' := ⋯ }
The monoid homomorphism including a single monoid into a dependent family of additive monoids, as functions supported at a point.
This is the MonoidHom
version of Pi.mulSingle
.
Equations
- MonoidHom.single f i = let __src := OneHom.single f i; { toOneHom := __src, map_mul' := ⋯ }
The multiplicative homomorphism including a single MulZeroClass
into a dependent family of MulZeroClass
es, as functions supported at a point.
This is the MulHom
version of Pi.single
.
Equations
- MulHom.single f i = { toFun := Pi.single i, map_mul' := ⋯ }
The injection into an additive pi group at different indices commutes.
For injections of commuting elements at the same index, see AddCommute.map
The injection into a pi group at different indices commutes.
For injections of commuting elements at the same index, see Commute.map
The injection into an additive pi group with the same values commutes.
The injection into a pi group with the same values commutes.
Function.extend s f 0
as a bundled hom.
Equations
- Function.ExtendByZero.hom R s = { toZeroHom := { toFun := fun (f : ι → R) => Function.extend s f 0, map_zero' := ⋯ }, map_add' := ⋯ }
Function.extend s f 1
as a bundled hom.
Equations
- Function.ExtendByOne.hom R s = { toOneHom := { toFun := fun (f : ι → R) => Function.extend s f 1, map_one' := ⋯ }, map_mul' := ⋯ }