Very basic algebraic operations on pi types #

This file provides very basic algebraic operations on functions.

source

def Pi.mulSingle {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → One (M i)] [DecidableEq ι] (i : ι) (x : M i) (j : ι) :

M j

The function supported at i, with value x there, and 1 elsewhere.

Equations

Pi.mulSingle i x = Function.update 1 i x

Instances For

source

def Pi.single {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → Zero (M i)] [DecidableEq ι] (i : ι) (x : M i) (j : ι) :

M j

The function supported at i, with value x there, and 0 elsewhere.

Equations

Pi.single i x = Function.update 0 i x

Instances For

source

@[simp]

theorem Pi.mulSingle_eq_same {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → One (M i)] [DecidableEq ι] (i : ι) (x : M i) :

mulSingle i x i = x

source

@[simp]

theorem Pi.single_eq_same {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → Zero (M i)] [DecidableEq ι] (i : ι) (x : M i) :

single i x i = x

source

@[simp]

theorem Pi.mulSingle_eq_of_ne {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → One (M i)] [DecidableEq ι] {i i' : ι} (h : i' ≠ i) (x : M i) :

mulSingle i x i' = 1

source

@[simp]

theorem Pi.single_eq_of_ne {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → Zero (M i)] [DecidableEq ι] {i i' : ι} (h : i' ≠ i) (x : M i) :

single i x i' = 0

source

@[simp]

