The additive circle #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define the additive circle add_circle p as the quotient 𝕜 ⧸ (ℤ ∙ p) for some period p : 𝕜.

See also circle and real.angle. For the normed group structure on add_circle, see add_circle.normed_add_comm_group in a later file.

Main definitions and results: #

add_circle: the additive circle 𝕜 ⧸ (ℤ ∙ p) for some period p : 𝕜
unit_add_circle: the special case ℝ ⧸ ℤ
add_circle.equiv_add_circle: the rescaling equivalence add_circle p ≃+ add_circle q
add_circle.equiv_Ico: the natural equivalence add_circle p ≃ Ico a (a + p)
add_circle.add_order_of_div_of_gcd_eq_one: rational points have finite order
add_circle.exists_gcd_eq_one_of_is_of_fin_add_order: finite-order points are rational
add_circle.homeo_Icc_quot: the natural topological equivalence between add_circle p and Icc a (a + p) with its endpoints identified.
add_circle.lift_Ico_continuous: if f : ℝ → B is continuous, and f a = f (a + p) for some a, then there is a continuous function add_circle p → B which agrees with f on Icc a (a + p).

Implementation notes: #

Although the most important case is 𝕜 = ℝ we wish to support other types of scalars, such as the rational circle add_circle (1 : ℚ), and so we set things up more generally.

TODO #

Link with periodicity
Lie group structure
Exponential equivalence to circle

source

