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:S^1\to S^1$ of degree 1 is to lift it to a map $\tilde{f}:\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:S^1\to S^1$ of degree other than one, including orientation-reversing maps.

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, denoted as f: G →+c[a, b] H.

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.

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

A bundled map f : G → H such that f (x + a) = f x + b for all x, denoted as f: G →+c[a, b] H.

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.

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.

Properties of AddConstMapClass maps

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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} [AddCommMagma G] [Add H] [AddConstMapClass F G H a b] (f : F) (x : G) : f (a + x) = f x + b

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem AddConstMapClass.map_fract {F : Type u_1} {H : Type u_3} {b : H} {R : Type u_4} [Ring R] [LinearOrder 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

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} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid 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)) : Relator.LiftFun (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.

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} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) : Monotone ⇑f ↔ MonotoneOn (⇑f) (Set.Icc l (l + a))

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} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) : Antitone ⇑f ↔ AntitoneOn (⇑f) (Set.Icc l (l + a))

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} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) : StrictMono ⇑f ↔ StrictMonoOn (⇑f) (Set.Icc l (l + a))

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} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid 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

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' := ⋯ }

@[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

@[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

@[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

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

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

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

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

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' := ⋯ }

@[simp]

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

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

Equations

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

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' := ⋯ }

@[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

@[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

@[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

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' := ⋯ }

@[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

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' := ⋯ } }

@[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

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

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

Equations

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

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

Equations

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

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' := ⋯ } }

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) ⋯ ⋯ ⋯ ⋯

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

@[simp]

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

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

@[simp]

theorem AddConstMap.coe_one {G : Type u_1} [Add G] {a : G} : ⇑1 = id

@[simp]

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

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

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' := ⋯ }

@[simp]

theorem AddConstMap.toEnd_apply {G : Type u_1} [Add G] {a : G} : ⇑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.

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' := ⋯ }

@[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) : ⇑(smul c f) = c • ⇑f

def AddConstMap.addLeftHom {G : Type u_1} [AddMonoid G] {a : G} : Multiplicative G →* AddConstMap G G a a

The map that sends c to a translation by c as a monoid homomorphism from Multiplicative G to G →+c[a, a] G.

Equations

• AddConstMap.addLeftHom = { toFun := fun (c : Multiplicative G) => Multiplicative.toAdd c +ᵥ AddConstMap.id, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AddConstMap.coe_addLeftHom_apply {G : Type u_1} [AddMonoid G] {a : G} (c : Multiplicative G) : ⇑(addLeftHom c) = Multiplicative.toAdd c +ᵥ id

def AddConstMap.conjNeg {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] {a : G} {b : H} : AddConstMap G H a b ≃ AddConstMap G H a b

If f : G → H is an AddConstMap, then so is fun x ↦ -f (-x).

Equations

• AddConstMap.conjNeg = Function.Involutive.toPerm (fun (f : AddConstMap G H a b) => { toFun := fun (x : G) => -f (-x), map_add_const' := ⋯ }) ⋯

@[simp]

theorem AddConstMap.coe_conjNeg_apply {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] {a : G} {b : H} (f : AddConstMap G H a b) (x : G) : (conjNeg f) x = -f (-x)

@[simp]

theorem AddConstMap.conjNeg_symm {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] {a : G} {b : H} : conjNeg.symm = conjNeg

def AddConstMap.mkFract {R : Type u_1} {G : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] [AddGroup G] (a : G) : (↑(Set.Ico 0 1) → G) ≃ AddConstMap R G 1 a

A map f : R →+c[1, a] G is defined by its values on Set.Ico 0 1.

Equations

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