# 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} [] [Archimedean ๐] [TopologicalSpace ๐] [OrderTopology ๐] {p : ๐} (hp : 0 < p) (a : ๐) (x : ๐) :
theorem continuous_left_toIocMod {๐ : Type u_1} [] [Archimedean ๐] [TopologicalSpace ๐] [OrderTopology ๐] {p : ๐} (hp : 0 < p) (a : ๐) (x : ๐) :
theorem toIcoMod_eventuallyEq_toIocMod {๐ : Type u_1} [] [Archimedean ๐] [TopologicalSpace ๐] [OrderTopology ๐] {p : ๐} (hp : 0 < p) (a : ๐) {x : ๐} (hx : โx โ  โa) :
theorem continuousAt_toIcoMod {๐ : Type u_1} [] [Archimedean ๐] [TopologicalSpace ๐] [OrderTopology ๐] {p : ๐} (hp : 0 < p) (a : ๐) {x : ๐} (hx : โx โ  โa) :
theorem continuousAt_toIocMod {๐ : Type u_1} [] [Archimedean ๐] [TopologicalSpace ๐] [OrderTopology ๐] {p : ๐} (hp : 0 < p) (a : ๐) {x : ๐} (hx : โx โ  โa) :
@[reducible, inline]
abbrev AddCircle {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) :
Type u_1

The "additive circle": ๐ โงธ (โค โ p). See also Circle and Real.angle.

Equations
• = ()
Instances For
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} [] [TopologicalSpace ๐] (p : ๐) :
def AddCircle.equivIco {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] (a : ๐) [Archimedean ๐] :
โ โ(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.

Equations
Instances For
def AddCircle.equivIoc {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] (a : ๐) [Archimedean ๐] :
โ โ(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.

Equations
Instances For
def AddCircle.liftIco {๐ : Type u_1} {B : Type u_2} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] (a : ๐) [Archimedean ๐] (f : ๐ โ B) :
โ B

Given a function on ๐, return the unique function on AddCircle p agreeing with f on [a, a + p).

Equations
Instances For
def AddCircle.liftIoc {๐ : Type u_1} {B : Type u_2} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] (a : ๐) [Archimedean ๐] (f : ๐ โ B) :
โ B

Given a function on ๐, return the unique function on AddCircle p agreeing with f on (a, a + p].

Equations
Instances For
theorem AddCircle.coe_eq_coe_iff_of_mem_Ico {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] {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
theorem AddCircle.liftIco_coe_apply {๐ : Type u_1} {B : Type u_2} [] [TopologicalSpace ๐] [OrderTopology ๐] {p : ๐} [hp : Fact (0 < p)] {a : ๐} [Archimedean ๐] {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} [] [TopologicalSpace ๐] [OrderTopology ๐] {p : ๐} [hp : Fact (0 < p)] {a : ๐} [Archimedean ๐] {f : ๐ โ B} {x : ๐} (hx : x โ Set.Ioc a (a + p)) :
AddCircle.liftIoc p a f โx = f x
theorem AddCircle.eq_coe_Ico {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] {p : ๐} [hp : Fact (0 < p)] [Archimedean ๐] (a : ) :
โ b โ Set.Ico 0 p, โb = a
theorem AddCircle.coe_eq_zero_iff_of_mem_Ico {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] {p : ๐} [hp : Fact (0 < p)] {a : ๐} [Archimedean ๐] (ha : a โ Set.Ico 0 p) :
โa = 0 โ a = 0
theorem AddCircle.continuous_equivIco_symm {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] (a : ๐) [Archimedean ๐] :
Continuous โ().symm
theorem AddCircle.continuous_equivIoc_symm {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] (a : ๐) [Archimedean ๐] :
Continuous โ().symm
theorem AddCircle.continuousAt_equivIco {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] (a : ๐) [Archimedean ๐] {x : } (hx : x โ  โa) :
ContinuousAt (โ()) x
theorem AddCircle.continuousAt_equivIoc {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] (a : ๐) [Archimedean ๐] {x : } (hx : x โ  โa) :
ContinuousAt (โ()) x
@[simp]
theorem AddCircle.partialHomeomorphCoe_target {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] (a : ๐) [Archimedean ๐] [] :
.target = {โa}แถ
@[simp]
theorem AddCircle.partialHomeomorphCoe_source {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] (a : ๐) [Archimedean ๐] [] :
.source = Set.Ioo a (a + p)
@[simp]
theorem AddCircle.partialHomeomorphCoe_symm_apply {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] (a : ๐) [Archimedean ๐] [] (x : ) :
โ.symm x = โ(() x)
@[simp]
theorem AddCircle.partialHomeomorphCoe_apply {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] (a : ๐) [Archimedean ๐] [] (a : ๐) :
โ() a = โa
def AddCircle.partialHomeomorphCoe {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] (a : ๐) [Archimedean ๐] [] :
PartialHomeomorph ๐ ()

The quotient map ๐ โ AddCircle p as a partial homeomorphism.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddCircle.isLocalHomeomorph_coe {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] [Archimedean ๐] [] [DenselyOrdered ๐] :
@[simp]
theorem AddCircle.coe_image_Ico_eq {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] (a : ๐) [Archimedean ๐] :
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} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] (a : ๐) [Archimedean ๐] :
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} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] (a : ๐) [Archimedean ๐] :
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} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) (q : ๐) (hp : p โ  0) (hq : q โ  0) :

