The additive circle

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 and AddCircle.equivIoc: the natural equivalences AddCircle p ≃ Ico a (a + p) and AddCircle p ≃ Ioc 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 and AddCircle.liftIoc_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

• Link with periodicity
• Lie group structure
• Exponential equivalence to Circle

theorem eventuallyEq_toIcoDiv_nhdsGE {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜) : toIcoDiv hp a =ᶠ[nhdsWithin x (Set.Ici x)] fun (x_1 : 𝕜) => toIcoDiv hp a x

toIcoDiv is eventually constant on the right at every point.

theorem continuousWithinAt_toIcoDiv_Ici {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜) : ContinuousWithinAt (toIcoDiv hp a) (Set.Ici x) x

toIcoDiv is continuous on the right at every point.

In fact, a stronger statement is true: it's eventually constant on the right, see eventuallyEq_toIcoDiv_nhdsGE.

theorem eventuallyEq_toIocDiv_nhdsLE {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜) : toIocDiv hp a =ᶠ[nhdsWithin x (Set.Iic x)] fun (x_1 : 𝕜) => toIocDiv hp a x

toIocDiv is eventually constant on the left at every point.

theorem continuousWithinAt_toIocDiv_Iic {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜) : ContinuousWithinAt (toIocDiv hp a) (Set.Iic x) x

toIocDiv is continuous on the left at every point.

In fact, a stronger statement is true: it's eventually constant on the left, see eventuallyEq_toIocDiv_nhdsLE.

theorem continuousWithinAt_toIcoMod_Ici {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜) : ContinuousWithinAt (toIcoMod hp a) (Set.Ici x) x

toIcoMod is continuous on the right at every point.

@[deprecated continuousWithinAt_toIcoMod_Ici (since := "2026-01-04")]

theorem continuous_right_toIcoMod {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜) : ContinuousWithinAt (toIcoMod hp a) (Set.Ici x) x

Alias of continuousWithinAt_toIcoMod_Ici.

---

toIcoMod is continuous on the right at every point.

theorem continuousWithinAt_toIocMod_Iic {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜) : ContinuousWithinAt (toIocMod hp a) (Set.Iic x) x

toIocMod is continuous on the right at every point.

@[deprecated continuousWithinAt_toIocMod_Iic (since := "2026-01-04")]

theorem continuous_left_toIocMod {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜) : ContinuousWithinAt (toIocMod hp a) (Set.Iic x) x

Alias of continuousWithinAt_toIocMod_Iic.

---

toIocMod is continuous on the right at every point.

theorem eventuallyEq_toIcoDiv_nhdsLT {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜) : toIcoDiv hp a =ᶠ[nhdsWithin x (Set.Iio x)] fun (x_1 : 𝕜) => toIocDiv hp a x

At every point x, for all y < x sufficiently close to x, we have toIcoDiv hp a y = toIocDiv hp a x.

Note that we use different functions on the LHS and on the RHS.

theorem eventuallyEq_toIocDiv_nhdsGT {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜) : toIocDiv hp a =ᶠ[nhdsWithin x (Set.Ioi x)] fun (x_1 : 𝕜) => toIcoDiv hp a x

At every point x, for all y > x sufficiently close to x, we have toIocDiv hp a y = toIcoDiv hp a x.

Note that we use different functions on the LHS and on the RHS.

theorem eventuallyEq_toIcoDiv_nhds {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : ¬x ≡ a [PMOD p]) : toIcoDiv hp a =ᶠ[nhds x] fun (x_1 : 𝕜) => toIcoDiv hp a x

If x is not congruent to a modulo p, then toIcoDiv is locally constant near x.

theorem continuousAt_toIcoDiv {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : ¬x ≡ a [PMOD p]) : ContinuousAt (toIcoDiv hp a) x

If x is not congruent to a modulo p, then toIcoDiv is continuous at x.

In fact, it is locally near x, see eventuallyEq_toIcoDiv_nhds.

