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

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

instance instAddCommGroupAddCircle {𝕜 : Type u_1} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) : AddCommGroup (AddCircle p)

Equations

• instAddCommGroupAddCircle p = inferInstanceAs (AddCommGroup (𝕜 ⧸ AddSubgroup.zmultiples p))

instance instTopologicalSpaceAddCircle {𝕜 : Type u_1} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) : TopologicalSpace (AddCircle p)

Equations

• instTopologicalSpaceAddCircle p = inferInstanceAs (TopologicalSpace (𝕜 ⧸ AddSubgroup.zmultiples p))

instance instTopologicalAddGroupAddCircleInstTopologicalSpaceAddCircleToAddGroupInstAddCommGroupAddCircle {𝕜 : Type u_1} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) : TopologicalAddGroup (AddCircle p)

Equations

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

instance instInhabitedAddCircle {𝕜 : Type u_1} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) : Inhabited (AddCircle p)

Equations

• instInhabitedAddCircle p = inferInstanceAs (Inhabited (𝕜 ⧸ AddSubgroup.zmultiples p))

instance instCoeAddCircle {𝕜 : Type u_1} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) : Coe 𝕜 (AddCircle p)

Equations

• instCoeAddCircle p = { coe := QuotientAddGroup.mk }

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

instance AddCircle.instCircularOrderAddCircle {𝕜 : Type u_1} [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] : CircularOrder (AddCircle p)

Equations

• AddCircle.instCircularOrderAddCircle p = QuotientAddGroup.circularOrder

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 (_ : 0 < p) 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 (_ : 0 < p) 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.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.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

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

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

@[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.instDivisibleByAddCircleToLinearOrderedAddCommGroupToLinearOrderedRingToLinearOrderedCommRingIntToAddMonoidToSubNegMonoidToAddGroupInstAddCommGroupAddCircleSMulIntToZeroToCommMonoidWithZeroInstCommSemiringInt {𝕜 : 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, 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 | 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

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

@[simp]

theorem AddCircle.card_addOrderOf_eq_totient {𝕜 : Type u_1} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) [hp : Fact (0 < p)] {n : ℕ} : Nat.card { u // 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 | addOrderOf u = n}

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

Equations

• AddCircle.pathConnectedSpace = AddCircle.pathConnectedSpace.proof_1

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

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

Equations

• AddCircle.compactSpace = AddCircle.compactSpace.proof_1

instance AddCircle.instProperlyDiscontinuousVAddSubtypeAddOppositeRealMemAddSubgroupAddGroupInstAddGroupRealInstMembershipInstSetLikeAddSubgroupOpZmultiplesToTopologicalSpaceToUniformSpacePseudoMetricSpaceVaddToAddZeroClassToAddMonoidToSubNegMonoidToHasOppositeVAddInstAddRealToAddSubmonoid (p : ℝ) : ProperlyDiscontinuousVAdd { x // x ∈ 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

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

instance AddCircle.instT2SpaceAddCircleRealInstLinearOrderedAddCommGroupRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstOrderTopologyRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstPreorderRealInstTopologicalSpaceAddCircle (p : ℝ) : T2Space (AddCircle p)

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

Equations

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

instance AddCircle.instT4SpaceAddCircleRealInstLinearOrderedAddCommGroupRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstOrderTopologyRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstPreorderRealInstTopologicalSpaceAddCircle (p : ℝ) [Fact (0 < p)] : T4Space (AddCircle p)

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

Equations

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

instance AddCircle.instSecondCountableTopologyAddCircleRealInstLinearOrderedAddCommGroupRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstOrderTopologyRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstPreorderRealInstTopologicalSpaceAddCircle (p : ℝ) : TopologicalSpace.SecondCountableTopology (AddCircle p)

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

Equations

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

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

• mk: ∀ {𝕜 : Type u_1} [inst : LinearOrderedAddCommGroup 𝕜] {p a : 𝕜} [hp : Fact (0 < p)], AddCircle.EndpointIdent p a { val := a, property := (_ : a ∈ Set.Icc a (a + p)) } { val := a + p, property := (_ : a + p ∈ Set.Icc a (a + p)) }

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

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 (_ : 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} [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 (_ : 0 < p) a x, property := (_ : toIocMod (_ : 0 < p) a x ∈ Set.Icc a (a + p)) }

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 = Homeomorph.mk (AddCircle.equivIccQuot p a)

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) (_ : ∀ (a b : ↑(Set.Icc a (a + p))), AddCircle.EndpointIdent p a a b → Set.restrict (Set.Icc a (a + p)) f a = Set.restrict (Set.Icc a (a + p)) f b) ∘ ↑(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)