The rescaling equivalence between additive circles with different periods.

Equations
Instances For
@[simp]
theorem AddCircle.equivAddCircle_apply_mk {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) (q : ๐) (hp : p โ  0) (hq : q โ  0) (x : ๐) :
(AddCircle.equivAddCircle p q hp hq) โx = โ(x * ( * q))
@[simp]
theorem AddCircle.equivAddCircle_symm_apply_mk {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) (q : ๐) (hp : p โ  0) (hq : q โ  0) (x : ๐) :
(AddCircle.equivAddCircle p q hp hq).symm โx = โ(x * ( * p))
def AddCircle.homeomorphAddCircle {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) (q : ๐) (hp : p โ  0) (hq : q โ  0) :

The rescaling homeomorphism between additive circles with different periods.

Equations
Instances For
@[simp]
theorem AddCircle.homeomorphAddCircle_apply_mk {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) (q : ๐) (hp : p โ  0) (hq : q โ  0) (x : ๐) :
() โx = โ(x * ( * q))
@[simp]
theorem AddCircle.homeomorphAddCircle_symm_apply_mk {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) (q : ๐) (hp : p โ  0) (hq : q โ  0) (x : ๐) :
().symm โx = โ(x * ( * p))
@[simp]
theorem AddCircle.coe_equivIco_mk_apply {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] [FloorRing ๐] (x : ๐) :
โ(() โx) = Int.fract (x / p) * p
instance AddCircle.instDivisibleByInt {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] [FloorRing ๐] :
Equations
• = { div := fun (x : ) (n : โค) => โ((โn)โปยน * โ(() x)), div_zero := โฏ, div_cancel := โฏ }
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) :
m.gcd 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 : m.gcd 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 : m.natAbs.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} [] [TopologicalSpace ๐] [OrderTopology ๐] {p : ๐} [hp : Fact (0 < p)] {u : } {n : โ} (h : 0 < n) :
= n โ โ m < n, m.gcd n = 1 โง โ(โm / โn * p) = u
theorem AddCircle.exists_gcd_eq_one_of_isOfFinAddOrder {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] {p : ๐} [hp : Fact (0 < p)] {u : } (h : ) :
โ (m : โ), m.gcd () = 1 โง m < โง โ(โm / โ() * p) = u
def AddCircle.setAddOrderOfEquiv {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] {n : โ} (hn : 0 < n) :
โ{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 : AddCircle p) where m is coprime to n and satisfies 0 โค m < n.

