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
- AddCircle.equivIco p a = QuotientAddGroup.equivIcoMod โฏ a
Instances For
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
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.
The action on โ
by right multiplication of its the subgroup zmultiples p
(the multiples of
p:โ
) is properly discontinuous.
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
.
The AddMonoidHom
from ZMod N
to โ / โค
sending j mod N
to j / N mod 1
.
Equations
- ZMod.toAddCircle = (ZMod.lift N) โจAddMonoidHom.mk' (fun (j : โค) => โ(โj / โN)) โฏ, โฏโฉ
Instances For
Explicit formula for toCircle j
. Note that this is "evil" because it uses ZMod.val
. Where
possible, it is recommended to lift j
to โค
and use toAddCircle_intCast
instead.