# Documentation

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

See also Circle and Real.angle. For the normed group structure on AddCircle, see AddCircle.NormedAddCommGroup in a later file.

## Main definitions and results: #

• AddCircle: the additive circle 𝕜 ⧸ (ℤ ∙ p) for some period p : 𝕜
• UnitAddCircle: the special case ℝ ⧸ ℤ
• AddCircle.equivAddCircle: the rescaling equivalence AddCircle p ≃+ AddCircle q
• AddCircle.equivIco: the natural equivalence AddCircle p ≃ Ico a (a + p)
• AddCircle.addOrderOf_div_of_gcd_eq_one: rational points have finite order
• AddCircle.exists_gcd_eq_one_of_isOfFinAddOrder: finite-order points are rational
• AddCircle.homeoIccQuot: the natural topological equivalence between AddCircle p and Icc a (a + p) with its endpoints identified.
• AddCircle.liftIco_continuous: if f : ℝ → B is continuous, and f a = f (a + p) for some a, then there is a continuous function AddCircle 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 AddCircle (1 : ℚ), and so we set things up more generally.

## TODO #

• Lie group structure
• Exponential equivalence to Circle
theorem continuous_right_toIcoMod {𝕜 : Type u_1} [] [] [] {p : 𝕜} (hp : 0 < p) (a : 𝕜) (x : 𝕜) :
theorem continuous_left_toIocMod {𝕜 : Type u_1} [] [] [] {p : 𝕜} (hp : 0 < p) (a : 𝕜) (x : 𝕜) :
theorem toIcoMod_eventuallyEq_toIocMod {𝕜 : Type u_1} [] [] [] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : x a) :
theorem continuousAt_toIcoMod {𝕜 : Type u_1} [] [] [] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : x a) :
theorem continuousAt_toIocMod {𝕜 : Type u_1} [] [] [] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : x a) :
def AddCircle {𝕜 : Type u_1} [] [] (p : 𝕜) :
Type u_1

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

Instances For
instance instAddCommGroupAddCircle {𝕜 : Type u_1} [] [] (p : 𝕜) :
instance instTopologicalSpaceAddCircle {𝕜 : Type u_1} [] [] (p : 𝕜) :
instance instInhabitedAddCircle {𝕜 : Type u_1} [] [] (p : 𝕜) :
instance instCoeAddCircle {𝕜 : Type u_1} [] [] (p : 𝕜) :
Coe 𝕜 ()
theorem AddCircle.coe_nsmul {𝕜 : Type u_1} (p : 𝕜) {n : } {x : 𝕜} :
↑(n x) = n x
theorem AddCircle.coe_zsmul {𝕜 : Type u_1} (p : 𝕜) {n : } {x : 𝕜} :
↑(n x) = n x
theorem AddCircle.coe_add {𝕜 : Type u_1} (p : 𝕜) (x : 𝕜) (y : 𝕜) :
↑(x + y) = x + y
theorem AddCircle.coe_sub {𝕜 : Type u_1} (p : 𝕜) (x : 𝕜) (y : 𝕜) :
↑(x - y) = x - y
theorem AddCircle.coe_neg {𝕜 : Type u_1} (p : 𝕜) {x : 𝕜} :
↑(-x) = -x
theorem AddCircle.coe_eq_zero_iff {𝕜 : Type u_1} (p : 𝕜) {x : 𝕜} :
x = 0 n, n p = x
theorem AddCircle.coe_eq_zero_of_pos_iff {𝕜 : Type u_1} (p : 𝕜) (hp : 0 < p) {x : 𝕜} (hx : 0 < x) :
x = 0 n, n p = x
theorem AddCircle.coe_period {𝕜 : Type u_1} (p : 𝕜) :
p = 0
theorem AddCircle.coe_add_period {𝕜 : Type u_1} (p : 𝕜) (x : 𝕜) :
↑(x + p) = x
theorem AddCircle.continuous_mk' {𝕜 : Type u_1} [] (p : 𝕜) :
instance AddCircle.instCircularOrderAddCircle {𝕜 : Type u_1} [] [] (p : 𝕜) [hp : Fact (0 < p)] [] :
def AddCircle.equivIco {𝕜 : Type u_1} [] [] (p : 𝕜) [hp : Fact (0 < p)] (a : 𝕜) [] :
↑(Set.Ico a (a + p))

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

Instances For
def AddCircle.equivIoc {𝕜 : Type u_1} [] [] (p : 𝕜) [hp : Fact (0 < p)] (a : 𝕜) [] :
↑(Set.Ioc a (a + p))

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

Instances For
def AddCircle.liftIco {𝕜 : Type u_1} {B : Type u_2} [] [] (p : 𝕜) [hp : Fact (0 < p)] (a : 𝕜) [] (f : 𝕜B) :
B

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

Instances For
def AddCircle.liftIoc {𝕜 : Type u_1} {B : Type u_2} [] [] (p : 𝕜) [hp : Fact (0 < p)] (a : 𝕜) [] (f : 𝕜B) :
B

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

