mathlib documentation

algebra.group.pi

Pi instances for groups and monoids #

This file defines instances for group, monoid, semigroup and related structures on Pi types.

source
@[protected, instance]
def pi.add_semigroup {I : Type u} {f : I → Type v} [Π (i : I), add_semigroup (f i)] :
add_semigroup (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.semigroup {I : Type u} {f : I → Type v} [Π (i : I), semigroup (f i)] :
semigroup (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.semigroup_with_zero {I : Type u} {f : I → Type v} [Π (i : I), semigroup_with_zero (f i)] :
semigroup_with_zero (Π (i : I), f i)
Equations
source
@[protected, 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
source
@[protected, 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)
Equations
source
@[protected, instance]
def pi.mul_one_class {I : Type u} {f : I → Type v} [Π (i : I), mul_one_class (f i)] :
mul_one_class (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.add_zero_class {I : Type u} {f : I → Type v} [Π (i : I), add_zero_class (f i)] :
add_zero_class (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.add_monoid {I : Type u} {f : I → Type v} [Π (i : I), add_monoid (f i)] :
add_monoid (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.monoid {I : Type u} {f : I → Type v} [Π (i : I), monoid (f i)] :
monoid (Π (i : I), f i)
Equations
source
@[simp]
theorem pi.pow_apply {I : Type u} {f : I → Type v} (x : Π (i : I), f i) (i : I) [Π (i : I), monoid (f i)] (n : ℕ) :
(x ^ n) i = x i ^ n
source
theorem pi.nsmul_apply {I : Type u} {f : I → Type v} (x : Π (i : I), f i) (i : I) [Π (i : I), add_monoid (f i)] (n : ℕ) :
(n • x) i = n • x i
source
@[protected, 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
source
@[protected, 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)
Equations
source
@[protected, instance]
def pi.sub_neg_add_monoid {I : Type u} {f : I → Type v} [Π (i : I), sub_neg_monoid (f i)] :
sub_neg_monoid (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.div_inv_monoid {I : Type u} {f : I → Type v} [Π (i : I), div_inv_monoid (f i)] :
div_inv_monoid (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.add_group {I : Type u} {f : I → Type v} [Π (i : I), add_group (f i)] :
add_group (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.group {I : Type u} {f : I → Type v} [Π (i : I), group (f i)] :
group (Π (i : I), f i)
Equations
source
@[protected, 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)
Equations
source
@[protected, 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
source
@[protected, 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)
Equations
source
@[protected, 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
source
@[protected, 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
source
@[protected, 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)
Equations
source
@[protected, instance]
def pi.add_left_cancel_monoid {I : Type u} {f : I → Type v} [Π (i : I), add_left_cancel_monoid (f i)] :
add_left_cancel_monoid (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.left_cancel_monoid {I : Type u} {f : I → Type v} [Π (i : I), left_cancel_monoid (f i)] :
left_cancel_monoid (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.add_right_cancel_monoid {I : Type u} {f : I → Type v} [Π (i : I), add_right_cancel_monoid (f i)] :
add_right_cancel_monoid (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.right_cancel_monoid {I : Type u} {f : I → Type v} [Π (i : I), right_cancel_monoid (f i)] :
right_cancel_monoid (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.add_cancel_monoid {I : Type u} {f : I → Type v} [Π (i : I), add_cancel_monoid (f i)] :
add_cancel_monoid (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.cancel_monoid {I : Type u} {f : I → Type v} [Π (i : I), cancel_monoid (f i)] :
cancel_monoid (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.cancel_comm_monoid {I : Type u} {f : I → Type v} [Π (i : I), cancel_comm_monoid (f i)] :
cancel_comm_monoid (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.add_cancel_comm_monoid {I : Type u} {f : I → Type v} [Π (i : I), add_cancel_comm_monoid (f i)] :
add_cancel_comm_monoid (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.mul_zero_class {I : Type u} {f : I → Type v} [Π (i : I), mul_zero_class (f i)] :
mul_zero_class (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.mul_zero_one_class {I : Type u} {f : I → Type v} [Π (i : I), mul_zero_one_class (f i)] :
mul_zero_one_class (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.monoid_with_zero {I : Type u} {f : I → Type v} [Π (i : I), monoid_with_zero (f i)] :
monoid_with_zero (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.comm_monoid_with_zero {I : Type u} {f : I → Type v} [Π (i : I), comm_monoid_with_zero (f i)] :
comm_monoid_with_zero (Π (i : I), f i)
Equations
source
theorem add_hom.coe_add {M : Type u_1} {N : Type u_2} {mM : has_add M} {mN : add_comm_semigroup N} (f g : add_hom M N) :
⇑f + ⇑g = λ (x : M), ⇑f x + ⇑g x
source
theorem mul_hom.coe_mul {M : Type u_1} {N : Type u_2} {mM : has_mul M} {mN : comm_semigroup N} (f g : M →ₙ* N) :
(⇑f) * ⇑g = λ (x : M), (⇑f x) * ⇑g x
source
@[simp]
theorem pi.eval_add_monoid_hom_apply {I : Type u} (f : I → Type v) [Π (i : I), add_zero_class (f i)] (i : I) (g : Π (i : I), f i) :
⇑(pi.eval_add_monoid_hom f i) g = g i
source
def pi.eval_add_monoid_hom {I : Type u} (f : I → Type v) [Π (i : I), add_zero_class (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 add_monoid_hom.

Equations
source
def pi.eval_monoid_hom {I : Type u} (f : I → Type v) [Π (i : I), mul_one_class (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 monoid_hom.

Equations
source
@[simp]
theorem pi.eval_monoid_hom_apply {I : Type u} (f : I → Type v) [Π (i : I), mul_one_class (f i)] (i : I) (g : Π (i : I), f i) :
⇑(pi.eval_monoid_hom f i) g = g i
source
def pi.const_add_monoid_hom (α : Type u_1) (β : Type u_2) [add_zero_class β] :
β →+ α → β

function.const as an add_monoid_hom.

Equations
source
def pi.const_monoid_hom (α : Type u_1) (β : Type u_2) [mul_one_class β] :
β →* α → β

function.const as a monoid_hom.

Equations
source
@[simp]
theorem pi.const_monoid_hom_apply (α : Type u_1) (β : Type u_2) [mul_one_class β] (a : β) (ᾰ : α) :
⇑(pi.const_monoid_hom α β) a ᾰ = function.const α a ᾰ
source
@[simp]
theorem pi.const_add_monoid_hom_apply (α : Type u_1) (β : Type u_2) [add_zero_class β] (a : β) (ᾰ : α) :
⇑(pi.const_add_monoid_hom α β) a ᾰ = function.const α a ᾰ
source
def monoid_hom.coe_fn (α : Type u_1) (β : Type u_2) [mul_one_class α] [comm_monoid β] :
(α →* β) →* α → β

Coercion of a monoid_hom into a function is itself a monoid_hom.

See also monoid_hom.eval.

Equations
source
@[simp]
theorem monoid_hom.coe_fn_apply (α : Type u_1) (β : Type u_2) [mul_one_class α] [comm_monoid β] (g : α →* β) (ᾰ : α) :
⇑(monoid_hom.coe_fn α β) g ᾰ = ⇑g ᾰ
source
def add_monoid_hom.coe_fn (α : Type u_1) (β : Type u_2) [add_zero_class α] [add_comm_monoid β] :
(α →+ β) →+ α → β

Coercion of an add_monoid_hom into a function is itself a add_monoid_hom.

See also add_monoid_hom.eval.

Equations
source
@[simp]
theorem add_monoid_hom.coe_fn_apply (α : Type u_1) (β : Type u_2) [add_zero_class α] [add_comm_monoid β] (g : α →+ β) (ᾰ : α) :
⇑(add_monoid_hom.coe_fn α β) g ᾰ = ⇑g ᾰ
source
@[protected]
def add_monoid_hom.comp_left {α : Type u_1} {β : Type u_2} [add_zero_class α] [add_zero_class β] (f : α →+ β) (I : Type u_3) :
(I → α) →+ I → β

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

Equations
source
@[simp]
theorem monoid_hom.comp_left_apply {α : Type u_1} {β : Type u_2} [mul_one_class α] [mul_one_class β] (f : α →* β) (I : Type u_3) (h : I → α) (ᾰ : I) :
⇑(f.comp_left I) h ᾰ = (⇑f ∘ h) ᾰ
source
@[simp]
theorem add_monoid_hom.comp_left_apply {α : Type u_1} {β : Type u_2} [add_zero_class α] [add_zero_class β] (f : α →+ β) (I : Type u_3) (h : I → α) (ᾰ : I) :
⇑(f.comp_left I) h ᾰ = (⇑f ∘ h) ᾰ
source
@[protected]
def monoid_hom.comp_left {α : Type u_1} {β : Type u_2} [mul_one_class α] [mul_one_class β] (f : α →* β) (I : Type u_3) :
(I → α) →* I → β

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

Equations
source
def one_hom.single {I : Type u} (f : I → Type v) [decidable_eq I] [Π (i : I), has_one (f i)] (i : I) :
one_hom (f i) (Π (i : I), f i)

The one-preserving homomorphism including a single value into a dependent family of values, as functions supported at a point.

This is the one_hom version of pi.mul_single.

Equations
source
def zero_hom.single {I : Type u} (f : I → Type v) [decidable_eq I] [Π (i : I), has_zero (f i)] (i : I) :
zero_hom (f i) (Π (i : I), f i)

The zero-preserving homomorphism including a single value into a dependent family of values, as functions supported at a point.

This is the zero_hom version of pi.single.

Equations
source
@[simp]
theorem zero_hom.single_apply {I : Type u} (f : I → Type v) [decidable_eq I] [Π (i : I), has_zero (f i)] (i : I) (x : f i) :
⇑(zero_hom.single f i) x = pi.single i x
source
@[simp]
theorem one_hom.single_apply {I : Type u} (f : I → Type v) [decidable_eq I] [Π (i : I), has_one (f i)] (i : I) (x : f i) :
⇑(one_hom.single f i) x = pi.mul_single i x
source
def monoid_hom.single {I : Type u} (f : I → Type v) [decidable_eq I] [Π (i : I), mul_one_class (f i)] (i : I) :
f i →* Π (i : I), f i

The monoid homomorphism including a single monoid into a dependent family of additive monoids, as functions supported at a point.

This is the monoid_hom version of pi.mul_single.

Equations
source
def add_monoid_hom.single {I : Type u} (f : I → Type v) [decidable_eq I] [Π (i : I), add_zero_class (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.

This is the add_monoid_hom version of pi.single.

Equations
source
@[simp]
theorem add_monoid_hom.single_apply {I : Type u} (f : I → Type v) [decidable_eq I] [Π (i : I), add_zero_class (f i)] (i : I) (x : f i) :
⇑(add_monoid_hom.single f i) x = pi.single i x
source
@[simp]
theorem monoid_hom.single_apply {I : Type u} (f : I → Type v) [decidable_eq I] [Π (i : I), mul_one_class (f i)] (i : I) (x : f i) :
⇑(monoid_hom.single f i) x = pi.mul_single i x
source
@[simp]
theorem mul_hom.single_apply {I : Type u} (f : I → Type v) [decidable_eq I] [Π (i : I), mul_zero_class (f i)] (i : I) (x : f i) (i_1 : I) :
⇑(mul_hom.single f i) x i_1 = pi.single i x i_1
source
def mul_hom.single {I : Type u} (f : I → Type v) [decidable_eq I] [Π (i : I), mul_zero_class (f i)] (i : I) :
f i →ₙ* Π (i : I), f i

The multiplicative homomorphism including a single mul_zero_class into a dependent family of mul_zero_classes, as functions supported at a point.

This is the mul_hom version of pi.single.

Equations
source
theorem pi.mul_single_mul {I : Type u} {f : I → Type v} [decidable_eq I] [Π (i : I), mul_one_class (f i)] (i : I) (x y : f i) :
pi.mul_single i (x * y) = (pi.mul_single i x) * pi.mul_single i y
source
theorem pi.single_add {I : Type u} {f : I → Type v} [decidable_eq I] [Π (i : I), add_zero_class (f i)] (i : I) (x y : f i) :
pi.single i (x + y) = pi.single i x + pi.single i y
source
theorem pi.single_neg {I : Type u} {f : I → Type v} [decidable_eq I] [Π (i : I), add_group (f i)] (i : I) (x : f i) :
pi.single i (-x) = -pi.single i x
source
theorem pi.mul_single_inv {I : Type u} {f : I → Type v} [decidable_eq I] [Π (i : I), group (f i)] (i : I) (x : f i) :
pi.mul_single i x⁻¹ = (pi.mul_single i x)⁻¹
source
theorem pi.single_div {I : Type u} {f : I → Type v} [decidable_eq I] [Π (i : I), group (f i)] (i : I) (x y : f i) :
pi.mul_single i (x / y) = pi.mul_single i x / pi.mul_single i y
source
theorem pi.single_sub {I : Type u} {f : I → Type v} [decidable_eq I] [Π (i : I), add_group (f i)] (i : I) (x y : f i) :
pi.single i (x - y) = pi.single i x - pi.single i y
source
theorem pi.single_mul {I : Type u} {f : I → Type v} [decidable_eq I] [Π (i : I), mul_zero_class (f i)] (i : I) (x y : f i) :
pi.single i (x * y) = (pi.single i x) * pi.single i y
source
theorem pi.mul_single_commute {I : Type u} {f : I → Type v} [decidable_eq I] [Π (i : I), mul_one_class (f i)] :
pairwise (λ (i j : I), ∀ (x : f i) (y : f j), commute (pi.mul_single i x) (pi.mul_single j y))

The injection into a pi group at different indices commutes.

For injections of commuting elements at the same index, see commute.map

source
theorem pi.single_commute {I : Type u} {f : I → Type v} [decidable_eq I] [Π (i : I), add_zero_class (f i)] :
pairwise (λ (i j : I), ∀ (x : f i) (y : f j), add_commute (pi.single i x) (pi.single j y))

The injection into an additive pi group at different indices commutes.

For injections of commuting elements at the same index, see add_commute.map

source
theorem pi.mul_single_apply_commute {I : Type u} {f : I → Type v} [decidable_eq I] [Π (i : I), mul_one_class (f i)] (x : Π (i : I), f i) (i j : I) :
commute (pi.mul_single i (x i)) (pi.mul_single j (x j))

The injection into a pi group with the same values commutes.

source
theorem pi.single_apply_commute {I : Type u} {f : I → Type v} [decidable_eq I] [Π (i : I), add_zero_class (f i)] (x : Π (i : I), f i) (i j : I) :
add_commute (pi.single i (x i)) (pi.single j (x j))

The injection into an additive pi group with the same values commutes.

source
theorem pi.update_eq_sub_add_single {I : Type u} {f : I → Type v} (i : I) [decidable_eq I] [Π (i : I), add_group (f i)] (g : Π (i : I), f i) (x : f i) :
function.update g i x = g - pi.single i (g i) + pi.single i x
source
theorem pi.update_eq_div_mul_single {I : Type u} {f : I → Type v} (i : I) [decidable_eq I] [Π (i : I), group (f i)] (g : Π (i : I), f i) (x : f i) :
function.update g i x = (g / pi.mul_single i (g i)) * pi.mul_single i x
source
@[simp]
theorem function.update_zero {I : Type u} {f : I → Type v} [Π (i : I), has_zero (f i)] [decidable_eq I] (i : I) :
function.update 0 i 0 = 0
source
@[simp]
theorem function.update_one {I : Type u} {f : I → Type v} [Π (i : I), has_one (f i)] [decidable_eq I] (i : I) :
function.update 1 i 1 = 1
source
theorem function.update_add {I : Type u} {f : I → Type v} [Π (i : I), has_add (f i)] [decidable_eq I] (f₁ f₂ : Π (i : I), f i) (i : I) (x₁ x₂ : f i) :
function.update (f₁ + f₂) i (x₁ + x₂) = function.update f₁ i x₁ + function.update f₂ i x₂
source
theorem function.update_mul {I : Type u} {f : I → Type v} [Π (i : I), has_mul (f i)] [decidable_eq I] (f₁ f₂ : Π (i : I), f i) (i : I) (x₁ x₂ : f i) :
function.update (f₁ * f₂) i (x₁ * x₂) = (function.update f₁ i x₁) * function.update f₂ i x₂
source
theorem function.update_inv {I : Type u} {f : I → Type v} [Π (i : I), has_inv (f i)] [decidable_eq I] (f₁ : Π (i : I), f i) (i : I) (x₁ : f i) :
function.update f₁⁻¹ i x₁⁻¹ = (function.update f₁ i x₁)⁻¹
source
theorem function.update_neg {I : Type u} {f : I → Type v} [Π (i : I), has_neg (f i)] [decidable_eq I] (f₁ : Π (i : I), f i) (i : I) (x₁ : f i) :
function.update (-f₁) i (-x₁) = -function.update f₁ i x₁
source
theorem function.update_sub {I : Type u} {f : I → Type v} [Π (i : I), has_sub (f i)] [decidable_eq I] (f₁ f₂ : Π (i : I), f i) (i : I) (x₁ x₂ : f i) :
function.update (f₁ - f₂) i (x₁ - x₂) = function.update f₁ i x₁ - function.update f₂ i x₂
source
theorem function.update_div {I : Type u} {f : I → Type v} [Π (i : I), has_div (f i)] [decidable_eq I] (f₁ f₂ : Π (i : I), f i) (i : I) (x₁ x₂ : f i) :
function.update (f₁ / f₂) i (x₁ / x₂) = function.update f₁ i x₁ / function.update f₂ i x₂
source
theorem set.piecewise_add {I : Type u} {f : I → Type v} [Π (i : I), has_add (f i)] (s : set I) [Π (i : I), decidable (i ∈ s)] (f₁ f₂ g₁ g₂ : Π (i : I), f i) :
s.piecewise (f₁ + f₂) (g₁ + g₂) = s.piecewise f₁ g₁ + s.piecewise f₂ g₂
source
theorem set.piecewise_mul {I : Type u} {f : I → Type v} [Π (i : I), has_mul (f i)] (s : set I) [Π (i : I), decidable (i ∈ s)] (f₁ f₂ g₁ g₂ : Π (i : I), f i) :
s.piecewise (f₁ * f₂) (g₁ * g₂) = (s.piecewise f₁ g₁) * s.piecewise f₂ g₂
source
theorem set.piecewise_inv {I : Type u} {f : I → Type v} [Π (i : I), has_inv (f i)] (s : set I) [Π (i : I), decidable (i ∈ s)] (f₁ g₁ : Π (i : I), f i) :
s.piecewise f₁⁻¹ g₁⁻¹ = (s.piecewise f₁ g₁)⁻¹
source
theorem set.piecewise_neg {I : Type u} {f : I → Type v} [Π (i : I), has_neg (f i)] (s : set I) [Π (i : I), decidable (i ∈ s)] (f₁ g₁ : Π (i : I), f i) :
s.piecewise (-f₁) (-g₁) = -s.piecewise f₁ g₁
source
theorem set.piecewise_div {I : Type u} {f : I → Type v} [Π (i : I), has_div (f i)] (s : set I) [Π (i : I), decidable (i ∈ s)] (f₁ f₂ g₁ g₂ : Π (i : I), f i) :
s.piecewise (f₁ / f₂) (g₁ / g₂) = s.piecewise f₁ g₁ / s.piecewise f₂ g₂
source
theorem set.piecewise_sub {I : Type u} {f : I → Type v} [Π (i : I), has_sub (f i)] (s : set I) [Π (i : I), decidable (i ∈ s)] (f₁ f₂ g₁ g₂ : Π (i : I), f i) :
s.piecewise (f₁ - f₂) (g₁ - g₂) = s.piecewise f₁ g₁ - s.piecewise f₂ g₂
source
@[simp]
theorem function.extend_by_one.hom_apply {ι : Type u} {η : Type v} (R : Type w) (s : ι → η) [mul_one_class R] (f : ι → R) (ᾰ : η) :
⇑(function.extend_by_one.hom R s) f ᾰ = function.extend s f 1 ᾰ
source
noncomputable def function.extend_by_zero.hom {ι : Type u} {η : Type v} (R : Type w) (s : ι → η) [add_zero_class R] :
(ι → R) →+ η → R

function.extend s f 0 as a bundled hom.

Equations
source
@[simp]
theorem function.extend_by_zero.hom_apply {ι : Type u} {η : Type v} (R : Type w) (s : ι → η) [add_zero_class R] (f : ι → R) (ᾰ : η) :
⇑(function.extend_by_zero.hom R s) f ᾰ = function.extend s f 0 ᾰ
source
noncomputable def function.extend_by_one.hom {ι : Type u} {η : Type v} (R : Type w) (s : ι → η) [mul_one_class R] :
(ι → R) →* η → R

function.extend s f 1 as a bundled hom.

Equations