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

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

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

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

theorem toIcoMod_eventuallyEq_toIocMod {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : ↑x ≠ ↑a) : 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) : 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) : 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.

Equations

• AddCircle p = (𝕜 ⧸ AddSubgroup.zmultiples p)

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

Equations

• AddCircle.equivIco p a = QuotientAddGroup.equivIcoMod ⋯ a

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.

Equations

• AddCircle.equivIoc p a = QuotientAddGroup.equivIocMod ⋯ a

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

Equations

• AddCircle.liftIco p a f = (Set.Ico a (a + p)).restrict f ∘ ⇑(AddCircle.equivIco p a)

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

Equations

• AddCircle.liftIoc p a f = (Set.Ioc a (a + p)).restrict f ∘ ⇑(AddCircle.equivIoc p a)

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.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.partialHomeomorphCoe {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] : PartialHomeomorph 𝕜 (AddCircle p)

The quotient map 𝕜 → AddCircle p as a partial homeomorphism.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem AddCircle.isLocalHomeomorph_coe {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] [DenselyOrdered 𝕜] : IsLocalHomeomorph QuotientAddGroup.mk

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

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.

Equations

• AddCircle.equivAddCircle p q hp hq = QuotientAddGroup.congr (AddSubgroup.zmultiples p) (AddSubgroup.zmultiples q) (AddAut.mulRight ((Units.mk0 p hp)⁻¹ * Units.mk0 q hq)) ⋯

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

Equations

• AddCircle.homeomorphAddCircle p q hp hq = { toEquiv := ↑(AddCircle.equivAddCircle p q hp hq), continuous_toFun := ⋯, continuous_invFun := ⋯ }

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

Equations

• AddCircle.instDivisibleByInt p = { div := fun (x : AddCircle p) (n : ℤ) => ↑((↑n)⁻¹ * ↑((AddCircle.equivIco p 0) x)), div_zero := ⋯, div_cancel := ⋯ }

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

@[deprecated AddCircle.not_isOfFinAddOrder_iff_forall_rat_ne_div (since := "2025-08-13")]

theorem AddCircle.addOrderOf_coe_eq_zero_iff_forall_rat_ne_div {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {a : 𝕜} : addOrderOf ↑a = 0 ↔ ∀ (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.

Equations

• AddCircle.setAddOrderOfEquiv p hn = (Equiv.ofBijective (fun (m : ↑{m : ℕ | m < n ∧ m.gcd n = 1}) => ⟨↑(↑↑m / ↑n * p), ⋯⟩) ⋯).symm

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

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

@[deprecated AddCircle.finite_setOf_addOrderOf_eq (since := "2025-03-26")]

theorem AddCircle.finite_setOf_add_order_eq {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {n : ℕ} (hn : 0 < n) : {u : AddCircle p | addOrderOf u = n}.Finite

Alias of AddCircle.finite_setOf_addOrderOf_eq.

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

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.

Equations

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

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.

Equations

• AddCircle.homeoIccQuot p a = { toEquiv := AddCircle.equivIccQuot p a, continuous_toFun := ⋯, continuous_invFun := ⋯ }

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