theorem continuousOn_toIcoDiv {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) : ContinuousOn (toIcoDiv hp a) {x : 𝕜 | ¬x ≡ a [PMOD p]}

toIcoDiv is continuous on the set of points that are not congruent to a modulo p.

theorem eventuallyEq_toIocDiv_nhds {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : ¬x ≡ a [PMOD p]) : toIocDiv hp a =ᶠ[nhds x] fun (x_1 : 𝕜) => toIocDiv hp a x

If x is not congruent to a modulo p, then toIocDiv is locally constant near x.

theorem continuousAt_toIocDiv {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : ¬x ≡ a [PMOD p]) : ContinuousAt (toIocDiv hp a) x

If x is not congruent to a modulo p, then toIocDiv is continuous at x.

In fact, it is locally near x, see eventuallyEq_toIocDiv_nhds.

theorem continuousOn_toIocDiv {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) : ContinuousOn (toIocDiv hp a) {x : 𝕜 | ¬x ≡ a [PMOD p]}

toIocDiv is continuous on the set of points that aren't congruent to the endpoint modulo the period.

theorem toIcoMod_eventuallyEq_toIocMod {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : ¬x ≡ a [PMOD p]) : toIcoMod hp a =ᶠ[nhds x] toIocMod hp a

theorem continuousAt_toIcoMod {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : ¬x ≡ a [PMOD p]) : ContinuousAt (toIcoMod hp a) x

theorem continuousAt_toIocMod {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : ¬x ≡ a [PMOD p]) : ContinuousAt (toIocMod hp a) x

@[reducible, inline]

abbrev AddCircle {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) : Type u_1

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

theorem AddCircle.coe_nsmul {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) {n : ℕ} {x : 𝕜} : ↑(n • x) = n • ↑x

theorem AddCircle.coe_zsmul {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) {n : ℤ} {x : 𝕜} : ↑(n • x) = n • ↑x

theorem AddCircle.coe_add {𝕜 : Type u_1} [AddCommGroup 𝕜] (p x y : 𝕜) : ↑(x + y) = ↑x + ↑y

theorem AddCircle.coe_sub {𝕜 : Type u_1} [AddCommGroup 𝕜] (p x y : 𝕜) : ↑(x - y) = ↑x - ↑y

theorem AddCircle.coe_neg {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) {x : 𝕜} : ↑(-x) = -↑x

theorem AddCircle.coe_zero {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) : ↑0 = 0

theorem AddCircle.coe_eq_zero_iff {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) {x : 𝕜} : ↑x = 0 ↔ ∃ (n : ℤ), n • p = x

theorem AddCircle.coe_period {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) : ↑p = 0

theorem AddCircle.coe_add_period {𝕜 : Type u_1} [AddCommGroup 𝕜] (p x : 𝕜) : ↑(x + p) = ↑x

theorem AddCircle.continuous_mk' {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [TopologicalSpace 𝕜] : Continuous ⇑(QuotientAddGroup.mk' (AddSubgroup.zmultiples p))

theorem AddCircle.card_torsion_le_of_isSMulRegular {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) (n : ℕ) (h0 : n ≠ 0) (hn : IsSMulRegular 𝕜 n) : {x : AddCircle p | n • x = 0}.encard ≤ ↑n

theorem AddCircle.finite_torsion_of_isSMulRegular {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) (n : ℕ) (hn : IsSMulRegular 𝕜 n) : {x : AddCircle p | n • x = 0}.Finite

theorem AddCircle.card_torsion_le_of_isSMulRegular_int {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) (n : ℤ) (h0 : n ≠ 0) (hn : IsSMulRegular 𝕜 n) : {x : AddCircle p | n • x = 0}.encard ≤ ↑n.natAbs

theorem AddCircle.finite_torsion_of_isSMulRegular_int {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) (n : ℤ) (hn : IsSMulRegular 𝕜 n) : {x : AddCircle p | n • x = 0}.Finite

