The additive circle #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define the additive circle add_circle p
as the quotient π β§Έ (β€ β p)
for some period p : π
.
See also circle
and real.angle
. For the normed group structure on add_circle
, see
add_circle.normed_add_comm_group
in a later file.
Main definitions and results: #
add_circle
: the additive circleπ β§Έ (β€ β p)
for some periodp : π
unit_add_circle
: the special caseβ β§Έ β€
add_circle.equiv_add_circle
: the rescaling equivalenceadd_circle p β+ add_circle q
add_circle.equiv_Ico
: the natural equivalenceadd_circle p β Ico a (a + p)
add_circle.add_order_of_div_of_gcd_eq_one
: rational points have finite orderadd_circle.exists_gcd_eq_one_of_is_of_fin_add_order
: finite-order points are rationaladd_circle.homeo_Icc_quot
: the natural topological equivalence betweenadd_circle p
andIcc a (a + p)
with its endpoints identified.add_circle.lift_Ico_continuous
: iff : β β B
is continuous, andf a = f (a + p)
for somea
, then there is a continuous functionadd_circle 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 add_circle (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
- add_circle p = (π β§Έ add_subgroup.zmultiples p)
Instances for add_circle
- add_circle.add_comm_group
- add_circle.topological_space
- add_circle.topological_add_group
- add_circle.inhabited
- add_circle.has_coe_t
- add_circle.circular_order
- add_circle.int.divisible_by
- add_circle.compact_space
- add_circle.t2_space
- add_circle.normal_space
- add_circle.topological_space.second_countable_topology
- unit_add_circle.compact_space
- unit_add_circle.normal_space
- unit_add_circle.second_countable_topology
- add_circle.normed_add_comm_group
- add_circle.measurable_space
- add_circle.borel_space
- add_circle.measure_space
- unit_add_circle.measure_space
The equivalence between add_circle p
and the half-open interval [a, a + p)
, whose inverse
is the natural quotient map.
Equations
The equivalence between add_circle p
and the half-open interval (a, a + p]
, whose inverse
is the natural quotient map.
Equations
Given a function on π
, return the unique function on add_circle p
agreeing with f
on
[a, a + p)
.
Equations
- add_circle.lift_Ico p a f = (set.Ico a (a + p)).restrict f β β(add_circle.equiv_Ico p a)
Given a function on π
, return the unique function on add_circle p
agreeing with f
on
(a, a + p]
.
Equations
- add_circle.lift_Ioc p a f = (set.Ioc a (a + p)).restrict f β β(add_circle.equiv_Ioc p a)
The image of the closed-open interval [a, a + p)
under the quotient map π β add_circle p
is
the entire space.
The image of the closed-open interval [a, a + p)
under the quotient map π β add_circle p
is
the entire space.
The image of the closed interval [0, p]
under the quotient map π β add_circle p
is the
entire space.
The rescaling equivalence between additive circles with different periods.
Equations
- add_circle.equiv_add_circle p q hp hq = quotient_add_group.congr (add_subgroup.zmultiples p) (add_subgroup.zmultiples q) (add_aut.mul_right ((units.mk0 p hp)β»ΒΉ * units.mk0 q hq)) _
Equations
- add_circle.int.divisible_by p = {div := Ξ» (x : add_circle p) (n : β€), β((βn)β»ΒΉ * β(β(add_circle.equiv_Ico 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 : add_circle p)
where m
is coprime to n
and
satisfies 0 β€ m < n
.
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 "additive circle" β β§Έ (β€ β p)
is Hausdorff.
The "additive circle" β β§Έ (β€ β p)
is normal.
The "additive circle" β β§Έ (β€ β p)
is second-countable.
This section proves that for any a
, the natural map from [a, a + p] β π
to add_circle p
gives an identification of add_circle p
, as a topological space, with the quotient of [a, a + p]
by the equivalence relation identifying the endpoints.
- mk : β {π : Type u_1} [_inst_1 : linear_ordered_add_comm_group π] [_inst_2 : topological_space π] [_inst_3 : order_topology π] {p a : π} [hp : fact (0 < p)], add_circle.endpoint_ident p a β¨a, _β© β¨a + p, _β©
The relation identifying the endpoints of Icc a (a + p)
.
The equivalence between add_circle p
and the quotient of [a, a + p]
by the relation
identifying the endpoints.
Equations
- add_circle.equiv_Icc_quot p a = {to_fun := Ξ» (x : add_circle p), quot.mk (add_circle.endpoint_ident p a) (set.inclusion _ (β(add_circle.equiv_Ico p a) x)), inv_fun := Ξ» (x : quot (add_circle.endpoint_ident p a)), x.lift_on coe _, left_inv := _, right_inv := _}
The natural map from [a, a + p] β π
with endpoints identified to π / β€ β’ p
, as a
homeomorphism of topological spaces.
Equations
- add_circle.homeo_Icc_quot p a = {to_equiv := add_circle.equiv_Icc_quot p a _inst_4, continuous_to_fun := _, continuous_inv_fun := _}
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 add_circle p
.