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 periodp : 𝕜
UnitAddCircle
: the special caseℝ ⧸ ℤ
AddCircle.equivAddCircle
: the rescaling equivalenceAddCircle p ≃+ AddCircle q
AddCircle.equivIco
: the natural equivalenceAddCircle p ≃ Ico a (a + p)
AddCircle.addOrderOf_div_of_gcd_eq_one
: rational points have finite orderAddCircle.exists_gcd_eq_one_of_isOfFinAddOrder
: finite-order points are rationalAddCircle.homeoIccQuot
: the natural topological equivalence betweenAddCircle p
andIcc a (a + p)
with its endpoints identified.AddCircle.liftIco_continuous
: iff : ℝ → B
is continuous, andf a = f (a + p)
for somea
, then there is a continuous functionAddCircle p → B
which agrees withf
onIcc 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
The "additive circle": 𝕜 ⧸ (ℤ ∙ p)
. See also Circle
and Real.angle
.
Equations
- AddCircle p = (𝕜 ⧸ AddSubgroup.zmultiples p)
Instances For
The equivalence between AddCircle p
and the half-open interval [a, a + p)
, whose inverse
is the natural quotient map.
Equations
Instances For
The equivalence between AddCircle p
and the half-open interval (a, a + p]
, whose inverse
is the natural quotient map.
Equations
Instances For
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)
Instances For
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)
Instances For
The quotient map 𝕜 → AddCircle p
as a partial homeomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The image of the closed-open interval [a, a + p)
under the quotient map 𝕜 → AddCircle p
is
the entire space.
The image of the closed-open interval [a, a + p)
under the quotient map 𝕜 → AddCircle p
is
the entire space.
The image of the closed interval [0, p]
under the quotient map 𝕜 → AddCircle p
is the
entire space.
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)) ⋯
Instances For
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 := ⋯ }
Instances For
Equations
- AddCircle.instDivisibleByInt p = { div := fun (x : AddCircle p) (n : ℤ) => ↑((↑n)⁻¹ * ↑((AddCircle.equivIco p 0) x)), div_zero := ⋯, div_cancel := ⋯ }
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
Instances For
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
- ⋯ = ⋯
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.
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 ⟨a, ⋯⟩ ⟨a + p, ⋯⟩
Instances For
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
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 := ⋯ }
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
.