theorem AddCircle.finite_torsion {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {n : ℕ} (hn : 0 < n) : {u : AddCircle p | n • u = 0}.Finite

theorem AddCircle.finite_setOf_addOrderOf_eq {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {n : ℕ} (hn : 0 < n) : {u : AddCircle p | addOrderOf u = n}.Finite

theorem AddCircle.coe_eq_zero_of_pos_iff {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] (hp : 0 < p) {x : 𝕜} (hx : 0 < x) : ↑x = 0 ↔ ∃ (n : ℕ), n • p = x

def AddCircle.equivIco {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] : AddCircle p ≃ ↑(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.

def AddCircle.equivIoc {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] : AddCircle p ≃ ↑(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.

def AddCircle.liftIco {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] (f : 𝕜 → B) : AddCircle p → B

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

def AddCircle.liftIoc {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] (f : 𝕜 → B) : AddCircle p → B

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

theorem AddCircle.equivIco_coe_eq {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {x : 𝕜} (hx : x ∈ Set.Ico a (a + p)) : (equivIco p a) ↑x = ⟨x, hx⟩

theorem AddCircle.equivIoc_coe_eq {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {x : 𝕜} (hx : x ∈ Set.Ioc a (a + p)) : (equivIoc p a) ↑x = ⟨x, hx⟩

theorem AddCircle.coe_eq_coe_iff_of_mem_Ico {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [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} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Set.Ico a (a + p)) : liftIco p a f ↑x = f x

theorem AddCircle.liftIoc_coe_apply {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Set.Ioc a (a + p)) : liftIoc p a f ↑x = f x

theorem AddCircle.liftIco_comp_apply {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] {α : Type u_3} {β : Type u_4} {f : 𝕜 → α} {g : α → β} {a : 𝕜} {x : AddCircle p} : liftIco p a (g ∘ f) x = g (liftIco p a f x)

theorem AddCircle.liftIoc_comp_apply {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] {α : Type u_3} {β : Type u_4} {f : 𝕜 → α} {g : α → β} {a : 𝕜} {x : AddCircle p} : liftIoc p a (g ∘ f) x = g (liftIoc p a f x)

theorem AddCircle.eq_coe_Ico {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] (a : AddCircle p) : ∃ b ∈ Set.Ico 0 p, ↑b = a

theorem AddCircle.coe_eq_zero_iff_of_mem_Ico {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] (ha : a ∈ Set.Ico 0 p) : ↑a = 0 ↔ a = 0

theorem AddCircle.continuous_equivIco_symm {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] : Continuous ⇑(equivIco p a).symm

theorem AddCircle.continuous_equivIoc_symm {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] : Continuous ⇑(equivIoc p a).symm

theorem AddCircle.continuousAt_equivIco {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {x : AddCircle p} (hx : x ≠ ↑a) : ContinuousAt (⇑(equivIco p a)) x

theorem AddCircle.continuousAt_equivIoc {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {x : AddCircle p} (hx : x ≠ ↑a) : ContinuousAt (⇑(equivIoc p a)) x

def AddCircle.openPartialHomeomorphCoe {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] : OpenPartialHomeomorph 𝕜 (AddCircle p)

The quotient map 𝕜 → AddCircle p as an open partial homeomorphism.

@[simp]

theorem AddCircle.openPartialHomeomorphCoe_symm_apply {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] (x : AddCircle p) : ↑(openPartialHomeomorphCoe p a).symm x = ↑((equivIco p a) x)

@[simp]

theorem AddCircle.openPartialHomeomorphCoe_source {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] : (openPartialHomeomorphCoe p a).source = Set.Ioo a (a + p)

@[simp]

theorem AddCircle.openPartialHomeomorphCoe_target {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] : (openPartialHomeomorphCoe p a).target = {↑a}ᶜ

@[simp]

theorem AddCircle.openPartialHomeomorphCoe_apply {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] (a✝ : 𝕜) : ↑(openPartialHomeomorphCoe p a) a✝ = ↑a✝

@[deprecated AddCircle.openPartialHomeomorphCoe (since := "2025-08-29")]

def AddCircle.partialHomeomorphCoe {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] : OpenPartialHomeomorph 𝕜 (AddCircle p)

Alias of AddCircle.openPartialHomeomorphCoe.

---

The quotient map 𝕜 → AddCircle p as an open partial homeomorphism.

@[simp]

theorem AddCircle.coe_image_Ico_eq {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [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} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [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} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [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.

theorem AddCircle.Ico_ext {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] {α : Type u_3} {f g : AddCircle p → α} (a : 𝕜) (h : ∀ x ∈ Set.Ico a (a + p), f ↑x = g ↑x) : f = g

If functions on AddCircle agree on the image of the interval [a, a + p) then they are equal

theorem AddCircle.Ioc_ext {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] {α : Type u_3} {f g : AddCircle p → α} (a : 𝕜) (h : ∀ x ∈ Set.Ioc a (a + p), f ↑x = g ↑x) : f = g

If functions on AddCircle agree on the image of the interval (a, a + p] then they are equal

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

The rescaling equivalence between additive circles with different periods.

@[simp]

theorem AddCircle.equivAddCircle_apply_mk {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) : (equivAddCircle p q hp hq) ↑x = ↑(x * (p⁻¹ * q))

@[simp]

theorem AddCircle.equivAddCircle_symm_apply_mk {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) : (equivAddCircle p q hp hq).symm ↑x = ↑(x * (q⁻¹ * p))

def AddCircle.homeomorphAddCircle {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (hp : p ≠ 0) (hq : q ≠ 0) : AddCircle p ≃ₜ AddCircle q

The rescaling homeomorphism between additive circles with different periods.

@[simp]

theorem AddCircle.homeomorphAddCircle_apply_mk {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) : (homeomorphAddCircle p q hp hq) ↑x = ↑(x * (p⁻¹ * q))

@[simp]

theorem AddCircle.homeomorphAddCircle_symm_apply_mk {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) : (homeomorphAddCircle p q hp hq).symm ↑x = ↑(x * (q⁻¹ * p))

theorem AddCircle.natCast_div_mul_eq_nsmul {𝕜 : Type u_1} [Field 𝕜] (p q r : 𝕜) (m : ℕ) : ↑(↑m / q * r) = m • ↑(r / q)

theorem AddCircle.intCast_div_mul_eq_zsmul {𝕜 : Type u_1} [Field 𝕜] (p q r : 𝕜) (m : ℤ) : ↑(↑m / q * r) = m • ↑(r / q)

@[simp]

theorem AddCircle.coe_equivIco_mk_apply {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] [FloorRing 𝕜] (x : 𝕜) : ↑((equivIco p 0) ↑x) = Int.fract (x / p) * p

instance AddCircle.instDivisibleByInt {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] [FloorRing 𝕜] : DivisibleBy (AddCircle p) ℤ

@[simp]

theorem AddCircle.coe_fract {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [FloorRing 𝕜] (x : 𝕜) : ↑(Int.fract x) = ↑x

theorem AddCircle.addOrderOf_period_div {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {n : ℕ} (h : 0 < n) : addOrderOf ↑(p / ↑n) = n

theorem AddCircle.gcd_mul_addOrderOf_div_eq {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {q : ℚ} : addOrderOf ↑(↑q * p) = q.den

theorem AddCircle.nsmul_eq_zero_iff {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {u : AddCircle p} {n : ℕ} (h : 0 < n) : n • u = 0 ↔ ∃ m < n, ↑(↑m / ↑n * p) = u

theorem AddCircle.addOrderOf_eq_pos_iff {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {u : AddCircle p} {n : ℕ} (h : 0 < n) : addOrderOf u = n ↔ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u

theorem AddCircle.exists_gcd_eq_one_of_isOfFinAddOrder {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {u : AddCircle p} (h : IsOfFinAddOrder u) : ∃ (m : ℕ), m.gcd (addOrderOf u) = 1 ∧ m < addOrderOf u ∧ ↑(↑m / ↑(addOrderOf u) * p) = u

theorem AddCircle.not_isOfFinAddOrder_iff_forall_rat_ne_div {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {a : 𝕜} : ¬IsOfFinAddOrder ↑a ↔ ∀ (q : ℚ), ↑q ≠ a / p

theorem AddCircle.isOfFinAddOrder_iff_exists_rat_eq_div {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {a : 𝕜} : IsOfFinAddOrder ↑a ↔ ∃ (q : ℚ), ↑q = a / p

def AddCircle.setAddOrderOfEquiv {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {n : ℕ} (hn : 0 < n) : ↑{u : AddCircle p | addOrderOf 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.

@[simp]

theorem AddCircle.card_addOrderOf_eq_totient {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {n : ℕ} : Nat.card { u : AddCircle p // addOrderOf u = n } = n.totient

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} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] (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} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] : EndpointIdent p a ⟨a, ⋯⟩ ⟨a + p, ⋯⟩

def AddCircle.equivIccQuot {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] (p a : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] : AddCircle p ≃ Quot (EndpointIdent p a)

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

theorem AddCircle.equivIccQuot_comp_mk_eq_toIcoMod {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] (p a : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] : ⇑(equivIccQuot p a) ∘ Quotient.mk'' = fun (x : 𝕜) => Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩

theorem AddCircle.equivIccQuot_comp_mk_eq_toIocMod {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] (p a : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] : ⇑(equivIccQuot p a) ∘ Quotient.mk'' = fun (x : 𝕜) => Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

def AddCircle.homeoIccQuot {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] (p a : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : AddCircle p ≃ₜ Quot (EndpointIdent p a)

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

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, by first showing that various lifts are equivalent.

theorem AddCircle.liftIoc_eq_liftIco {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] {f : 𝕜 → B} (hf : f a = f (a + p)) : liftIoc p a f = liftIco p a f

theorem AddCircle.liftIco_eq_lift_Icc {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] {f : 𝕜 → B} (h : f a = f (a + p)) : liftIco p a f = Quot.lift ((Set.Icc a (a + p)).restrict f) ⋯ ∘ ⇑(equivIccQuot p a)

theorem AddCircle.liftIoc_eq_lift_Icc {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] {f : 𝕜 → B} (h : f a = f (a + p)) : liftIoc p a f = Quot.lift ((Set.Icc a (a + p)).restrict f) ⋯ ∘ ⇑(equivIccQuot p a)

theorem AddCircle.liftIco_zero_coe_apply {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Set.Ico 0 p) : liftIco p 0 f ↑x = f x

theorem AddCircle.liftIoc_zero_coe_apply {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Set.Ioc 0 p) : liftIoc p 0 f ↑x = f x

theorem AddCircle.liftIco_continuous {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [TopologicalSpace B] {f : 𝕜 → B} (hf : f a = f (a + p)) (hc : ContinuousOn f (Set.Icc a (a + p))) : Continuous (liftIco p a f)

theorem AddCircle.liftIco_zero_continuous {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [TopologicalSpace B] {f : 𝕜 → B} (hf : f 0 = f p) (hc : ContinuousOn f (Set.Icc 0 p)) : Continuous (liftIco p 0 f)

theorem AddCircle.liftIoc_continuous {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [TopologicalSpace B] {f : 𝕜 → B} (hf : f a = f (a + p)) (hc : ContinuousOn f (Set.Icc a (a + p))) : Continuous (liftIoc p a f)

theorem AddCircle.liftIoc_zero_continuous {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [TopologicalSpace B] {f : 𝕜 → B} (hf : f 0 = f p) (hc : ContinuousOn f (Set.Icc 0 p)) : Continuous (liftIoc p 0 f)