Maps (semi)conjugating a shift to a shift #

Denote by $S^1$ the unit circle UnitAddCircle. A common way to study a self-map $f\colon S^1\to S^1$ of degree 1 is to lift it to a map $\tilde f\colon \mathbb R\to \mathbb R$ such that $\tilde f(x + 1) = \tilde f(x)+1$ for all x.

In this file we define a structure and a typeclass for bundled maps satisfying f (x + a) = f x + b.

We use parameters a and b instead of 1 to accommodate for two use cases:

maps between circles of different lengths;
self-maps $f\colon S^1\to S^1$ of degree other than one, including orientation-reversing maps.

source

structure AddConstMap (G : Type u_1) (H : Type u_2) [Add G] [Add H] (a : G) (b : H) :

Type (max u_1 u_2)

A bundled map f : G → H such that f (x + a) = f x + b for all x.

One can think about f as a lift to G of a map between two AddCircles.

toFun : G → H
The underlying function of an AddConstMap. Use automatic coercion to function instead.
map_add_const' (x : G) : self.toFun (x + a) = self.toFun x + b
An AddConstMap satisfies f (x + a) = f x + b. Use map_add_const instead.

Instances For

source

def AddConstMap.«term_→+c[_,_]_» :

Lean.TrailingParserDescr

A bundled map f : G → H such that f (x + a) = f x + b for all x.

One can think about f as a lift to G of a map between two AddCircles.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

class AddConstMapClass (F : Type u_1) (G : outParam (Type u_2)) (H : outParam (Type u_3)) [Add G] [Add H] (a : outParam G) (b : outParam H) [FunLike F G H] :

Prop

Typeclass for maps satisfying f (x + a) = f x + b.

Note that a and b are outParams, so one should not add instances like [AddConstMapClass F G H a b] : AddConstMapClass F G H (-a) (-b).

map_add_const (f : F) (x : G) : f (x + a) = f x + b
A map of AddConstMapClass class semiconjugates shift by a to the shift by b: ∀ x, f (x + a) = f x + b.

Instances

Properties of `AddConstMapClass` maps #

In this section we prove properties like f (x + n • a) = f x + n • b.

source

