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} [LinearOrderedAddCommGroup 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) (x : 𝕜) : ContinuousWithinAt (toIcoMod hp a) (Set.Ici x) x

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

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

theorem continuousAt_toIocMod {𝕜 : Type u_1} [LinearOrderedAddCommGroup 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : ↑x ≠ ↑a) : ContinuousAt (toIocMod hp a) x

@[inline, reducible]

abbrev AddCircle {𝕜 : Type u_1} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (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} [LinearOrderedAddCommGroup 𝕜] (p : 𝕜) {n : ℕ} {x : 𝕜} : ↑(n • x) = n • ↑x

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

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

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

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

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

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

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

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

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

def AddCircle.equivIco {𝕜 : Type u_1} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) [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} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) [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} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) [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.restrict (Set.Ico a (a + p)) f ∘ ⇑(AddCircle.equivIco p a)

def AddCircle.liftIoc {𝕜 : Type u_1} {B : Type u_2} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) [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.restrict (Set.Ioc a (a + p)) f ∘ ⇑(AddCircle.equivIoc p a)

theorem AddCircle.coe_eq_coe_iff_of_mem_Ico {𝕜 : Type u_1} [LinearOrderedAddCommGroup 𝕜] [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} [LinearOrderedAddCommGroup 𝕜] [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} [LinearOrderedAddCommGroup 𝕜] [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} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} [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} [LinearOrderedAddCommGroup 𝕜] [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} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] : Continuous ⇑(AddCircle.equivIco p a).symm

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def AddCircle.partialHomeomorphCoe {𝕜 : Type u_1} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [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.

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

@[simp]

theorem AddCircle.coe_image_Ico_eq {𝕜 : Type u_1} [LinearOrderedAddCommGroup 𝕜] [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} [LinearOrderedAddCommGroup 𝕜] [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} [LinearOrderedAddCommGroup 𝕜] [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} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (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} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (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} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) (q : 𝕜) (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) : (AddEquiv.symm (AddCircle.equivAddCircle p q hp hq)) ↑x = ↑(x * (q⁻¹ * p))

def AddCircle.homeomorphAddCircle {𝕜 : Type u_1} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) (q : 𝕜) (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} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) (q : 𝕜) (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) : (AddCircle.homeomorphAddCircle p q hp hq) ↑x = ↑(x * (p⁻¹ * q))

@[simp]

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

@[simp]

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

instance AddCircle.instDivisibleByAddCircleToLinearOrderedAddCommGroupToLinearOrderedRingToLinearOrderedCommRingIntToAddMonoidToSubNegMonoidAddGroupToAddGroupToAddCommGroupToOrderedAddCommGroupZmultiplesNormal_of_commToAddCommGroupToRingToDivisionRingToFieldSMulIntToZeroToCommMonoidWithZeroInstCommSemiring {𝕜 : Type u_1} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) [hp : Fact (0 < p)] [FloorRing 𝕜] : DivisibleBy (AddCircle p) ℤ

Equations

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

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

theorem AddCircle.gcd_mul_addOrderOf_div_eq {𝕜 : Type u_1} [LinearOrderedField 𝕜] (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} [LinearOrderedField 𝕜] {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} [LinearOrderedField 𝕜] {p : 𝕜} [hp : Fact (0 < p)] {m : ℤ} {n : ℕ} (hn : 0 < n) (h : Nat.gcd (Int.natAbs m) n = 1) : addOrderOf ↑(↑m / ↑n * p) = n

theorem AddCircle.addOrderOf_coe_rat {𝕜 : Type u_1} [LinearOrderedField 𝕜] {p : 𝕜} [hp : Fact (0 < p)] {q : ℚ} : addOrderOf ↑(↑q * p) = q.den

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

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

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

Equations

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

@[simp]

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

theorem AddCircle.finite_setOf_add_order_eq {𝕜 : Type u_1} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) [hp : Fact (0 < p)] {n : ℕ} (hn : 0 < n) : Set.Finite {u : AddCircle p | addOrderOf u = n}

instance AddCircle.pathConnectedSpace (p : ℝ) : PathConnectedSpace (AddCircle p)

Equations

• ⋯ = ⋯

instance AddCircle.compactSpace (p : ℝ) [Fact (0 < p)] : CompactSpace (AddCircle p)

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

Equations

• ⋯ = ⋯

instance AddCircle.instProperlyDiscontinuousVAddSubtypeAddOppositeRealMemAddSubgroupInstAddGroupInstAddGroupRealInstMembershipInstSetLikeAddSubgroupOpZmultiplesToTopologicalSpaceToUniformSpacePseudoMetricSpaceVaddToAddZeroClassToAddMonoidToSubNegMonoidToHasOppositeVAddInstAddRealToAddSubmonoid (p : ℝ) : ProperlyDiscontinuousVAdd ↥(AddSubgroup.op (AddSubgroup.zmultiples p)) ℝ

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} [StrictOrderedSemiring 𝕜] : Fact (0 < 1)

Equations

• ⋯ = ⋯

@[inline, reducible]

abbrev UnitAddCircle : Type

The unit circle ℝ ⧸ ℤ.

Equations

• UnitAddCircle = AddCircle 1

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} [LinearOrderedAddCommGroup 𝕜] (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 : LinearOrderedAddCommGroup 𝕜] {p a : 𝕜} [hp : Fact (0 < p)], AddCircle.EndpointIdent p a { val := a, property := ⋯ } { val := a + p, property := ⋯ }

def AddCircle.equivIccQuot {𝕜 : Type u_1} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) (a : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] : AddCircle p ≃ Quot (AddCircle.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} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) (a : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] : ⇑(AddCircle.equivIccQuot p a) ∘ Quotient.mk'' = fun (x : 𝕜) => Quot.mk (AddCircle.EndpointIdent p a) { val := toIcoMod ⋯ a x, property := ⋯ }

theorem AddCircle.equivIccQuot_comp_mk_eq_toIocMod {𝕜 : Type u_1} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) (a : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] : ⇑(AddCircle.equivIccQuot p a) ∘ Quotient.mk'' = fun (x : 𝕜) => Quot.mk (AddCircle.EndpointIdent p a) { val := toIocMod ⋯ a x, property := ⋯ }

def AddCircle.homeoIccQuot {𝕜 : Type u_1} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) (a : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] : AddCircle p ≃ₜ Quot (AddCircle.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} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} {a : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] {f : 𝕜 → B} (h : f a = f (a + p)) : AddCircle.liftIco p a f = Quot.lift (Set.restrict (Set.Icc a (a + p)) f) ⋯ ∘ ⇑(AddCircle.equivIccQuot p a)

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

theorem AddCircle.liftIco_zero_coe_apply {𝕜 : Type u_1} {B : Type u_2} [LinearOrderedAddCommGroup 𝕜] [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} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace B] {f : 𝕜 → B} (hf : f 0 = f p) (hc : ContinuousOn f (Set.Icc 0 p)) : Continuous (AddCircle.liftIco p 0 f)