Instances For
theorem AddCircle.coe_eq_coe_iff_of_mem_Ico {𝕜 : Type u_1} [] [] {p : 𝕜} [hp : Fact (0 < p)] {a : 𝕜} [] {x : 𝕜} {y : 𝕜} (hx : x Set.Ico a (a + p)) (hy : y Set.Ico a (a + p)) :
x = y x = y
theorem AddCircle.liftIco_coe_apply {𝕜 : Type u_1} {B : Type u_2} [] [] {p : 𝕜} [hp : Fact (0 < p)] {a : 𝕜} [] {f : 𝕜B} {x : 𝕜} (hx : x Set.Ico a (a + p)) :
AddCircle.liftIco p a f x = f x
theorem AddCircle.liftIoc_coe_apply {𝕜 : Type u_1} {B : Type u_2} [] [] {p : 𝕜} [hp : Fact (0 < p)] {a : 𝕜} [] {f : 𝕜B} {x : 𝕜} (hx : x Set.Ioc a (a + p)) :
AddCircle.liftIoc p a f x = f x
theorem AddCircle.continuous_equivIco_symm {𝕜 : Type u_1} [] [] (p : 𝕜) [hp : Fact (0 < p)] (a : 𝕜) [] :
Continuous ().symm
theorem AddCircle.continuous_equivIoc_symm {𝕜 : Type u_1} [] [] (p : 𝕜) [hp : Fact (0 < p)] (a : 𝕜) [] :
Continuous ().symm
theorem AddCircle.continuousAt_equivIco {𝕜 : Type u_1} [] [] (p : 𝕜) [hp : Fact (0 < p)] (a : 𝕜) [] {x : } (hx : x a) :
ContinuousAt (↑()) x
theorem AddCircle.continuousAt_equivIoc {𝕜 : Type u_1} [] [] (p : 𝕜) [hp : Fact (0 < p)] (a : 𝕜) [] {x : } (hx : x a) :
ContinuousAt (↑()) x
@[simp]
theorem AddCircle.coe_image_Ico_eq {𝕜 : Type u_1} [] [] (p : 𝕜) [hp : Fact (0 < p)] (a : 𝕜) [] :
QuotientAddGroup.mk '' Set.Ico a (a + p) = Set.univ

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

@[simp]
theorem AddCircle.coe_image_Ioc_eq {𝕜 : Type u_1} [] [] (p : 𝕜) [hp : Fact (0 < p)] (a : 𝕜) [] :
QuotientAddGroup.mk '' Set.Ioc a (a + p) = Set.univ

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

@[simp]
theorem AddCircle.coe_image_Icc_eq {𝕜 : Type u_1} [] [] (p : 𝕜) [hp : Fact (0 < p)] (a : 𝕜) [] :
QuotientAddGroup.mk '' Set.Icc a (a + p) = Set.univ

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

def AddCircle.equivAddCircle {𝕜 : Type u_1} [] [] (p : 𝕜) (q : 𝕜) (hp : p 0) (hq : q 0) :

The rescaling equivalence between additive circles with different periods.

Instances For
@[simp]
theorem AddCircle.equivAddCircle_apply_mk {𝕜 : Type u_1} [] [] (p : 𝕜) (q : 𝕜) (hp : p 0) (hq : q 0) (x : 𝕜) :
↑(AddCircle.equivAddCircle p q hp hq) x = ↑(x * (p⁻¹ * q))
@[simp]
theorem AddCircle.equivAddCircle_symm_apply_mk {𝕜 : Type u_1} [] [] (p : 𝕜) (q : 𝕜) (hp : p 0) (hq : q 0) (x : 𝕜) :
@[simp]
theorem AddCircle.coe_equivIco_mk_apply {𝕜 : Type u_1} [] [] (p : 𝕜) [hp : Fact (0 < p)] [] (x : 𝕜) :
↑(↑() x) = Int.fract (x / p) * p
theorem AddCircle.addOrderOf_period_div {𝕜 : Type u_1} {p : 𝕜} [hp : Fact (0 < p)] {n : } (h : 0 < n) :
addOrderOf ↑(p / n) = n
theorem AddCircle.gcd_mul_addOrderOf_div_eq {𝕜 : Type u_1} (p : 𝕜) [hp : Fact (0 < p)] {n : } (m : ) (hn : 0 < n) :
Nat.gcd m n * addOrderOf ↑(m / n * p) = n
theorem AddCircle.addOrderOf_div_of_gcd_eq_one {𝕜 : Type u_1} {p : 𝕜} [hp : Fact (0 < p)] {m : } {n : } (hn : 0 < n) (h : Nat.gcd m n = 1) :
addOrderOf ↑(m / n * p) = n
theorem AddCircle.addOrderOf_div_of_gcd_eq_one' {𝕜 : Type u_1} {p : 𝕜} [hp : Fact (0 < p)] {m : } {n : } (hn : 0 < n) (h : Nat.gcd () n = 1) :
addOrderOf ↑(m / n * p) = n
theorem AddCircle.addOrderOf_coe_rat {𝕜 : Type u_1} {p : 𝕜} [hp : Fact (0 < p)] {q : } :
addOrderOf ↑(q * p) = q.den
theorem AddCircle.addOrderOf_eq_pos_iff {𝕜 : Type u_1} [] [] {p : 𝕜} [hp : Fact (0 < p)] {u : } {n : } (h : 0 < n) :
= n m, m < n Nat.gcd m n = 1 ↑(m / n * p) = u
theorem AddCircle.exists_gcd_eq_one_of_isOfFinAddOrder {𝕜 : Type u_1} [] [] {p : 𝕜} [hp : Fact (0 < p)] {u : } (h : ) :
m, Nat.gcd m () = 1 m < ↑(m / ↑() * p) = u
def AddCircle.setAddOrderOfEquiv {𝕜 : Type u_1} [] [] (p : 𝕜) [hp : Fact (0 < p)] {n : } (hn : 0 < n) :
{u | = n} {m | m < n Nat.gcd m 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 : AddCircle p) where m is coprime to n and satisfies 0 ≤ m < n.