theorem Pi.mulSingle_eq_of_ne' {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → One (M i)] [DecidableEq ι] {i i' : ι} (h : i ≠ i') (x : M i) :

mulSingle i x i' = 1

Abbreviation for mulSingle_eq_of_ne h.symm, for ease of use by simp.

source

@[simp]

theorem Pi.single_eq_of_ne' {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → Zero (M i)] [DecidableEq ι] {i i' : ι} (h : i ≠ i') (x : M i) :

single i x i' = 0

Abbreviation for single_eq_of_ne h.symm, for ease of use by simp.

source

@[simp]

theorem Pi.mulSingle_one {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → One (M i)] [DecidableEq ι] (i : ι) :

mulSingle i 1 = 1

source

@[simp]

theorem Pi.single_zero {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → Zero (M i)] [DecidableEq ι] (i : ι) :

single i 0 = 0

source

@[simp]

theorem Pi.mulSingle_eq_one_iff {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → One (M i)] [DecidableEq ι] {i : ι} {x : M i} :

mulSingle i x = 1 ↔ x = 1

source

@[simp]

theorem Pi.single_eq_zero_iff {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → Zero (M i)] [DecidableEq ι] {i : ι} {x : M i} :

single i x = 0 ↔ x = 0

source

theorem Pi.mulSingle_ne_one_iff {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → One (M i)] [DecidableEq ι] {i : ι} {x : M i} :

mulSingle i x ≠ 1 ↔ x ≠ 1

source

theorem Pi.single_ne_zero_iff {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → Zero (M i)] [DecidableEq ι] {i : ι} {x : M i} :

single i x ≠ 0 ↔ x ≠ 0

source

theorem Pi.apply_mulSingle {ι : Type u_1} {M : ι → Type u_5} {N : ι → Type u_6} [(i : ι) → One (M i)] [(i : ι) → One (N i)] [DecidableEq ι] (f' : (i : ι) → M i → N i) (hf' : ∀ (i : ι), f' i 1 = 1) (i : ι) (x : M i) (j : ι) :

f' j (mulSingle i x j) = mulSingle i (f' i x) j

source

theorem Pi.apply_single {ι : Type u_1} {M : ι → Type u_5} {N : ι → Type u_6} [(i : ι) → Zero (M i)] [(i : ι) → Zero (N i)] [DecidableEq ι] (f' : (i : ι) → M i → N i) (hf' : ∀ (i : ι), f' i 0 = 0) (i : ι) (x : M i) (j : ι) :

f' j (single i x j) = single i (f' i x) j

source

theorem Pi.apply_mulSingle₂ {ι : Type u_1} {M : ι → Type u_5} {N : ι → Type u_6} {O : ι → Type u_7} [(i : ι) → One (M i)] [(i : ι) → One (N i)] [(i : ι) → One (O i)] [DecidableEq ι] (f' : (i : ι) → M i → N i → O i) (hf' : ∀ (i : ι), f' i 1 1 = 1) (i : ι) (x : M i) (y : N i) (j : ι) :

f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j

source

theorem Pi.apply_single₂ {ι : Type u_1} {M : ι → Type u_5} {N : ι → Type u_6} {O : ι → Type u_7} [(i : ι) → Zero (M i)] [(i : ι) → Zero (N i)] [(i : ι) → Zero (O i)] [DecidableEq ι] (f' : (i : ι) → M i → N i → O i) (hf' : ∀ (i : ι), f' i 0 0 = 0) (i : ι) (x : M i) (y : N i) (j : ι) :

f' j (single i x j) (single i y j) = single i (f' i x y) j

source

theorem Pi.mulSingle_op {ι : Type u_1} {M : ι → Type u_5} {N : ι → Type u_6} [(i : ι) → One (M i)] [(i : ι) → One (N i)] [DecidableEq ι] (op : (i : ι) → M i → N i) (h : ∀ (i : ι), op i 1 = 1) (i : ι) (x : M i) :

mulSingle i (op i x) = fun (j : ι) => op j (mulSingle i x j)

source

theorem Pi.single_op {ι : Type u_1} {M : ι → Type u_5} {N : ι → Type u_6} [(i : ι) → Zero (M i)] [(i : ι) → Zero (N i)] [DecidableEq ι] (op : (i : ι) → M i → N i) (h : ∀ (i : ι), op i 0 = 0) (i : ι) (x : M i) :

single i (op i x) = fun (j : ι) => op j (single i x j)

source

theorem Pi.mulSingle_op₂ {ι : Type u_1} {M : ι → Type u_5} {N : ι → Type u_6} {O : ι → Type u_7} [(i : ι) → One (M i)] [(i : ι) → One (N i)] [(i : ι) → One (O i)] [DecidableEq ι] (op : (i : ι) → M i → N i → O i) (h : ∀ (i : ι), op i 1 1 = 1) (i : ι) (x : M i) (y : N i) :

mulSingle i (op i x y) = fun (j : ι) => op j (mulSingle i x j) (mulSingle i y j)

source

theorem Pi.single_op₂ {ι : Type u_1} {M : ι → Type u_5} {N : ι → Type u_6} {O : ι → Type u_7} [(i : ι) → Zero (M i)] [(i : ι) → Zero (N i)] [(i : ι) → Zero (O i)] [DecidableEq ι] (op : (i : ι) → M i → N i → O i) (h : ∀ (i : ι), op i 0 0 = 0) (i : ι) (x : M i) (y : N i) :

single i (op i x y) = fun (j : ι) => op j (single i x j) (single i y j)

source

theorem Pi.mulSingle_injective {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → One (M i)] [DecidableEq ι] (i : ι) :

Function.Injective (mulSingle i)

source

theorem Pi.single_injective {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → Zero (M i)] [DecidableEq ι] (i : ι) :

Function.Injective (single i)

source

@[simp]

theorem Pi.mulSingle_inj {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → One (M i)] [DecidableEq ι] (i : ι) {x y : M i} :

mulSingle i x = mulSingle i y ↔ x = y

source

@[simp]

theorem Pi.single_inj {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → Zero (M i)] [DecidableEq ι] (i : ι) {x y : M i} :

single i x = single i y ↔ x = y

source

theorem Pi.mulSingle_apply {ι : Type u_1} [DecidableEq ι] {M : Type u_8} [One M] (i : ι) (x : M) (i' : ι) :

mulSingle i x i' = if i' = i then x else 1

On non-dependent functions, Pi.mulSingle can be expressed as an ite

source

theorem Pi.single_apply {ι : Type u_1} [DecidableEq ι] {M : Type u_8} [Zero M] (i : ι) (x : M) (i' : ι) :

single i x i' = if i' = i then x else 0

On non-dependent functions, Pi.single can be expressed as an ite

source

theorem Pi.mulSingle_comm {ι : Type u_1} [DecidableEq ι] {M : Type u_8} [One M] (i : ι) (x : M) (j : ι) :

mulSingle i x j = mulSingle j x i

On non-dependent functions, Pi.mulSingle is symmetric in the two indices.

source

theorem Pi.single_comm {ι : Type u_1} [DecidableEq ι] {M : Type u_8} [Zero M] (i : ι) (x : M) (j : ι) :

single i x j = single j x i

On non-dependent functions, Pi.single is symmetric in the two indices.

Documentation

Mathlib.Algebra.Notation.Pi.Basic

Very basic algebraic operations on pi types #