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 accomodate 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) extends DFunLike :

Type (max (max u_1 u_2) u_3)

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

coe : F → G → H
coe_injective' : Function.Injective DFunLike.coe
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} {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

@[simp]

theorem AddConstMapClass.map_add_nsmul {F : Type u_1} {G : Type u_2} {H : Type u_3} {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

@[simp]

theorem AddConstMapClass.map_add_nat' {F : Type u_1} {G : Type u_2} {H : Type u_3} {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} {b : H} [AddMonoidWithOne G] [Add H] [AddConstMapClass F G H 1 b] (f : F) (x : G) :

f (x + 1) = f x + b

source

@[simp]

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

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} [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} [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ℕ) [Nat.AtLeastTwo n] :

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

source

@[simp]

theorem AddConstMapClass.map_const {F : Type u_1} {G : Type u_2} {H : Type u_3} {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} {b : H} [AddZeroClass G] [One G] [Add H] [AddConstMapClass F G H 1 b] (f : F) :

f 1 = f 0 + b

source

@[simp]

theorem AddConstMapClass.map_nsmul_const {F : Type u_1} {G : Type u_2} {H : Type u_3} {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

@[simp]

theorem AddConstMapClass.map_nat' {F : Type u_1} {G : Type u_2} {H : Type u_3} {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} {b : H} [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ℕ) [Nat.AtLeastTwo n] :

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} [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} [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℕ) [Nat.AtLeastTwo n] :

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

source

@[simp]

theorem AddConstMapClass.map_const_add {F : Type u_1} {G : Type u_2} {H : Type u_3} {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} {b : H} [AddCommMonoidWithOne G] [Add H] [AddConstMapClass F G H 1 b] (f : F) (x : G) :

f (1 + x) = f x + b

source

@[simp]

theorem AddConstMapClass.map_nsmul_add {F : Type u_1} {G : Type u_2} {H : Type u_3} {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

@[simp]

theorem AddConstMapClass.map_nat_add' {F : Type u_1} {G : Type u_2} {H : Type u_3} {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} {b : H} [AddCommMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ℕ) [Nat.AtLeastTwo n] (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} [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} [AddCommMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℕ) [Nat.AtLeastTwo n] (x : G) :

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

source

@[simp]

theorem AddConstMapClass.map_sub_nsmul {F : Type u_1} {G : Type u_2} {H : Type u_3} {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

@[simp]

theorem AddConstMapClass.map_sub_const {F : Type u_1} {G : Type u_2} {H : Type u_3} {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} {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

@[simp]

theorem AddConstMapClass.map_sub_nat' {F : Type u_1} {G : Type u_2} {H : Type u_3} {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

@[simp]

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

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

source

@[simp]

theorem AddConstMapClass.map_add_zsmul {F : Type u_1} {G : Type u_2} {H : Type u_3} {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

@[simp]

theorem AddConstMapClass.map_zsmul_const {F : Type u_1} {G : Type u_2} {H : Type u_3} {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

@[simp]

theorem AddConstMapClass.map_add_int' {F : Type u_1} {G : Type u_2} {H : Type u_3} {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} [AddGroupWithOne G] [AddGroupWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ℤ) :

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

source

@[simp]

theorem AddConstMapClass.map_sub_zsmul {F : Type u_1} {G : Type u_2} {H : Type u_3} {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

@[simp]

theorem AddConstMapClass.map_sub_int' {F : Type u_1} {G : Type u_2} {H : Type u_3} {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} [AddGroupWithOne G] [AddGroupWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ℤ) :

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

source

@[simp]

theorem AddConstMapClass.map_zsmul_add {F : Type u_1} {G : Type u_2} {H : Type u_3} {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

@[simp]

theorem AddConstMapClass.map_int_add' {F : Type u_1} {G : Type u_2} {H : Type u_3} {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} [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] [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} {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 (x x_1 : G) => x < x_1) ⇒ 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} {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} {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} {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} {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.instAddConstMapClassAddConstMap {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

Equations

AddConstMap.instAddConstMapClassAddConstMap = AddConstMapClass.mk (_ : ∀ (f : AddConstMap G H a b) (x : G), f.toFun (x + a) = f.toFun x + b)

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' := (_ : ∀ (x : G), f.toFun (x + a) = f.toFun x + b) } = f

source

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

f = g

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

source

@[simp]

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

⇑AddConstMap.id = id

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' := (_ : ∀ (x : G), id (x + a) = id (x + a)) }

Instances For

source

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

Inhabited (AddConstMap G G a a)

Equations

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

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

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

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

AddConstMap.comp g f = { toFun := ⇑g ∘ ⇑f, map_add_const' := (_ : ∀ (a_1 : G), g (f (a_1 + a)) = g (f a_1) + c) }

Instances For

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

AddConstMap.comp f 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.comp AddConstMap.id f = f

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') :

⇑(AddConstMap.replaceConsts f a' b' ha hb) = ⇑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

AddConstMap.replaceConsts f a' b' ha hb = { toFun := ⇑f, map_add_const' := (_ : ∀ (x : G), f (x + a') = f x + b') }

Instances For

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

source

instance AddConstMap.instVAddAddConstMap {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.instVAddAddConstMap = { vadd := fun (c : K) (f : AddConstMap G H a b) => { toFun := c +ᵥ ⇑f, map_add_const' := (_ : ∀ (x : G), c +ᵥ f (x + a) = c +ᵥ f x + b) } }

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.instAddActionAddConstMap {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

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

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

source

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

Monoid (AddConstMap G G a a)

Equations

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

source

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

f * g = AddConstMap.comp f g

source

@[simp]

theorem AddConstMap.coe_mul {G : Type u_1} [Add G] {a : G} (f : AddConstMap G G a a) (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

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

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

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

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