Pi instances for groups and monoids
This file defines instances for group, monoid, semigroup and related structures on Pi Types
@[instance]
def
pi.has_zero
{I : Type u}
{f : I → Type v}
[Π (i : I), has_zero (f i)] :
has_zero (Π (i : I), f i)
@[instance]
Equations
- pi.has_one = {one := λ (_x : I), 1}
@[simp]
@[simp]
@[instance]
Equations
- pi.has_mul = {mul := λ (f_1 g : Π (i : I), f i) (i : I), f_1 i * g i}
@[instance]
@[instance]
@[instance]
Equations
- pi.has_inv = {inv := λ (f_1 : Π (i : I), f i) (i : I), (f_1 i)⁻¹}
@[instance]
def
pi.semigroup
{I : Type u}
{f : I → Type v}
[Π (i : I), semigroup (f i)] :
semigroup (Π (i : I), f i)
Equations
- pi.semigroup = {mul := has_mul.mul pi.has_mul, mul_assoc := _}
@[instance]
def
pi.add_semigroup
{I : Type u}
{f : I → Type v}
[Π (i : I), add_semigroup (f i)] :
add_semigroup (Π (i : I), f i)
@[instance]
def
pi.add_comm_semigroup
{I : Type u}
{f : I → Type v}
[Π (i : I), add_comm_semigroup (f i)] :
add_comm_semigroup (Π (i : I), f i)
@[instance]
def
pi.comm_semigroup
{I : Type u}
{f : I → Type v}
[Π (i : I), comm_semigroup (f i)] :
comm_semigroup (Π (i : I), f i)
Equations
- pi.comm_semigroup = {mul := has_mul.mul pi.has_mul, mul_assoc := _, mul_comm := _}
@[instance]
Equations
- pi.monoid = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _}
@[instance]
def
pi.add_monoid
{I : Type u}
{f : I → Type v}
[Π (i : I), add_monoid (f i)] :
add_monoid (Π (i : I), f i)
@[instance]
def
pi.comm_monoid
{I : Type u}
{f : I → Type v}
[Π (i : I), comm_monoid (f i)] :
comm_monoid (Π (i : I), f i)
Equations
- pi.comm_monoid = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, mul_comm := _}
@[instance]
def
pi.add_comm_monoid
{I : Type u}
{f : I → Type v}
[Π (i : I), add_comm_monoid (f i)] :
add_comm_monoid (Π (i : I), f i)
@[instance]
def
pi.add_group
{I : Type u}
{f : I → Type v}
[Π (i : I), add_group (f i)] :
add_group (Π (i : I), f i)
@[instance]
Equations
- pi.group = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, inv := has_inv.inv pi.has_inv, mul_left_inv := _}
@[instance]
def
pi.add_comm_group
{I : Type u}
{f : I → Type v}
[Π (i : I), add_comm_group (f i)] :
add_comm_group (Π (i : I), f i)
@[instance]
def
pi.comm_group
{I : Type u}
{f : I → Type v}
[Π (i : I), comm_group (f i)] :
comm_group (Π (i : I), f i)
Equations
- pi.comm_group = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, inv := has_inv.inv pi.has_inv, mul_left_inv := _, mul_comm := _}
@[instance]
def
pi.add_left_cancel_semigroup
{I : Type u}
{f : I → Type v}
[Π (i : I), add_left_cancel_semigroup (f i)] :
add_left_cancel_semigroup (Π (i : I), f i)
@[instance]
def
pi.left_cancel_semigroup
{I : Type u}
{f : I → Type v}
[Π (i : I), left_cancel_semigroup (f i)] :
left_cancel_semigroup (Π (i : I), f i)
Equations
- pi.left_cancel_semigroup = {mul := has_mul.mul pi.has_mul, mul_assoc := _, mul_left_cancel := _}
@[instance]
def
pi.right_cancel_semigroup
{I : Type u}
{f : I → Type v}
[Π (i : I), right_cancel_semigroup (f i)] :
right_cancel_semigroup (Π (i : I), f i)
Equations
- pi.right_cancel_semigroup = {mul := has_mul.mul pi.has_mul, mul_assoc := _, mul_right_cancel := _}
@[instance]
def
pi.add_right_cancel_semigroup
{I : Type u}
{f : I → Type v}
[Π (i : I), add_right_cancel_semigroup (f i)] :
add_right_cancel_semigroup (Π (i : I), f i)
@[instance]
def
pi.ordered_cancel_comm_monoid
{I : Type u}
{f : I → Type v}
[Π (i : I), ordered_cancel_comm_monoid (f i)] :
ordered_cancel_comm_monoid (Π (i : I), f i)
Equations
- pi.ordered_cancel_comm_monoid = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, mul_comm := _, mul_left_cancel := _, mul_right_cancel := _, le := has_le.le (preorder.to_has_le (Π (i : I), f i)), lt := has_lt.lt (preorder.to_has_lt (Π (i : I), f i)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}
@[instance]
def
pi.ordered_cancel_add_comm_monoid
{I : Type u}
{f : I → Type v}
[Π (i : I), ordered_cancel_add_comm_monoid (f i)] :
ordered_cancel_add_comm_monoid (Π (i : I), f i)
@[instance]
def
pi.ordered_add_comm_group
{I : Type u}
{f : I → Type v}
[Π (i : I), ordered_add_comm_group (f i)] :
ordered_add_comm_group (Π (i : I), f i)
@[instance]
def
pi.ordered_comm_group
{I : Type u}
{f : I → Type v}
[Π (i : I), ordered_comm_group (f i)] :
ordered_comm_group (Π (i : I), f i)
Equations
- pi.ordered_comm_group = {mul := comm_group.mul pi.comm_group, mul_assoc := _, one := comm_group.one pi.comm_group, one_mul := _, mul_one := _, inv := comm_group.inv pi.comm_group, mul_left_inv := _, mul_comm := _, le := partial_order.le pi.partial_order, lt := partial_order.lt pi.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}
def
pi.single
{I : Type u}
{f : I → Type v}
[decidable_eq I]
[Π (i : I), has_zero (f i)]
(i : I)
(x : f i)
(i_1 : I) :
f i_1
The function supported at i, with value x there.
@[simp]
theorem
pi.single_eq_same
{I : Type u}
{f : I → Type v}
[decidable_eq I]
[Π (i : I), has_zero (f i)]
(i : I)
(x : f i) :
@[simp]
theorem
pi.single_eq_of_ne
{I : Type u}
{f : I → Type v}
[decidable_eq I]
[Π (i : I), has_zero (f i)]
{i i' : I}
(h : i' ≠ i)
(x : f i) :
def
add_monoid_hom.apply
{I : Type u}
(f : I → Type v)
[Π (i : I), add_monoid (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.
def
monoid_hom.apply
{I : Type u}
(f : I → Type v)
[Π (i : I), monoid (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.
@[simp]
theorem
add_monoid_hom.apply_apply
{I : Type u}
(f : I → Type v)
[Π (i : I), add_monoid (f i)]
(i : I)
(g : Π (i : I), f i) :
⇑(add_monoid_hom.apply f i) g = g i
@[simp]
theorem
monoid_hom.apply_apply
{I : Type u}
(f : I → Type v)
[Π (i : I), monoid (f i)]
(i : I)
(g : Π (i : I), f i) :
⇑(monoid_hom.apply f i) g = g i
def
add_monoid_hom.single
{I : Type u}
(f : I → Type v)
[decidable_eq I]
[Π (i : I), add_monoid (f i)]
(i : I) :
f i →+ Π (i : I), f i
The additive monoid homomorphism including a single additive monoid into a dependent family of additive monoids, as functions supported at a point.
@[simp]
theorem
add_monoid_hom.single_apply
{I : Type u}
(f : I → Type v)
[decidable_eq I]
[Π (i : I), add_monoid (f i)]
{i : I}
(x : f i) :
⇑(add_monoid_hom.single f i) x = pi.single i x