Translation operator

This file defines the translation of a function from a group by an element of that group.

Notation

τ a f is notation for translate a f.

See also

Generally, translation is the same as acting on the domain by subtraction. This setting is abstracted by DomAddAct in such a way that τ a f = DomAddAct.mk (-a) +ᵥ f (see translate_eq_domAddActMk_vadd). Using DomAddAct is irritating in applications because of this negation appearing inside DomAddAct.mk. Although mathematically equivalent, the pen and paper convention is that translating is an action by subtraction, not by addition.

def translate {α : Type u_2} {G : Type u_5} [AddCommGroup G] (a : G) (f : G → α) : G → α

Translation of a function in a group by an element of that group. τ a f is defined as x ↦ f (x - a).

Equations

• translate a f x = f (x - a)

def translate.termτ : Lean.ParserDescr

Translation of a function in a group by an element of that group. τ a f is defined as x ↦ f (x - a).

Equations

• translate.termτ = Lean.ParserDescr.node `translate.termτ 1024 (Lean.ParserDescr.symbol "τ ")

@[simp]

theorem translate_apply {α : Type u_2} {G : Type u_5} [AddCommGroup G] (a : G) (f : G → α) (x : G) : translate a f x = f (x - a)

@[simp]

theorem translate_zero {α : Type u_2} {G : Type u_5} [AddCommGroup G] (f : G → α) : translate 0 f = f

theorem translate_translate {α : Type u_2} {G : Type u_5} [AddCommGroup G] (a b : G) (f : G → α) : translate a (translate b f) = translate (a + b) f

theorem translate_add {α : Type u_2} {G : Type u_5} [AddCommGroup G] (a b : G) (f : G → α) : translate (a + b) f = translate a (translate b f)

theorem translate_add' {α : Type u_2} {G : Type u_5} [AddCommGroup G] (a b : G) (f : G → α) : translate (a + b) f = translate b (translate a f)

See translate_add

theorem translate_comm {α : Type u_2} {G : Type u_5} [AddCommGroup G] (a b : G) (f : G → α) : translate a (translate b f) = translate b (translate a f)

@[simp]

theorem comp_translate {α : Type u_2} {β : Type u_3} {G : Type u_5} [AddCommGroup G] (a : G) (f : G → α) (g : α → β) : g ∘ translate a f = translate a (g ∘ f)

theorem translate_eq_domAddActMk_vadd {α : Type u_2} {G : Type u_5} [AddCommGroup G] (a : G) (f : G → α) : translate a f = DomAddAct.mk (-a) +ᵥ f

@[simp]

theorem translate_smul_right {α : Type u_2} {G : Type u_5} {H : Type u_6} [AddCommGroup G] [SMul H α] (a : G) (f : G → α) (c : H) : translate a (c • f) = c • translate a f

@[simp]

theorem translate_zero_right {α : Type u_2} {G : Type u_5} [AddCommGroup G] [Zero α] (a : G) : translate a 0 = 0

theorem translate_add_right {α : Type u_2} {G : Type u_5} [AddCommGroup G] [Add α] (a : G) (f g : G → α) : translate a (f + g) = translate a f + translate a g

theorem translate_sub_right {α : Type u_2} {G : Type u_5} [AddCommGroup G] [Sub α] (a : G) (f g : G → α) : translate a (f - g) = translate a f - translate a g

theorem translate_neg_right {α : Type u_2} {G : Type u_5} [AddCommGroup G] [Neg α] (a : G) (f : G → α) : translate a (-f) = -translate a f

theorem translate_sum_right {ι : Type u_1} {M : Type u_4} {G : Type u_5} [AddCommGroup G] [AddCommMonoid M] (a : G) (f : ι → G → M) (s : Finset ι) : translate a (∑ i ∈ s, f i) = ∑ i ∈ s, translate a (f i)

theorem sum_translate {M : Type u_4} {G : Type u_5} [AddCommGroup G] [AddCommMonoid M] [Fintype G] (a : G) (f : G → M) : ∑ b : G, translate a f b = ∑ b : G, f b

@[simp]

theorem support_translate {G : Type u_5} {H : Type u_6} [AddCommGroup G] [AddCommGroup H] (a : G) (f : G → H) : Function.support (translate a f) = a +ᵥ Function.support f

theorem translate_prod_right {ι : Type u_1} {M : Type u_4} {G : Type u_5} [AddCommGroup G] [CommMonoid M] (a : G) (f : ι → G → M) (s : Finset ι) : translate a (∏ i ∈ s, f i) = ∏ i ∈ s, translate a (f i)