Pi instances for groups and monoids #
This file defines instances for group, monoid, semigroup and related structures on Pi types.
Equations
- Pi.addCommSemigroup = let src := Pi.addSemigroup; AddCommSemigroup.mk (_ : ∀ (a b : (i : I) → f i), a + b = b + a)
Equations
- Pi.commSemigroup = let src := Pi.semigroup; CommSemigroup.mk (_ : ∀ (a b : (i : I) → f i), a * b = b * a)
Equations
- Pi.addMonoidWithOne = let src := Pi.addMonoid; AddMonoidWithOne.mk
Equations
- (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0)
Equations
- (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)
Equations
- Pi.addCommMonoid = let src := Pi.addMonoid; let src_1 := Pi.addCommSemigroup; AddCommMonoid.mk (_ : ∀ (a b : (i : I) → f i), a + b = b + a)
Equations
- Pi.commMonoid = let src := Pi.monoid; let src_1 := Pi.commSemigroup; CommMonoid.mk (_ : ∀ (a b : (i : I) → f i), a * b = b * a)
Equations
- (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)
Equations
- Pi.subNegMonoid = let src := Pi.addMonoid; SubNegMonoid.mk fun z x i => z • x i
Equations
- Pi.divInvMonoid = let src := Pi.monoid; DivInvMonoid.mk fun z x i => x i ^ z
Equations
- Pi.involutiveNeg = InvolutiveNeg.mk (_ : ∀ (x : (i : I) → f i), - -x = x)
Equations
- Pi.involutiveInv = InvolutiveInv.mk (_ : ∀ (x : (i : I) → f i), x⁻¹⁻¹ = x)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (a : (i : I) → f i), SubNegMonoid.zsmul 0 a = 0) = (_ : ∀ (a : (i : I) → f i), SubNegMonoid.zsmul 0 a = 0)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Pi.subtractionCommMonoid = let src := Pi.subtractionMonoid; let src_1 := Pi.addCommSemigroup; SubtractionCommMonoid.mk (_ : ∀ (a b : (i : I) → f i), a + b = b + a)
Equations
- Pi.instDivisionCommMonoidForAll = let src := Pi.divisionMonoid; let src_1 := Pi.commSemigroup; DivisionCommMonoid.mk (_ : ∀ (a b : (i : I) → f i), a * b = b * a)
Equations
- (_ : ∀ (a : (i : I) → f i), SubNegMonoid.zsmul 0 a = 0) = (_ : ∀ (a : (i : I) → f i), SubNegMonoid.zsmul 0 a = 0)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Pi.addGroupWithOne = let src := Pi.addGroup; let src_1 := Pi.addMonoidWithOne; AddGroupWithOne.mk SubNegMonoid.zsmul (_ : ∀ (a : (i : I) → f i), -a + a = 0)
Equations
- Pi.addCommGroup = let src := Pi.addGroup; let src_1 := Pi.addCommMonoid; AddCommGroup.mk (_ : ∀ (a b : (i : I) → f i), a + b = b + a)
Equations
- (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)
Equations
- (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : (i : I) → f i), AddMonoid.nsmul 0 x = 0)
Equations
- (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : (i : I) → f i), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (x : (i : I) → f i), AddLeftCancelMonoid.nsmul 0 x = 0) = (_ : ∀ (x : (i : I) → f i), AddLeftCancelMonoid.nsmul 0 x = 0)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (x : (i : I) → f i), AddLeftCancelMonoid.nsmul 0 x = 0) = (_ : ∀ (x : (i : I) → f i), AddLeftCancelMonoid.nsmul 0 x = 0)
Equations
- Pi.addCancelCommMonoid = let src := Pi.addLeftCancelMonoid; let src_1 := Pi.addCommMonoid; AddCancelCommMonoid.mk (_ : ∀ (a b : (i : I) → f i), a + b = b + a)
Equations
- One or more equations did not get rendered due to their size.
Equations
- Pi.cancelCommMonoid = let src := Pi.leftCancelMonoid; let src_1 := Pi.commMonoid; CancelCommMonoid.mk (_ : ∀ (a b : (i : I) → f i), a * b = b * a)
Equations
- Pi.addHom_injective.match_1 motive x h_1 = Nonempty.casesOn x fun val => h_1 val
Equations
- One or more equations did not get rendered due to their size.
A family of additive monoid homomorphisms f a : γ →+ β a→+ β a
defines a monoid homomorphism
Pi.addMonoidHom f : γ →+ Π a, β a→+ Π a, β a
given by Pi.addMonoidHom f x b = f b x
.
Equations
- One or more equations did not get rendered due to their size.
A family of monoid homomorphisms f a : γ →* β a→* β a
defines a monoid homomorphism
Pi.monoidHom f : γ →* Π a, β a→* Π a, β a
given by Pi.monoidHom f x b = f b x
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : (((i : I) → f i) + ((i : I) → f i)) ((i : I) → f i) instHAdd x x i = x i + x i) = (_ : (((i : I) → f i) + ((i : I) → f i)) ((i : I) → f i) instHAdd x x i = x i + x 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 => g i, map_add' := (_ : ∀ (x x_1 : (i : I) → f i), (((i : I) → f i) + ((i : I) → f i)) ((i : I) → f i) instHAdd x x_1 i = x i + x_1 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 => g i, map_mul' := (_ : ∀ (x x_1 : (i : I) → f i), (((i : I) → f i) * ((i : I) → f i)) ((i : I) → f i) instHMul x x_1 i = x i * x_1 i) }
Equations
- (_ : Function.const α (x + x) = Function.const α (x + x)) = (_ : Function.const α (x + x) = Function.const α (x + x))
Function.const
as an AddHom
.
Equations
- Pi.constAddHom α β = { toFun := Function.const α, map_add' := (_ : ∀ (x x_1 : β), Function.const α (x + x_1) = Function.const α (x + x_1)) }
Function.const
as a MulHom
.
Equations
- Pi.constMulHom α β = { toFun := Function.const α, map_mul' := (_ : ∀ (x x_1 : β), Function.const α (x * x_1) = Function.const α (x * x_1)) }
Coercion of an AddHom
into a function is itself an AddHom
.
See also AddHom.eval
.
Coercion of a MulHom
into a function is itself a MulHom
.
See also MulHom.eval
.
Equations
- (_ : (((i : I) → f i) + ((i : I) → f i)) ((i : I) → f i) instHAdd x x i = x i + x i) = (_ : (((i : I) → f i) + ((i : I) → f i)) ((i : I) → f i) instHAdd x x i = x i + x 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
- One or more equations did not get rendered due to their size.
Equations
- (_ : OfNat.ofNat ((i : I) → f i) 0 Zero.toOfNat0 i = 0) = (_ : OfNat.ofNat ((i : I) → f i) 0 Zero.toOfNat0 i = 0)
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
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.const α 0 = Function.const α 0) = (_ : Function.const α 0 = Function.const α 0)
Function.const
as an AddMonoidHom
.
Equations
- One or more equations did not get rendered due to their size.
Function.const
as a MonoidHom
.
Equations
- One or more equations did not get rendered due to their size.
Coercion of an AddMonoidHom
into a function is itself
a AddMonoidHom
.
See also AddMonoidHom.eval
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Coercion of a MonoidHom
into a function is itself a MonoidHom
.
See also MonoidHom.eval
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Additive monoid homomorphism between the function spaces I → α→ α
and I → β→ β
, induced by an
additive monoid homomorphism f
between α
and β
Equations
- One or more equations did not get rendered due to their size.
Monoid homomorphism between the function spaces I → α→ α
and I → β→ β
, induced by a monoid
homomorphism f
between α
and β
.
Equations
- One or more equations did not get rendered due to their size.
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' := (_ : Pi.single i 0 = 0) }
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' := (_ : Pi.mulSingle i 1 = 1) }
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
- One or more equations did not get rendered due to their size.
Equations
- (_ : ZeroHom.toFun (ZeroHom.single f i) 0 = 0) = (_ : ZeroHom.toFun (ZeroHom.single f i) 0 = 0)
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
- One or more equations did not get rendered due to their size.
The multiplicative homomorphism including a single MulZeroClass
into a dependent family of MulZeroClass
es, as functions supported at a point.
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
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.extend s 0 0 = 0) = (_ : Function.extend s 0 0 = 0)
Equations
- One or more equations did not get rendered due to their size.
Function.extend s f 1
as a bundled hom.
Equations
- One or more equations did not get rendered due to their size.