Instances For
@[simp]
theorem AddCircle.card_addOrderOf_eq_totient {𝕜 : Type u_1} [] [] (p : 𝕜) [hp : Fact (0 < p)] {n : } :
Nat.card { u // = n } =
theorem AddCircle.finite_setOf_add_order_eq {𝕜 : Type u_1} [] [] (p : 𝕜) [hp : Fact (0 < p)] {n : } (hn : 0 < n) :
Set.Finite {u | = n}
instance AddCircle.compactSpace (p : ) [Fact (0 < p)] :

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

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

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

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

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

@[inline, reducible]

The unit circle ℝ ⧸ ℤ.

Instances For

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

inductive AddCircle.EndpointIdent {𝕜 : Type u_1} (p : 𝕜) (a : 𝕜) [hp : Fact (0 < p)] :
↑(Set.Icc a (a + p))↑(Set.Icc a (a + p))Prop

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

Instances For
def AddCircle.equivIccQuot {𝕜 : Type u_1} [] [] (p : 𝕜) (a : 𝕜) [hp : Fact (0 < p)] [] :

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

Instances For
theorem AddCircle.equivIccQuot_comp_mk_eq_toIcoMod {𝕜 : Type u_1} [] [] (p : 𝕜) (a : 𝕜) [hp : Fact (0 < p)] [] :
↑() Quotient.mk'' = fun x => Quot.mk () { val := toIcoMod (_ : 0 < p) a x, property := (_ : toIcoMod (_ : 0 < p) a x Set.Icc a (a + p)) }
theorem AddCircle.equivIccQuot_comp_mk_eq_toIocMod {𝕜 : Type u_1} [] [] (p : 𝕜) (a : 𝕜) [hp : Fact (0 < p)] [] :
↑() Quotient.mk'' = fun x => Quot.mk () { val := toIocMod (_ : 0 < p) a x, property := (_ : toIocMod (_ : 0 < p) a x Set.Icc a (a + p)) }
def AddCircle.homeoIccQuot {𝕜 : Type u_1} [] [] (p : 𝕜) (a : 𝕜) [hp : Fact (0 < p)] [] :

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

Instances For

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 AddCircle p.

theorem AddCircle.liftIco_eq_lift_Icc {𝕜 : Type u_1} {B : Type u_2} [] [] {p : 𝕜} {a : 𝕜} [hp : Fact (0 < p)] [] {f : 𝕜B} (h : f a = f (a + p)) :
= Quot.lift (Set.restrict (Set.Icc a (a + p)) f) (_ : ∀ (a b : ↑(Set.Icc a (a + p))), Set.restrict (Set.Icc a (a + p)) f a = Set.restrict (Set.Icc a (a + p)) f b) ↑()
theorem AddCircle.liftIco_continuous {𝕜 : Type u_1} {B : Type u_2} [] [] {p : 𝕜} {a : 𝕜} [hp : Fact (0 < p)] [] [] {f : 𝕜B} (hf : f a = f (a + p)) (hc : ContinuousOn f (Set.Icc a (a + p))) :
theorem AddCircle.liftIco_zero_coe_apply {𝕜 : Type u_1} {B : Type u_2} [] [] {p : 𝕜} [hp : Fact (0 < p)] [] {f : 𝕜B} {x : 𝕜} (hx : x Set.Ico 0 p) :
AddCircle.liftIco p 0 f x = f x
theorem AddCircle.liftIco_zero_continuous {𝕜 : Type u_1} {B : Type u_2} [] [] {p : 𝕜} [hp : Fact (0 < p)] [] [] {f : 𝕜B} (hf : f 0 = f p) (hc : ContinuousOn f (Set.Icc 0 p)) :