Equations
Instances For
@[simp]
theorem AddCircle.card_addOrderOf_eq_totient {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] {n : โ} :
Nat.card { u : // = n } = n.totient
theorem AddCircle.finite_setOf_add_order_eq {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) [hp : Fact (0 < p)] {n : โ} (hn : 0 < n) :
{u : | = n}.Finite
Equations
• โฏ = โฏ
instance AddCircle.compactSpace (p : โ) [Fact (0 < p)] :

The "additive circle" โ โงธ (โค โ p) is compact.

Equations
• โฏ = โฏ

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

Equations
• โฏ = โฏ
instance instZeroLTOne {๐ : Type u_1} [] :
Fact (0 < 1)
Equations
• โฏ = โฏ
@[reducible, inline]

The unit circle โ โงธ โค.

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

• mk: โ {๐ : Type u_1} [inst : ] {p a : ๐} [hp : Fact (0 < p)], AddCircle.EndpointIdent p a โจa, โฏโฉ โจa + p, โฏโฉ
Instances For
def AddCircle.equivIccQuot {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) (a : ๐) [hp : Fact (0 < p)] [Archimedean ๐] :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddCircle.equivIccQuot_comp_mk_eq_toIcoMod {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) (a : ๐) [hp : Fact (0 < p)] [Archimedean ๐] :
โ() โ Quotient.mk'' = fun (x : ๐) => Quot.mk () โจtoIcoMod โฏ a x, โฏโฉ
theorem AddCircle.equivIccQuot_comp_mk_eq_toIocMod {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) (a : ๐) [hp : Fact (0 < p)] [Archimedean ๐] :
โ() โ Quotient.mk'' = fun (x : ๐) => Quot.mk () โจtoIocMod โฏ a x, โฏโฉ
def AddCircle.homeoIccQuot {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] (p : ๐) (a : ๐) [hp : Fact (0 < p)] [Archimedean ๐] :

The natural map from [a, a + p] โ ๐ with endpoints identified to ๐ / โค โข p, as a homeomorphism of topological spaces.

Equations
• = { toEquiv := , continuous_toFun := โฏ, continuous_invFun := โฏ }
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} [] [TopologicalSpace ๐] [OrderTopology ๐] {p : ๐} {a : ๐} [hp : Fact (0 < p)] [Archimedean ๐] {f : ๐ โ B} (h : f a = f (a + p)) :
= Quot.lift ((Set.Icc a (a + p)).restrict f) โฏ โ โ()
theorem AddCircle.liftIco_continuous {๐ : Type u_1} {B : Type u_2} [] [TopologicalSpace ๐] [OrderTopology ๐] {p : ๐} {a : ๐} [hp : Fact (0 < p)] [Archimedean ๐] [] {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} [] [TopologicalSpace ๐] [OrderTopology ๐] {p : ๐} [hp : Fact (0 < p)] [Archimedean ๐] {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} [] [TopologicalSpace ๐] [OrderTopology ๐] {p : ๐} [hp : Fact (0 < p)] [Archimedean ๐] [] {f : ๐ โ B} (hf : f 0 = f p) (hc : ContinuousOn f (Set.Icc 0 p)) :
noncomputable def ZMod.toAddCircle {N : โ} [] :

The AddMonoidHom from ZMod N to โ / โค sending j mod N to j / N mod 1.

Equations
Instances For
theorem ZMod.toAddCircle_intCast {N : โ} [] (j : โค) :
ZMod.toAddCircle โj = โ(โj / โN)
theorem ZMod.toAddCircle_natCast {N : โ} [] (j : โ) :
ZMod.toAddCircle โj = โ(โj / โN)
theorem ZMod.toAddCircle_apply {N : โ} [] (j : ZMod N) :
ZMod.toAddCircle j = โ(โj.val / โN)

Explicit formula for toCircle j. Note that this is "evil" because it uses ZMod.val. Where possible, it is recommended to lift j to โค and use toAddCircle_intCast instead.

theorem ZMod.toAddCircle_injective (N : โ) [] :