Documentation

Mathlib.Algebra.Notation.Pi.Basic

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_6} [(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
Instances For
    source
    def Pi.single {ι : Type u_1} {M : ι → Type u_6} [(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
    Instances For
      source
      @[simp]
      theorem Pi.mulSingle_eq_same {ι : Type u_1} {M : ι → Type u_6} [(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_6} [(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_6} [(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_6} [(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_6} [(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_6} [(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_6} [(i : ι) → One (M i)] [DecidableEq ι] (i : ι) :
      mulSingle i 1 = 1
      source
      @[simp]
      theorem Pi.single_zero {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → Zero (M i)] [DecidableEq ι] (i : ι) :
      single i 0 = 0
      source
      @[simp]
      theorem Pi.mulSingle_eq_one_iff {ι : Type u_1} {M : ι → Type u_6} [(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_6} [(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_6} [(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_6} [(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_6} {N : ι → Type u_7} [(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_6} {N : ι → Type u_7} [(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_6} {N : ι → Type u_7} {O : ι → Type u_8} [(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_6} {N : ι → Type u_7} {O : ι → Type u_8} [(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_6} {N : ι → Type u_7} [(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_6} {N : ι → Type u_7} [(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_6} {N : ι → Type u_7} {O : ι → Type u_8} [(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_6} {N : ι → Type u_7} {O : ι → Type u_8} [(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_6} [(i : ι) → One (M i)] [DecidableEq ι] (i : ι) :
      Function.Injective (mulSingle i)
      source
      theorem Pi.single_injective {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → Zero (M i)] [DecidableEq ι] (i : ι) :
      Function.Injective (single i)
      source
      @[simp]
      theorem Pi.mulSingle_inj {ι : Type u_1} {M : ι → Type u_6} [(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_6} [(i : ι) → Zero (M i)] [DecidableEq ι] (i : ι) {x y : M i} :
      single i x = single i y ↔ x = y
      source
      theorem Pi.mulSingle_congr {ι : Type u_1} [DecidableEq ι] {M : Type u_9} [One M] {i₁ i₂ : ι} (hi : i₁ = i₂) {x₁ x₂ : M} (hx : x₁ = x₂) {j₁ j₂ : ι} (hj : j₁ = j₂) :
      mulSingle i₁ x₁ j₁ = mulSingle i₂ x₂ j₂

      A congruence lemma for Pi.mulSingle, specialized for the non-dependent case. Without this, simp can't rewrite in the first and third argument (i and j) because of dependence. See also https://github.com/leanprover/lean4/issues/12478.

      source
      theorem Pi.single_congr {ι : Type u_1} [DecidableEq ι] {M : Type u_9} [Zero M] {i₁ i₂ : ι} (hi : i₁ = i₂) {x₁ x₂ : M} (hx : x₁ = x₂) {j₁ j₂ : ι} (hj : j₁ = j₂) :
      single i₁ x₁ j₁ = single i₂ x₂ j₂

      A congruence lemma for Pi.single, specialized for the non-dependent case. Without this, simp can't rewrite in the first and third argument (i and j) because of dependence. See also https://github.com/leanprover/lean4/issues/12478.

      source
      theorem Pi.mulSingle_apply {ι : Type u_1} [DecidableEq ι] {M : Type u_9} [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_9} [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_9} [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_9} [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.

      source
      @[simp]
      theorem Pi.curry_mulSingle {ι : Type u_1} {ι' : Type u_2} [DecidableEq ι] {M : Type u_9} [One M] [DecidableEq ι'] (i : ι × ι') (b : M) :
      Function.curry (mulSingle i b) = mulSingle i.fst (mulSingle i.snd b)
      source
      @[simp]
      theorem Pi.curry_single {ι : Type u_1} {ι' : Type u_2} [DecidableEq ι] {M : Type u_9} [Zero M] [DecidableEq ι'] (i : ι × ι') (b : M) :
      Function.curry (single i b) = single i.fst (single i.snd b)
      source
      @[simp]
      theorem Pi.uncurry_mulSingle_mulSingle {ι : Type u_1} {ι' : Type u_2} [DecidableEq ι] {M : Type u_9} [One M] [DecidableEq ι'] (i : ι) (i' : ι') (b : M) :
      Function.uncurry (mulSingle i (mulSingle i' b)) = mulSingle (i, i') b
      source
      @[simp]
      theorem Pi.uncurry_single_single {ι : Type u_1} {ι' : Type u_2} [DecidableEq ι] {M : Type u_9} [Zero M] [DecidableEq ι'] (i : ι) (i' : ι') (b : M) :
      Function.uncurry (single i (single i' b)) = single (i, i') b