theorem AddConstMapClass.semiconj {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [Add G] [Add H] [AddConstMapClass F G H a b] (f : F) :

Function.Semiconj (⇑f) (fun (x : G) => x + a) fun (x : H) => x + b

source

theorem AddConstMapClass.map_add_nsmul {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddMonoid G] [AddMonoid H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℕ) :

f (x + n • a) = f x + n • b

source

theorem AddConstMapClass.map_add_nat' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℕ) :

f (x + ↑n) = f x + n • b

source

theorem AddConstMapClass.map_add_one {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddMonoidWithOne G] [Add H] [AddConstMapClass F G H 1 b] (f : F) (x : G) :

f (x + 1) = f x + b

source

theorem AddConstMapClass.map_add_ofNat' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℕ) [n.AtLeastTwo] :

f (x + OfNat.ofNat n) = f x + OfNat.ofNat n • b

source

theorem AddConstMapClass.map_add_nat {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ℕ) :

f (x + ↑n) = f x + ↑n

source

theorem AddConstMapClass.map_add_ofNat {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ℕ) [n.AtLeastTwo] :

f (x + OfNat.ofNat n) = f x + OfNat.ofNat n

source

theorem AddConstMapClass.map_const {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddZeroClass G] [Add H] [AddConstMapClass F G H a b] (f : F) :

f a = f 0 + b

source

theorem AddConstMapClass.map_one {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddZeroClass G] [One G] [Add H] [AddConstMapClass F G H 1 b] (f : F) :

f 1 = f 0 + b

source

theorem AddConstMapClass.map_nsmul_const {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddMonoid G] [AddMonoid H] [AddConstMapClass F G H a b] (f : F) (n : ℕ) :

f (n • a) = f 0 + n • b

source

theorem AddConstMapClass.map_nat' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ℕ) :

f ↑n = f 0 + n • b

source

theorem AddConstMapClass.map_ofNat' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ℕ) [n.AtLeastTwo] :

f (OfNat.ofNat n) = f 0 + OfNat.ofNat n • b

source

theorem AddConstMapClass.map_nat {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℕ) :

f ↑n = f 0 + ↑n

source

theorem AddConstMapClass.map_ofNat {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℕ) [n.AtLeastTwo] :

f (OfNat.ofNat n) = f 0 + OfNat.ofNat n

source

theorem AddConstMapClass.map_const_add {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddCommSemigroup G] [Add H] [AddConstMapClass F G H a b] (f : F) (x : G) :

f (a + x) = f x + b

source

theorem AddConstMapClass.map_one_add {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddCommMonoidWithOne G] [Add H] [AddConstMapClass F G H 1 b] (f : F) (x : G) :

f (1 + x) = f x + b

source

theorem AddConstMapClass.map_nsmul_add {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddCommMonoid G] [AddMonoid H] [AddConstMapClass F G H a b] (f : F) (n : ℕ) (x : G) :

f (n • a + x) = f x + n • b

source

theorem AddConstMapClass.map_nat_add' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddCommMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ℕ) (x : G) :

f (↑n + x) = f x + n • b

source

theorem AddConstMapClass.map_ofNat_add' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddCommMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ℕ) [n.AtLeastTwo] (x : G) :

f (OfNat.ofNat n + x) = f x + OfNat.ofNat n • b

source

theorem AddConstMapClass.map_nat_add {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddCommMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℕ) (x : G) :

f (↑n + x) = f x + ↑n

source

theorem AddConstMapClass.map_ofNat_add {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddCommMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℕ) [n.AtLeastTwo] (x : G) :

f (OfNat.ofNat n + x) = f x + OfNat.ofNat n

source

theorem AddConstMapClass.map_sub_nsmul {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℕ) :

f (x - n • a) = f x - n • b

source

theorem AddConstMapClass.map_sub_const {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) :

f (x - a) = f x - b

source

theorem AddConstMapClass.map_sub_one {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddGroup G] [One G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) :

f (x - 1) = f x - b

source

theorem AddConstMapClass.map_sub_nat' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℕ) :

f (x - ↑n) = f x - n • b

source

theorem AddConstMapClass.map_sub_ofNat' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℕ) [n.AtLeastTwo] :

f (x - OfNat.ofNat n) = f x - OfNat.ofNat n • b

source

theorem AddConstMapClass.map_add_zsmul {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℤ) :

f (x + n • a) = f x + n • b

source

theorem AddConstMapClass.map_zsmul_const {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (n : ℤ) :

f (n • a) = f 0 + n • b

source

theorem AddConstMapClass.map_add_int' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℤ) :

f (x + ↑n) = f x + n • b

source

theorem AddConstMapClass.map_add_int {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddGroupWithOne G] [AddGroupWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ℤ) :

f (x + ↑n) = f x + ↑n

source

theorem AddConstMapClass.map_sub_zsmul {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℤ) :

f (x - n • a) = f x - n • b

source

theorem AddConstMapClass.map_sub_int' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℤ) :

f (x - ↑n) = f x - n • b

source

theorem AddConstMapClass.map_sub_int {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddGroupWithOne G] [AddGroupWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ℤ) :

f (x - ↑n) = f x - ↑n

source

theorem AddConstMapClass.map_zsmul_add {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddCommGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (n : ℤ) (x : G) :

f (n • a + x) = f x + n • b

source

theorem AddConstMapClass.map_int_add' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddCommGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (n : ℤ) (x : G) :

f (↑n + x) = f x + n • b

source

theorem AddConstMapClass.map_int_add {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddCommGroupWithOne G] [AddGroupWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℤ) (x : G) :

f (↑n + x) = f x + ↑n

source

theorem AddConstMapClass.map_fract {F : Type u_1} {H : Type u_3} {b : H} {R : Type u_4} [LinearOrderedRing R] [FloorRing R] [AddGroup H] [FunLike F R H] [AddConstMapClass F R H 1 b] (f : F) (x : R) :

f (Int.fract x) = f x - ⌊x⌋ • b

source

theorem AddConstMapClass.rel_map_of_Icc {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [LinearOrderedAddCommGroup G] [Archimedean G] [AddGroup H] [AddConstMapClass F G H a b] {f : F} {R : H → H → Prop} [IsTrans H R] [hR : CovariantClass H H (fun (x y : H) => y + x) R] (ha : 0 < a) {l : G} (hf : ∀ x ∈ Set.Icc l (l + a), ∀ y ∈ Set.Icc l (l + a), x < y → R (f x) (f y)) :

((fun (x1 x2 : G) => x1 < x2) ⇒ R) ⇑f ⇑f

Auxiliary lemmas for the "monotonicity on a fundamental interval implies monotonicity" lemmas. We formulate it for any relation so that the proof works both for Monotone and StrictMono.

source

theorem AddConstMapClass.monotone_iff_Icc {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [LinearOrderedAddCommGroup G] [Archimedean G] [OrderedAddCommGroup H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) :

Monotone ⇑f ↔ MonotoneOn (⇑f) (Set.Icc l (l + a))

source

theorem AddConstMapClass.antitone_iff_Icc {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [LinearOrderedAddCommGroup G] [Archimedean G] [OrderedAddCommGroup H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) :

Antitone ⇑f ↔ AntitoneOn (⇑f) (Set.Icc l (l + a))

source

theorem AddConstMapClass.strictMono_iff_Icc {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [LinearOrderedAddCommGroup G] [Archimedean G] [OrderedAddCommGroup H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) :

StrictMono ⇑f ↔ StrictMonoOn (⇑f) (Set.Icc l (l + a))

source

theorem AddConstMapClass.strictAnti_iff_Icc {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [LinearOrderedAddCommGroup G] [Archimedean G] [OrderedAddCommGroup H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) :

StrictAnti ⇑f ↔ StrictAntiOn (⇑f) (Set.Icc l (l + a))

Coercion to function #

source

instance AddConstMap.instFunLike {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} :

FunLike (AddConstMap G H a b) G H

Equations

AddConstMap.instFunLike = { coe := AddConstMap.toFun, coe_injective' := ⋯ }

source

@[simp]

theorem AddConstMap.coe_mk {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (f : G → H) (hf : ∀ (x : G), f (x + a) = f x + b) :

⇑{ toFun := f, map_add_const' := hf } = f

source

@[simp]

theorem AddConstMap.mk_coe {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (f : AddConstMap G H a b) :

{ toFun := ⇑f, map_add_const' := ⋯ } = f

source

@[simp]

theorem AddConstMap.toFun_eq_coe {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (f : AddConstMap G H a b) :

f.toFun = ⇑f

source

instance AddConstMap.instAddConstMapClass {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} :

AddConstMapClass (AddConstMap G H a b) G H a b

source

theorem AddConstMap.ext {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {f g : AddConstMap G H a b} (h : ∀ (x : G), f x = g x) :

f = g

Constructions about `G →+c[a, b] H` #

source

def AddConstMap.id {G : Type u_1} [Add G] {a : G} :

AddConstMap G G a a

The identity map as G →+c[a, a] G.

Equations

AddConstMap.id = { toFun := id, map_add_const' := ⋯ }

Instances For

source

@[simp]

theorem AddConstMap.coe_id {G : Type u_1} [Add G] {a : G} :

⇑AddConstMap.id = id

source

instance AddConstMap.instInhabited {G : Type u_1} [Add G] {a : G} :

Inhabited (AddConstMap G G a a)

Equations

AddConstMap.instInhabited = { default := AddConstMap.id }

source

def AddConstMap.comp {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {K : Type u_3} [Add K] {c : K} (g : AddConstMap H K b c) (f : AddConstMap G H a b) :

AddConstMap G K a c

Composition of two AddConstMaps.

Equations

g.comp f = { toFun := ⇑g ∘ ⇑f, map_add_const' := ⋯ }

Instances For

source

@[simp]

theorem AddConstMap.coe_comp {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {K : Type u_3} [Add K] {c : K} (g : AddConstMap H K b c) (f : AddConstMap G H a b) :

⇑(g.comp f) = ⇑g ∘ ⇑f

source

@[simp]

theorem AddConstMap.comp_id {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (f : AddConstMap G H a b) :

f.comp AddConstMap.id = f

source

@[simp]

theorem AddConstMap.id_comp {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (f : AddConstMap G H a b) :

AddConstMap.id.comp f = f

source

def AddConstMap.replaceConsts {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (f : AddConstMap G H a b) (a' : G) (b' : H) (ha : a = a') (hb : b = b') :

AddConstMap G H a' b'

Change constants a and b in (f : G →+c[a, b] H) to improve definitional equalities.

Equations

f.replaceConsts a' b' ha hb = { toFun := ⇑f, map_add_const' := ⋯ }

Instances For

source

@[simp]

theorem AddConstMap.coe_replaceConsts {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (f : AddConstMap G H a b) (a' : G) (b' : H) (ha : a = a') (hb : b = b') :

⇑(f.replaceConsts a' b' ha hb) = ⇑f

Additive action on `G →+c[a, b] H` #

source

instance AddConstMap.instVAddOfVAddAssocClass {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {K : Type u_3} [VAdd K H] [VAddAssocClass K H H] :

VAdd K (AddConstMap G H a b)

If f is an AddConstMap, then so is (c +ᵥ f ·).

Equations

AddConstMap.instVAddOfVAddAssocClass = { vadd := fun (c : K) (f : AddConstMap G H a b) => { toFun := c +ᵥ ⇑f, map_add_const' := ⋯ } }

source

@[simp]

theorem AddConstMap.coe_vadd {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {K : Type u_3} [VAdd K H] [VAddAssocClass K H H] (c : K) (f : AddConstMap G H a b) :

⇑(c +ᵥ f) = c +ᵥ ⇑f

source

instance AddConstMap.instAddActionOfVAddAssocClass {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {K : Type u_3} [AddMonoid K] [AddAction K H] [VAddAssocClass K H H] :

AddAction K (AddConstMap G H a b)

Equations

AddConstMap.instAddActionOfVAddAssocClass = Function.Injective.addAction (fun (f : AddConstMap G H a b) => ⇑f) ⋯ ⋯

Monoid structure on endomorphisms `G →+c[a, a] G` #

source

instance AddConstMap.instMul {G : Type u_1} [Add G] {a : G} :

Mul (AddConstMap G G a a)

Equations

AddConstMap.instMul = { mul := AddConstMap.comp }

source

instance AddConstMap.instOne {G : Type u_1} [Add G] {a : G} :

One (AddConstMap G G a a)

Equations

AddConstMap.instOne = { one := AddConstMap.id }

source

instance AddConstMap.instPowNat {G : Type u_1} [Add G] {a : G} :

Pow (AddConstMap G G a a) ℕ

Equations

AddConstMap.instPowNat = { pow := fun (f : AddConstMap G G a a) (n : ℕ) => { toFun := (⇑f)^[n], map_add_const' := ⋯ } }

source

instance AddConstMap.instMonoid {G : Type u_1} [Add G] {a : G} :

Monoid (AddConstMap G G a a)

Equations

AddConstMap.instMonoid = Function.Injective.monoid (fun (f : AddConstMap G G a a) => ⇑f) ⋯ ⋯ ⋯ ⋯

source

theorem AddConstMap.mul_def {G : Type u_1} [Add G] {a : G} (f g : AddConstMap G G a a) :

f * g = f.comp g

source

@[simp]

theorem AddConstMap.coe_mul {G : Type u_1} [Add G] {a : G} (f g : AddConstMap G G a a) :

⇑(f * g) = ⇑f ∘ ⇑g

source

theorem AddConstMap.one_def {G : Type u_1} [Add G] {a : G} :

1 = AddConstMap.id

source

@[simp]

theorem AddConstMap.coe_one {G : Type u_1} [Add G] {a : G} :

⇑1 = id

source

@[simp]

theorem AddConstMap.coe_pow {G : Type u_1} [Add G] {a : G} (f : AddConstMap G G a a) (n : ℕ) :

⇑(f ^ n) = (⇑f)^[n]

source

theorem AddConstMap.pow_apply {G : Type u_1} [Add G] {a : G} (f : AddConstMap G G a a) (n : ℕ) (x : G) :

(f ^ n) x = (⇑f)^[n] x

source

def AddConstMap.toEnd {G : Type u_1} [Add G] {a : G} :

AddConstMap G G a a →* Function.End G

Coercion to functions as a monoid homomorphism to Function.End G.

Equations

AddConstMap.toEnd = { toFun := DFunLike.coe, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem AddConstMap.toEnd_apply {G : Type u_1} [Add G] {a : G} :

⇑AddConstMap.toEnd = DFunLike.coe

Multiplicative action on `(b : H) × (G →+c[a, b] H)` #

If K acts distributively on H, then for each f : G →+c[a, b] H we define (AddConstMap.smul c f : G →+c[a, c • b] H).

One can show that this defines a multiplicative action of K on (b : H) × (G →+c[a, b] H) but we don't do this at the moment because we don't need this.

source

def AddConstMap.smul {G : Type u_1} {H : Type u_2} {K : Type u_3} [Add G] [AddZeroClass H] {a : G} {b : H} [DistribSMul K H] (c : K) (f : AddConstMap G H a b) :

AddConstMap G H a (c • b)

Pointwise scalar multiplication of f : G →+c[a, b] H as a map G →+c[a, c • b] H.

Equations

AddConstMap.smul c f = { toFun := c • ⇑f, map_add_const' := ⋯ }

Instances For

source

@[simp]

theorem AddConstMap.coe_smul {G : Type u_1} {H : Type u_2} {K : Type u_3} [Add G] [AddZeroClass H] {a : G} {b : H} [DistribSMul K H] (c : K) (f : AddConstMap G H a b) :

⇑(AddConstMap.smul c f) = c • ⇑f

source