theorem continuous_right_to_Ico_mod {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [archimedean 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜) :

continuous_within_at (to_Ico_mod hp a) (set.Ici x) x

source

theorem continuous_left_to_Ioc_mod {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [archimedean 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜) :

continuous_within_at (to_Ioc_mod hp a) (set.Iic x) x

source

theorem to_Ico_mod_eventually_eq_to_Ioc_mod {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [archimedean 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : ↑x ≠ ↑a) :

to_Ico_mod hp a =ᶠ[nhds x] to_Ioc_mod hp a

source

theorem continuous_at_to_Ico_mod {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [archimedean 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : ↑x ≠ ↑a) :

continuous_at (to_Ico_mod hp a) x

source

theorem continuous_at_to_Ioc_mod {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [archimedean 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : ↑x ≠ ↑a) :

continuous_at (to_Ioc_mod hp a) x

source

@[protected, instance]

def add_circle.add_comm_group {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) :

add_comm_group (add_circle p)

source

@[nolint]

def add_circle {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) :

Type u_1

The "additive circle": 𝕜 ⧸ (ℤ ∙ p). See also circle and real.angle.

Equations

add_circle p = (𝕜 ⧸ add_subgroup.zmultiples p)

Instances for add_circle

source

@[protected, instance]

def add_circle.topological_space {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) :

topological_space (add_circle p)

source

@[protected, instance]

def add_circle.has_coe_t {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) :

has_coe_t 𝕜 (add_circle p)

source

@[protected, instance]

def add_circle.inhabited {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) :

inhabited (add_circle p)

source

@[protected, instance]

def add_circle.topological_add_group {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) :

topological_add_group (add_circle p)

source

theorem add_circle.coe_nsmul {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) {n : ℕ} {x : 𝕜} :

↑(n • x) = n • ↑x

source

theorem add_circle.coe_zsmul {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) {n : ℤ} {x : 𝕜} :

↑(n • x) = n • ↑x

source

theorem add_circle.coe_add {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p x y : 𝕜) :

↑(x + y) = ↑x + ↑y

source

theorem add_circle.coe_sub {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p x y : 𝕜) :

↑(x - y) = ↑x - ↑y

source

theorem add_circle.coe_neg {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) {x : 𝕜} :

↑-x = -↑x

source

theorem add_circle.coe_eq_zero_iff {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) {x : 𝕜} :

↑x = 0 ↔ ∃ (n : ℤ), n • p = x

source

theorem add_circle.coe_eq_zero_of_pos_iff {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) (hp : 0 < p) {x : 𝕜} (hx : 0 < x) :

↑x = 0 ↔ ∃ (n : ℕ), n • p = x

source

theorem add_circle.coe_period {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) :

↑p = 0

source

@[simp]

theorem add_circle.coe_add_period {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p x : 𝕜) :

↑(x + p) = ↑x

source

@[protected, nolint, continuity]

theorem add_circle.continuous_mk' {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) :

continuous ⇑(quotient_add_group.mk' (add_subgroup.zmultiples p))

source

@[protected, instance]

def add_circle.circular_order {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] [archimedean 𝕜] :

circular_order (add_circle p)

Equations

add_circle.circular_order p = quotient_add_group.circular_order

source

noncomputable def add_circle.equiv_Ico {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] (a : 𝕜) [archimedean 𝕜] :

add_circle p ≃ ↥(set.Ico a (a + p))

The equivalence between add_circle p and the half-open interval [a, a + p), whose inverse is the natural quotient map.

Equations

add_circle.equiv_Ico p a = quotient_add_group.equiv_Ico_mod _ a

source

noncomputable def add_circle.equiv_Ioc {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] (a : 𝕜) [archimedean 𝕜] :

add_circle p ≃ ↥(set.Ioc a (a + p))

The equivalence between add_circle p and the half-open interval (a, a + p], whose inverse is the natural quotient map.

Equations

add_circle.equiv_Ioc p a = quotient_add_group.equiv_Ioc_mod _ a

source

noncomputable def add_circle.lift_Ico {𝕜 : Type u_1} {B : Type u_2} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] (a : 𝕜) [archimedean 𝕜] (f : 𝕜 → B) :

add_circle p → B

Given a function on 𝕜, return the unique function on add_circle p agreeing with f on [a, a + p).

Equations

add_circle.lift_Ico p a f = (set.Ico a (a + p)).restrict f ∘ ⇑(add_circle.equiv_Ico p a)

source

noncomputable def add_circle.lift_Ioc {𝕜 : Type u_1} {B : Type u_2} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] (a : 𝕜) [archimedean 𝕜] (f : 𝕜 → B) :

add_circle p → B

Given a function on 𝕜, return the unique function on add_circle p agreeing with f on (a, a + p].

Equations

add_circle.lift_Ioc p a f = (set.Ioc a (a + p)).restrict f ∘ ⇑(add_circle.equiv_Ioc p a)

source

theorem add_circle.coe_eq_coe_iff_of_mem_Ico {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p : 𝕜} [hp : fact (0 < p)] {a : 𝕜} [archimedean 𝕜] {x y : 𝕜} (hx : x ∈ set.Ico a (a + p)) (hy : y ∈ set.Ico a (a + p)) :

↑x = ↑y ↔ x = y

source

theorem add_circle.lift_Ico_coe_apply {𝕜 : Type u_1} {B : Type u_2} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p : 𝕜} [hp : fact (0 < p)] {a : 𝕜} [archimedean 𝕜] {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ set.Ico a (a + p)) :

add_circle.lift_Ico p a f ↑x = f x

source

theorem add_circle.lift_Ioc_coe_apply {𝕜 : Type u_1} {B : Type u_2} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p : 𝕜} [hp : fact (0 < p)] {a : 𝕜} [archimedean 𝕜] {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ set.Ioc a (a + p)) :

add_circle.lift_Ioc p a f ↑x = f x

source

@[continuity]

theorem add_circle.continuous_equiv_Ico_symm {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] (a : 𝕜) [archimedean 𝕜] :

continuous ⇑((add_circle.equiv_Ico p a).symm)

source

@[continuity]

theorem add_circle.continuous_equiv_Ioc_symm {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] (a : 𝕜) [archimedean 𝕜] :

continuous ⇑((add_circle.equiv_Ioc p a).symm)

source

theorem add_circle.continuous_at_equiv_Ico {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] (a : 𝕜) [archimedean 𝕜] {x : add_circle p} (hx : x ≠ ↑a) :

continuous_at ⇑(add_circle.equiv_Ico p a) x

source

theorem add_circle.continuous_at_equiv_Ioc {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] (a : 𝕜) [archimedean 𝕜] {x : add_circle p} (hx : x ≠ ↑a) :

continuous_at ⇑(add_circle.equiv_Ioc p a) x

source

@[simp]

theorem add_circle.coe_image_Ico_eq {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] (a : 𝕜) [archimedean 𝕜] :

coe '' set.Ico a (a + p) = set.univ

The image of the closed-open interval [a, a + p) under the quotient map 𝕜 → add_circle p is the entire space.

source

@[simp]

theorem add_circle.coe_image_Ioc_eq {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] (a : 𝕜) [archimedean 𝕜] :

coe '' set.Ioc a (a + p) = set.univ

The image of the closed-open interval [a, a + p) under the quotient map 𝕜 → add_circle p is the entire space.

source

@[simp]

theorem add_circle.coe_image_Icc_eq {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] (a : 𝕜) [archimedean 𝕜] :

coe '' set.Icc a (a + p) = set.univ

The image of the closed interval [0, p] under the quotient map 𝕜 → add_circle p is the entire space.

source

def add_circle.equiv_add_circle {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p q : 𝕜) (hp : p ≠ 0) (hq : q ≠ 0) :

add_circle p ≃+ add_circle q

The rescaling equivalence between additive circles with different periods.

Equations

add_circle.equiv_add_circle p q hp hq = quotient_add_group.congr (add_subgroup.zmultiples p) (add_subgroup.zmultiples q) (add_aut.mul_right ((units.mk0 p hp)⁻¹ * units.mk0 q hq)) _

source

@[simp]

theorem add_circle.equiv_add_circle_apply_mk {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p q : 𝕜) (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) :

⇑(add_circle.equiv_add_circle p q hp hq) ↑x = ↑(x * (p⁻¹ * q))

source

@[simp]

theorem add_circle.equiv_add_circle_symm_apply_mk {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p q : 𝕜) (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) :

⇑((add_circle.equiv_add_circle p q hp hq).symm) ↑x = ↑(x * (q⁻¹ * p))

source

@[simp]

theorem add_circle.coe_equiv_Ico_mk_apply {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] [floor_ring 𝕜] (x : 𝕜) :

↑(⇑(add_circle.equiv_Ico p 0) (quotient_add_group.mk x)) = int.fract (x / p) * p

source

@[protected, instance]

noncomputable def add_circle.int.divisible_by {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] [floor_ring 𝕜] :

divisible_by (add_circle p) ℤ

Equations

add_circle.int.divisible_by p = {div := λ (x : add_circle p) (n : ℤ), ↑((↑n)⁻¹ * ↑(⇑(add_circle.equiv_Ico p 0) x)), div_zero := _, div_cancel := _}

source

theorem add_circle.add_order_of_period_div {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p : 𝕜} [hp : fact (0 < p)] {n : ℕ} (h : 0 < n) :

add_order_of ↑(p / ↑n) = n

source

theorem add_circle.gcd_mul_add_order_of_div_eq {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] {n : ℕ} (m : ℕ) (hn : 0 < n) :

m.gcd n * add_order_of ↑(↑m / ↑n * p) = n

source

theorem add_circle.add_order_of_div_of_gcd_eq_one {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p : 𝕜} [hp : fact (0 < p)] {m n : ℕ} (hn : 0 < n) (h : m.gcd n = 1) :

add_order_of ↑(↑m / ↑n * p) = n

source

theorem add_circle.add_order_of_div_of_gcd_eq_one' {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p : 𝕜} [hp : fact (0 < p)] {m : ℤ} {n : ℕ} (hn : 0 < n) (h : m.nat_abs.gcd n = 1) :

add_order_of ↑(↑m / ↑n * p) = n

source

theorem add_circle.add_order_of_coe_rat {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p : 𝕜} [hp : fact (0 < p)] {q : ℚ} :

add_order_of ↑(↑q * p) = q.denom

source

theorem add_circle.add_order_of_eq_pos_iff {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p : 𝕜} [hp : fact (0 < p)] {u : add_circle p} {n : ℕ} (h : 0 < n) :

add_order_of u = n ↔ ∃ (m : ℕ) (H : m < n), m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u

source

theorem add_circle.exists_gcd_eq_one_of_is_of_fin_add_order {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p : 𝕜} [hp : fact (0 < p)] {u : add_circle p} (h : is_of_fin_add_order u) :

∃ (m : ℕ), m.gcd (add_order_of u) = 1 ∧ m < add_order_of u ∧ ↑(↑m / ↑(add_order_of u) * p) = u

source

noncomputable def add_circle.set_add_order_of_equiv {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] {n : ℕ} (hn : 0 < n) :

↥{u : add_circle p | add_order_of u = n} ≃ ↥{m : ℕ | m < n ∧ m.gcd n = 1}

The natural bijection between points of order n and natural numbers less than and coprime to n. The inverse of the map sends m ↦ (m/n * p : add_circle p) where m is coprime to n and satisfies 0 ≤ m < n.

Equations

add_circle.set_add_order_of_equiv p hn = (equiv.of_bijective (λ (m : ↥{m : ℕ | m < n ∧ m.gcd n = 1}), ⟨↑(↑m / ↑n * p), _⟩) _).symm

source

@[simp]

theorem add_circle.card_add_order_of_eq_totient {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] {n : ℕ} :

nat.card {u // add_order_of u = n} = n.totient

source

theorem add_circle.finite_set_of_add_order_eq {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p : 𝕜) [hp : fact (0 < p)] {n : ℕ} (hn : 0 < n) :

{u : add_circle p | add_order_of u = n}.finite

source

@[protected, instance]

def add_circle.compact_space (p : ℝ) [fact (0 < p)] :

compact_space (add_circle p)

The "additive circle" ℝ ⧸ (ℤ ∙ p) is compact.

source

@[protected, instance]

def add_circle.real.properly_discontinuous_vadd (p : ℝ) :

properly_discontinuous_vadd ↥(⇑add_subgroup.opposite (add_subgroup.zmultiples p)) ℝ

The action on ℝ by right multiplication of its the subgroup zmultiples p (the multiples of p:ℝ) is properly discontinuous.

source

@[protected, instance]

def add_circle.t2_space (p : ℝ) :

t2_space (add_circle p)

The "additive circle" ℝ ⧸ (ℤ ∙ p) is Hausdorff.

source

@[protected, instance]

def add_circle.normal_space (p : ℝ) [fact (0 < p)] :

normal_space (add_circle p)

The "additive circle" ℝ ⧸ (ℤ ∙ p) is normal.

source

@[protected, instance]

def add_circle.topological_space.second_countable_topology (p : ℝ) :

topological_space.second_countable_topology (add_circle p)

The "additive circle" ℝ ⧸ (ℤ ∙ p) is second-countable.

source

@[protected, instance]

def unit_add_circle.compact_space :

compact_space unit_add_circle

source

@[protected, instance]

def unit_add_circle.normal_space :

normal_space unit_add_circle

source

@[protected, instance]

def unit_add_circle.second_countable_topology :

topological_space.second_countable_topology unit_add_circle

source

@[reducible]

def unit_add_circle :

Type

The unit circle ℝ ⧸ ℤ.

This section proves that for any a, the natural map from [a, a + p] ⊂ 𝕜 to add_circle p gives an identification of add_circle p, as a topological space, with the quotient of [a, a + p] by the equivalence relation identifying the endpoints.

source

inductive add_circle.endpoint_ident {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p a : 𝕜) [hp : fact (0 < p)] :

↥(set.Icc a (a + p)) → ↥(set.Icc a (a + p)) → Prop

mk : ∀ {𝕜 : Type u_1} [_inst_1 : linear_ordered_add_comm_group 𝕜] [_inst_2 : topological_space 𝕜] [_inst_3 : order_topology 𝕜] {p a : 𝕜} [hp : fact (0 < p)], add_circle.endpoint_ident p a ⟨a, _⟩ ⟨a + p, _⟩

The relation identifying the endpoints of Icc a (a + p).

source

noncomputable def add_circle.equiv_Icc_quot {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p a : 𝕜) [hp : fact (0 < p)] [archimedean 𝕜] :

add_circle p ≃ quot (add_circle.endpoint_ident p a)

The equivalence between add_circle p and the quotient of [a, a + p] by the relation identifying the endpoints.

Equations

add_circle.equiv_Icc_quot p a = {to_fun := λ (x : add_circle p), quot.mk (add_circle.endpoint_ident p a) (set.inclusion _ (⇑(add_circle.equiv_Ico p a) x)), inv_fun := λ (x : quot (add_circle.endpoint_ident p a)), x.lift_on coe _, left_inv := _, right_inv := _}

source

theorem add_circle.equiv_Icc_quot_comp_mk_eq_to_Ico_mod {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p a : 𝕜) [hp : fact (0 < p)] [archimedean 𝕜] :

⇑(add_circle.equiv_Icc_quot p a) ∘ quotient.mk' = λ (x : 𝕜), quot.mk (add_circle.endpoint_ident p a) ⟨to_Ico_mod _ a x, _⟩

source

theorem add_circle.equiv_Icc_quot_comp_mk_eq_to_Ioc_mod {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p a : 𝕜) [hp : fact (0 < p)] [archimedean 𝕜] :

⇑(add_circle.equiv_Icc_quot p a) ∘ quotient.mk' = λ (x : 𝕜), quot.mk (add_circle.endpoint_ident p a) ⟨to_Ioc_mod _ a x, _⟩

source

noncomputable def add_circle.homeo_Icc_quot {𝕜 : Type u_1} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p a : 𝕜) [hp : fact (0 < p)] [archimedean 𝕜] :

add_circle p ≃ₜ quot (add_circle.endpoint_ident p a)

The natural map from [a, a + p] ⊂ 𝕜 with endpoints identified to 𝕜 / ℤ • p, as a homeomorphism of topological spaces.

Equations

add_circle.homeo_Icc_quot p a = {to_equiv := add_circle.equiv_Icc_quot p a _inst_4, continuous_to_fun := _, continuous_inv_fun := _}

We now show that a continuous function on [a, a + p] satisfying f a = f (a + p) is the pullback of a continuous function on add_circle p.

source

theorem add_circle.lift_Ico_eq_lift_Icc {𝕜 : Type u_1} {B : Type u_2} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p a : 𝕜} [hp : fact (0 < p)] [archimedean 𝕜] {f : 𝕜 → B} (h : f a = f (a + p)) :

add_circle.lift_Ico p a f = quot.lift ((set.Icc a (a + p)).restrict f) _ ∘ ⇑(add_circle.equiv_Icc_quot p a)

source

theorem add_circle.lift_Ico_continuous {𝕜 : Type u_1} {B : Type u_2} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p a : 𝕜} [hp : fact (0 < p)] [archimedean 𝕜] [topological_space B] {f : 𝕜 → B} (hf : f a = f (a + p)) (hc : continuous_on f (set.Icc a (a + p))) :

continuous (add_circle.lift_Ico p a f)

source

theorem add_circle.lift_Ico_zero_coe_apply {𝕜 : Type u_1} {B : Type u_2} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p : 𝕜} [hp : fact (0 < p)] [archimedean 𝕜] {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ set.Ico 0 p) :

add_circle.lift_Ico p 0 f ↑x = f x

source

theorem add_circle.lift_Ico_zero_continuous {𝕜 : Type u_1} {B : Type u_2} [linear_ordered_add_comm_group 𝕜] [topological_space 𝕜] [order_topology 𝕜] {p : 𝕜} [hp : fact (0 < p)] [archimedean 𝕜] [topological_space B] {f : 𝕜 → B} (hf : f 0 = f p) (hc : continuous_on f (set.Icc 0 p)) :

continuous (add_circle.lift_Ico p 0 f)