Documentation

Mathlib.Topology.Instances.AddCircle

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

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 #

theorem continuous_right_toIcoMod {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {p : ๐•œ} (hp : 0 < p) (a : ๐•œ) (x : ๐•œ) :
theorem continuous_left_toIocMod {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {p : ๐•œ} (hp : 0 < p) (a : ๐•œ) (x : ๐•œ) :
theorem toIcoMod_eventuallyEq_toIocMod {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {p : ๐•œ} (hp : 0 < p) (a : ๐•œ) {x : ๐•œ} (hx : โ†‘x โ‰  โ†‘a) :
theorem continuousAt_toIcoMod {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {p : ๐•œ} (hp : 0 < p) (a : ๐•œ) {x : ๐•œ} (hx : โ†‘x โ‰  โ†‘a) :
theorem continuousAt_toIocMod {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {p : ๐•œ} (hp : 0 < p) (a : ๐•œ) {x : ๐•œ} (hx : โ†‘x โ‰  โ†‘a) :
@[inline, reducible]
abbrev AddCircle {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] (p : ๐•œ) :
Type u_1

The "additive circle": ๐•œ โงธ (โ„ค โˆ™ p). See also Circle and Real.angle.

Equations
Instances For
    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 : ๐•œ) :
    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
    Instances For
      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
      Instances For
        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
        Instances For
          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
          Instances For
            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) :
            theorem AddCircle.continuousAt_equivIoc {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] {x : AddCircle p} (hx : x โ‰  โ†‘a) :
            @[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) :

            The rescaling equivalence between additive circles with different periods.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[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
              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 < 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 : AddCircle p | 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.
              Instances For
                @[simp]
                theorem AddCircle.card_addOrderOf_eq_totient {๐•œ : Type u_1} [LinearOrderedField ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] {n : โ„•} :
                theorem AddCircle.finite_setOf_add_order_eq {๐•œ : Type u_1} [LinearOrderedField ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] {n : โ„•} (hn : 0 < n) :

                The "additive circle" โ„ โงธ (โ„ค โˆ™ p) is compact.

                Equations
                @[inline, reducible]

                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.

                  inductive AddCircle.EndpointIdent {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (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).

                  Instances For
                    def AddCircle.equivIccQuot {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] (p : ๐•œ) (a : ๐•œ) [hp : Fact (0 < p)] [Archimedean ๐•œ] :

                    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
                      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 ๐•œ] :

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

                      Equations
                      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.

                        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_1 b : โ†‘(Set.Icc a (a + p))), AddCircle.EndpointIdent p a a_1 b โ†’ Set.restrict (Set.Icc a (a + p)) f a_1 = 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))) :
                        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)) :