mathlib3 documentation

topology.instances.add_circle

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: #

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 #

theorem continuous_right_to_Ico_mod {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [archimedean π•œ] [topological_space π•œ] [order_topology π•œ] {p : π•œ} (hp : 0 < p) (a x : π•œ) :
theorem continuous_left_to_Ioc_mod {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [archimedean π•œ] [topological_space π•œ] [order_topology π•œ] {p : π•œ} (hp : 0 < p) (a x : π•œ) :
theorem to_Ico_mod_eventually_eq_to_Ioc_mod {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [archimedean π•œ] [topological_space π•œ] [order_topology π•œ] {p : π•œ} (hp : 0 < p) (a : π•œ) {x : π•œ} (hx : ↑x β‰  ↑a) :
theorem continuous_at_to_Ico_mod {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [archimedean π•œ] [topological_space π•œ] [order_topology π•œ] {p : π•œ} (hp : 0 < p) (a : π•œ) {x : π•œ} (hx : ↑x β‰  ↑a) :
theorem continuous_at_to_Ioc_mod {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [archimedean π•œ] [topological_space π•œ] [order_topology π•œ] {p : π•œ} (hp : 0 < p) (a : π•œ) {x : π•œ} (hx : ↑x β‰  ↑a) :
@[protected, instance]
def add_circle.add_comm_group {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) :
@[protected, instance]
def add_circle.topological_space {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) :
@[protected, instance]
def add_circle.has_coe_t {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) :
has_coe_t π•œ (add_circle p)
@[protected, instance]
def add_circle.inhabited {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) :
@[protected, instance]
theorem add_circle.coe_nsmul {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) {n : β„•} {x : π•œ} :
theorem add_circle.coe_zsmul {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) {n : β„€} {x : π•œ} :
theorem add_circle.coe_add {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p x y : π•œ) :
theorem add_circle.coe_sub {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p x y : π•œ) :
theorem add_circle.coe_neg {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) {x : π•œ} :
theorem add_circle.coe_eq_zero_iff {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) {x : π•œ} :
theorem add_circle.coe_eq_zero_of_pos_iff {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) (hp : 0 < p) {x : π•œ} (hx : 0 < x) :
theorem add_circle.coe_period {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) :
@[simp]
theorem add_circle.coe_add_period {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p x : π•œ) :
@[protected, nolint, continuity]
@[protected, instance]
def add_circle.circular_order {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] [archimedean π•œ] :
Equations
noncomputable def add_circle.equiv_Ico {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] (a : π•œ) [archimedean π•œ] :

The equivalence between add_circle p and the half-open interval [a, a + p), whose inverse is the natural quotient map.

Equations
noncomputable def add_circle.equiv_Ioc {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] (a : π•œ) [archimedean π•œ] :

The equivalence between add_circle p and the half-open interval (a, a + p], whose inverse is the natural quotient map.

Equations
noncomputable def add_circle.lift_Ico {π•œ : Type u_1} {B : Type u_2} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] (a : π•œ) [archimedean π•œ] (f : π•œ β†’ B) :

Given a function on π•œ, return the unique function on add_circle p agreeing with f on [a, a + p).

Equations
noncomputable def add_circle.lift_Ioc {π•œ : Type u_1} {B : Type u_2} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] (a : π•œ) [archimedean π•œ] (f : π•œ β†’ B) :

Given a function on π•œ, return the unique function on add_circle p agreeing with f on (a, a + p].

Equations
theorem add_circle.coe_eq_coe_iff_of_mem_Ico {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] {p : π•œ} [hp : fact (0 < p)] {a : π•œ} [archimedean π•œ] {x y : π•œ} (hx : x ∈ set.Ico a (a + p)) (hy : y ∈ set.Ico a (a + p)) :
theorem add_circle.lift_Ico_coe_apply {π•œ : Type u_1} {B : Type u_2} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] {p : π•œ} [hp : fact (0 < p)] {a : π•œ} [archimedean π•œ] {f : π•œ β†’ B} {x : π•œ} (hx : x ∈ set.Ico a (a + p)) :
theorem add_circle.lift_Ioc_coe_apply {π•œ : Type u_1} {B : Type u_2} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] {p : π•œ} [hp : fact (0 < p)] {a : π•œ} [archimedean π•œ] {f : π•œ β†’ B} {x : π•œ} (hx : x ∈ set.Ioc a (a + p)) :
@[continuity]
theorem add_circle.continuous_equiv_Ico_symm {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] (a : π•œ) [archimedean π•œ] :
@[continuity]
theorem add_circle.continuous_equiv_Ioc_symm {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] (a : π•œ) [archimedean π•œ] :
theorem add_circle.continuous_at_equiv_Ico {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] (a : π•œ) [archimedean π•œ] {x : add_circle p} (hx : x β‰  ↑a) :
theorem add_circle.continuous_at_equiv_Ioc {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] (a : π•œ) [archimedean π•œ] {x : add_circle p} (hx : x β‰  ↑a) :
@[simp]
theorem add_circle.coe_image_Ico_eq {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] (a : π•œ) [archimedean π•œ] :

The image of the closed-open interval [a, a + p) under the quotient map π•œ β†’ add_circle p is the entire space.

@[simp]
theorem add_circle.coe_image_Ioc_eq {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] (a : π•œ) [archimedean π•œ] :

The image of the closed-open interval [a, a + p) under the quotient map π•œ β†’ add_circle p is the entire space.

@[simp]
theorem add_circle.coe_image_Icc_eq {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] (a : π•œ) [archimedean π•œ] :

The image of the closed interval [0, p] under the quotient map π•œ β†’ add_circle p is the entire space.

def add_circle.equiv_add_circle {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] (p q : π•œ) (hp : p β‰  0) (hq : q β‰  0) :

The rescaling equivalence between additive circles with different periods.

Equations
@[simp]
theorem add_circle.equiv_add_circle_apply_mk {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] (p q : π•œ) (hp : p β‰  0) (hq : q β‰  0) (x : π•œ) :
@[simp]
theorem add_circle.equiv_add_circle_symm_apply_mk {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] (p q : π•œ) (hp : p β‰  0) (hq : q β‰  0) (x : π•œ) :
@[simp]
theorem add_circle.coe_equiv_Ico_mk_apply {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] [floor_ring π•œ] (x : π•œ) :
@[protected, instance]
noncomputable def add_circle.int.divisible_by {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] [floor_ring π•œ] :
Equations
theorem add_circle.add_order_of_period_div {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] {p : π•œ} [hp : fact (0 < p)] {n : β„•} (h : 0 < n) :
theorem add_circle.gcd_mul_add_order_of_div_eq {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] {n : β„•} (m : β„•) (hn : 0 < n) :
theorem add_circle.add_order_of_div_of_gcd_eq_one {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] {p : π•œ} [hp : fact (0 < p)] {m n : β„•} (hn : 0 < n) (h : m.gcd n = 1) :
theorem add_circle.add_order_of_div_of_gcd_eq_one' {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] {p : π•œ} [hp : fact (0 < p)] {m : β„€} {n : β„•} (hn : 0 < n) (h : m.nat_abs.gcd n = 1) :
theorem add_circle.add_order_of_coe_rat {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] {p : π•œ} [hp : fact (0 < p)] {q : β„š} :
theorem add_circle.add_order_of_eq_pos_iff {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] {p : π•œ} [hp : fact (0 < p)] {u : add_circle p} {n : β„•} (h : 0 < n) :
add_order_of u = n ↔ βˆƒ (m : β„•) (H : m < n), m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u
theorem add_circle.exists_gcd_eq_one_of_is_of_fin_add_order {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] {p : π•œ} [hp : fact (0 < p)] {u : add_circle p} (h : is_of_fin_add_order u) :
noncomputable def add_circle.set_add_order_of_equiv {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] {n : β„•} (hn : 0 < n) :
β†₯{u : add_circle p | add_order_of u = n} ≃ β†₯{m : β„• | m < n ∧ m.gcd 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 : add_circle p) where m is coprime to n and satisfies 0 ≀ m < n.

Equations
@[simp]
theorem add_circle.card_add_order_of_eq_totient {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] {n : β„•} :
theorem add_circle.finite_set_of_add_order_eq {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] {n : β„•} (hn : 0 < n) :
@[protected, instance]

The "additive circle" ℝ β§Έ (β„€ βˆ™ p) is compact.

@[protected, instance]

The action on ℝ by right multiplication of its the subgroup zmultiples p (the multiples of p:ℝ) is properly discontinuous.

@[protected, instance]

The "additive circle" ℝ β§Έ (β„€ βˆ™ p) is Hausdorff.

@[protected, instance]

The "additive circle" ℝ β§Έ (β„€ βˆ™ p) is normal.

@[protected, instance]

The "additive circle" ℝ β§Έ (β„€ βˆ™ p) is second-countable.

@[reducible]

The unit circle ℝ β§Έ β„€.

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.

inductive add_circle.endpoint_ident {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (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).

noncomputable def add_circle.equiv_Icc_quot {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p a : π•œ) [hp : fact (0 < p)] [archimedean π•œ] :

The equivalence between add_circle p and the quotient of [a, a + p] by the relation identifying the endpoints.

Equations
theorem add_circle.equiv_Icc_quot_comp_mk_eq_to_Ico_mod {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p a : π•œ) [hp : fact (0 < p)] [archimedean π•œ] :
⇑(add_circle.equiv_Icc_quot p a) ∘ quotient.mk' = Ξ» (x : π•œ), quot.mk (add_circle.endpoint_ident p a) ⟨to_Ico_mod _ a x, _⟩
theorem add_circle.equiv_Icc_quot_comp_mk_eq_to_Ioc_mod {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p a : π•œ) [hp : fact (0 < p)] [archimedean π•œ] :
⇑(add_circle.equiv_Icc_quot p a) ∘ quotient.mk' = Ξ» (x : π•œ), quot.mk (add_circle.endpoint_ident p a) ⟨to_Ioc_mod _ a x, _⟩
noncomputable def add_circle.homeo_Icc_quot {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p a : π•œ) [hp : fact (0 < p)] [archimedean π•œ] :

The natural map from [a, a + p] βŠ‚ π•œ with endpoints identified to π•œ / β„€ β€’ p, as a homeomorphism of topological spaces.

Equations

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.

theorem add_circle.lift_Ico_eq_lift_Icc {π•œ : Type u_1} {B : Type u_2} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] {p a : π•œ} [hp : fact (0 < p)] [archimedean π•œ] {f : π•œ β†’ B} (h : f a = f (a + p)) :
theorem add_circle.lift_Ico_continuous {π•œ : Type u_1} {B : Type u_2} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] {p a : π•œ} [hp : fact (0 < p)] [archimedean π•œ] [topological_space B] {f : π•œ β†’ B} (hf : f a = f (a + p)) (hc : continuous_on f (set.Icc a (a + p))) :
theorem add_circle.lift_Ico_zero_coe_apply {π•œ : Type u_1} {B : Type u_2} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] {p : π•œ} [hp : fact (0 < p)] [archimedean π•œ] {f : π•œ β†’ B} {x : π•œ} (hx : x ∈ set.Ico 0 p) :
theorem add_circle.lift_Ico_zero_continuous {π•œ : Type u_1} {B : Type u_2} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] {p : π•œ} [hp : fact (0 < p)] [archimedean π•œ] [topological_space B] {f : π•œ β†’ B} (hf : f 0 = f p) (hc : continuous_on f (set.Icc 0 p)) :