The circle AddCircle p as a smooth manifold

For a positive real p, the circle AddCircle p = ℝ ⧸ pℤ is the orbit space of the action of Multiplicative ℤ on the real line by n • t = t + n p. This action is free and properly discontinuous and acts by analytic maps, so TauCeti.instIsManifoldQuotient makes its orbit space an analytic manifold modelled on ℝ. This file transports that structure to Mathlib's topological circle AddCircle p, along the homeomorphism of the orbit space with AddCircle p. The quotient map ((↑) : ℝ → AddCircle p) is then an analytic local diffeomorphism; it is a covering map by Mathlib's AddCircle.isCoveringMap_coe.

So that ℝ itself does not acquire a p-dependent action of Multiplicative ℤ, the action lives on the type synonym TauCeti.PeriodLine p of ℝ, which carries the topology and the manifold structure of ℝ. The equivalence TauCeti.PeriodLine.ofReal p identifies ℝ with it.

The charts of AddCircle p are local lifts to ℝ: every chart c of the atlas satisfies (c x : AddCircle p) = x on its source (AddCircle.coe_apply_of_mem_atlas). Read in these charts, the quotient map and every translation have derivative 1, and AddCircle p is an analytic additive Lie group. For a second positive period q, the rescaling AddCircle.equivAddCircle p q, sending the class of t to the class of t * (p⁻¹ * q), is an analytic diffeomorphism with derivative p⁻¹ * q.

Main definitions

• TauCeti.PeriodLine p: the real line, with the action of Multiplicative ℤ by translations by integer multiples of p.
• TauCeti.PeriodLine.quotientHomeomorph p: the homeomorphism of the orbit space of this action with AddCircle p.
• AddCircle.instChartedSpace, AddCircle.instIsManifold: the charts of AddCircle p, and the analytic manifold structure they form.
• TauCeti.PeriodLine.quotientDiffeomorph p n: the orbit space is diffeomorphic to AddCircle p.
• AddCircle.diffeomorphAddCircle p q n: the rescaling diffeomorphism AddCircle p ≃ AddCircle q.

Main results

• TauCeti.PeriodLine.instProperlyDiscontinuousSMul, TauCeti.PeriodLine.instIsCancelSMul, TauCeti.PeriodLine.instContMDiffConstSMul: the action is properly discontinuous, free and by analytic maps.
• AddCircle.isLocalDiffeomorph_coe: the quotient map ℝ → AddCircle p is an analytic local diffeomorphism.
• AddCircle.coe_apply_of_mem_atlas: the charts of AddCircle p are local lifts to ℝ.
• AddCircle.symm_apply_of_coe_apply, AddCircle.mfderiv_of_coe_apply, AddCircle.mfderiv_extChartAt_symm: the inverse of a local lift is the quotient map, and local lifts and the inverses of the extended charts have derivative the identity of ℝ.
• AddCircle.coe_extChartAt_apply, AddCircle.coe_extChartAt_self, AddCircle.extChartAt_symm_apply: the extended charts are local lifts, and their inverses are the quotient map on their targets.
• AddCircle.instLieAddGroup: AddCircle p is an analytic additive Lie group. In particular, multiplication by an integer is analytic (TauCeti.contMDiff_zsmul).
• AddCircle.contMDiff_of_comp_coe_eq, AddCircle.hasMFDerivAt_of_comp_coe_eq: a map AddCircle p → AddCircle q lifting a map f : ℝ → ℝ is as smooth as f, and has the derivative of f. Conversely a continuous lift of a C^n map is C^n (AddCircle.contDiff_of_comp_coe_eq).
• AddCircle.hasMFDerivAt_coe, AddCircle.mfderiv_add_right: the quotient map and the translations have derivative the identity of ℝ.
• AddCircle.isLocalDiffeomorph_prodMap_coe, AddCircle.hasMFDerivAt_prodMap_coe, AddCircle.mfderiv_prodMap_coe: the quotient map ℝ × ℝ → AddCircle p × AddCircle q is an analytic local diffeomorphism whose differential is the identity of ℝ × ℝ.
• AddCircle.hasMFDerivAt_add_coe_comp: the velocity of a curve s ↦ x + [f s] is the derivative of f.
• AddCircle.mfderiv_zsmul: multiplication by an integer k has derivative multiplication by k.
• AddCircle.mfderiv_diffeomorphAddCircle: the rescaling from period p to period q has derivative multiplication by p⁻¹ * q.

References

• John M. Lee, Introduction to Smooth Manifolds, second edition, Graduate Texts in Mathematics 218, Springer, 2013, Chapter 21 (quotients by discrete group actions).

def TauCeti.PeriodLine (_p : ℝ) : Type

The real line, as the covering space of the circle AddCircle p: a type synonym of ℝ carrying the action of Multiplicative ℤ by translations by integer multiples of p.

@[instance_reducible]

instance TauCeti.PeriodLine.instTopologicalSpace (p : ℝ) : TopologicalSpace (PeriodLine p)

instance TauCeti.PeriodLine.instT2Space (p : ℝ) : T2Space (PeriodLine p)

instance TauCeti.PeriodLine.instLocallyCompactSpace (p : ℝ) : LocallyCompactSpace (PeriodLine p)

@[instance_reducible]

instance TauCeti.PeriodLine.instChartedSpaceReal (p : ℝ) : ChartedSpace ℝ (PeriodLine p)

instance TauCeti.PeriodLine.instIsManifoldRealModelWithCornersSelf (p : ℝ) {n : WithTop ℕ∞} : IsManifold (modelWithCornersSelf ℝ ℝ) n (PeriodLine p)

def TauCeti.PeriodLine.ofReal (p : ℝ) : ℝ ≃ PeriodLine p

The identification of the real line with PeriodLine p.

theorem TauCeti.PeriodLine.chartAt_apply (p : ℝ) (s t : PeriodLine p) : ↑(chartAt ℝ s) t = (ofReal p).symm t

The chart of PeriodLine p at any point is the identification with ℝ.

theorem TauCeti.PeriodLine.continuous_ofReal (p : ℝ) : Continuous ⇑(ofReal p)

The identification of the real line with PeriodLine p is continuous.

theorem TauCeti.PeriodLine.continuous_ofReal_symm (p : ℝ) : Continuous ⇑(ofReal p).symm

The identification of PeriodLine p with the real line is continuous.

theorem TauCeti.PeriodLine.contMDiff_ofReal (p : ℝ) (n : WithTop ℕ∞) : ContMDiff (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) n ⇑(ofReal p)

The identification of the real line with PeriodLine p is analytic.

theorem TauCeti.PeriodLine.contMDiff_ofReal_symm (p : ℝ) (n : WithTop ℕ∞) : ContMDiff (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) n ⇑(ofReal p).symm

The identification of PeriodLine p with the real line is analytic.

theorem TauCeti.PeriodLine.isLocalDiffeomorph_ofReal (p : ℝ) (n : WithTop ℕ∞) : IsLocalDiffeomorph (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) n ⇑(ofReal p)

The identification of the real line with PeriodLine p is a local diffeomorphism.

The action of Multiplicative ℤ

@[instance_reducible]

instance TauCeti.PeriodLine.instSMulMultiplicativeInt (p : ℝ) : SMul (Multiplicative ℤ) (PeriodLine p)

theorem TauCeti.PeriodLine.smul_def (p : ℝ) (n : Multiplicative ℤ) (t : PeriodLine p) : n • t = (ofReal p) ((ofReal p).symm t + Multiplicative.toAdd n • p)

The integer n acts on PeriodLine p by translation by n • p.

@[simp]

theorem TauCeti.PeriodLine.ofReal_symm_smul (p : ℝ) (n : Multiplicative ℤ) (t : PeriodLine p) : (ofReal p).symm (n • t) = (ofReal p).symm t + Multiplicative.toAdd n • p

The integer n acts on PeriodLine p by translation by n • p, read in ℝ.

@[simp]

theorem TauCeti.PeriodLine.smul_ofReal (p : ℝ) (n : Multiplicative ℤ) (t : ℝ) : n • (ofReal p) t = (ofReal p) (t + Multiplicative.toAdd n • p)

The integer n acts on PeriodLine p by translation by n • p, read in ℝ.

@[instance_reducible]

instance TauCeti.PeriodLine.instMulActionMultiplicativeInt (p : ℝ) : MulAction (Multiplicative ℤ) (PeriodLine p)

Multiplicative ℤ acts on the real line by translations by integer multiples of p.

instance TauCeti.PeriodLine.instContinuousSMulMultiplicativeInt (p : ℝ) : ContinuousSMul (Multiplicative ℤ) (PeriodLine p)

The action is jointly continuous.

instance TauCeti.PeriodLine.instContMDiffConstSMul (p : ℝ) {n : WithTop ℕ∞} : ContMDiffConstSMul (modelWithCornersSelf ℝ ℝ) n (Multiplicative ℤ) (PeriodLine p)

The action is by analytic maps.

The orbit space

theorem TauCeti.PeriodLine.orbitRel_iff (p : ℝ) {s t : PeriodLine p} : (MulAction.orbitRel (Multiplicative ℤ) (PeriodLine p)) s t ↔ ↑((ofReal p).symm s) = ↑((ofReal p).symm t)

Two points of PeriodLine p lie in one orbit exactly when the real numbers they represent have the same image in AddCircle p.

def TauCeti.PeriodLine.quotientHomeomorph (p : ℝ) : MulAction.orbitRel.Quotient (Multiplicative ℤ) (PeriodLine p) ≃ₜ AddCircle p

The orbit space of the action of Multiplicative ℤ on PeriodLine p is homeomorphic to AddCircle p.

@[simp]

theorem TauCeti.PeriodLine.quotientHomeomorph_mk (p : ℝ) (t : PeriodLine p) : (quotientHomeomorph p) ⟦t⟧ = ↑((ofReal p).symm t)

The orbit of t corresponds to the image of t in AddCircle p.

@[simp]

theorem TauCeti.PeriodLine.quotientHomeomorph_symm_coe (p t : ℝ) : (quotientHomeomorph p).symm ↑t = ⟦(ofReal p) t⟧

The image of t in AddCircle p corresponds to the orbit of t.

instance TauCeti.PeriodLine.instIsCancelSMul (p : ℝ) [hp : Fact (0 < p)] : IsCancelSMul (Multiplicative ℤ) (PeriodLine p)

For positive p, the action is free: a translation by a nonzero multiple of p has no fixed point.

instance TauCeti.PeriodLine.instProperlyDiscontinuousSMul (p : ℝ) [hp : Fact (0 < p)] : ProperlyDiscontinuousSMul (Multiplicative ℤ) (PeriodLine p)

For positive p, the action is properly discontinuous: only finitely many integers translate a compact set to meet another compact set.

The manifold structure of AddCircle p

@[instance_reducible]

noncomputable instance AddCircle.instChartedSpace (p : ℝ) [Fact (0 < p)] : ChartedSpace ℝ (AddCircle p)

The charts of AddCircle p, transported from the orbit space of the action of Multiplicative ℤ on PeriodLine p along TauCeti.PeriodLine.quotientHomeomorph p.

instance AddCircle.instIsManifold (p : ℝ) [Fact (0 < p)] {n : WithTop ℕ∞} : IsManifold (modelWithCornersSelf ℝ ℝ) n (AddCircle p)

The circle AddCircle p is an analytic manifold modelled on ℝ.

noncomputable def TauCeti.PeriodLine.quotientDiffeomorph (p : ℝ) [Fact (0 < p)] (n : WithTop ℕ∞) : Diffeomorph (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) (MulAction.orbitRel.Quotient (Multiplicative ℤ) (PeriodLine p)) (AddCircle p) n

The orbit space of the action of Multiplicative ℤ on PeriodLine p is diffeomorphic to AddCircle p.

@[simp]

theorem TauCeti.PeriodLine.coe_quotientDiffeomorph (p : ℝ) [Fact (0 < p)] (n : WithTop ℕ∞) : ⇑(quotientDiffeomorph p n) = ⇑(quotientHomeomorph p)

The underlying map of quotientDiffeomorph p n is quotientHomeomorph p.

@[simp]

theorem TauCeti.PeriodLine.coe_quotientDiffeomorph_symm (p : ℝ) [Fact (0 < p)] (n : WithTop ℕ∞) : ⇑(quotientDiffeomorph p n).symm = ⇑(quotientHomeomorph p).symm

The underlying map of the inverse of quotientDiffeomorph p n is the inverse of quotientHomeomorph p.

theorem AddCircle.isLocalDiffeomorph_coe (p : ℝ) [Fact (0 < p)] (n : WithTop ℕ∞) : IsLocalDiffeomorph (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) n QuotientAddGroup.mk

The quotient map ℝ → AddCircle p is an analytic local diffeomorphism.

theorem AddCircle.contMDiff_coe (p : ℝ) [Fact (0 < p)] (n : WithTop ℕ∞) : ContMDiff (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) n QuotientAddGroup.mk

The quotient map ℝ → AddCircle p is analytic.

theorem AddCircle.coe_apply_of_mem_atlas {p : ℝ} [Fact (0 < p)] {c : OpenPartialHomeomorph (AddCircle p) ℝ} (hc : c ∈ atlas ℝ (AddCircle p)) {x : AddCircle p} (hx : x ∈ c.source) : ↑(↑c x) = x

The charts of AddCircle p are local lifts to ℝ: a chart sends each point of its source to a real number representing it.

theorem AddCircle.symm_apply_of_coe_apply {p : ℝ} {c : OpenPartialHomeomorph (AddCircle p) ℝ} (hc : ∀ x ∈ c.source, ↑(↑c x) = x) {u : ℝ} (hu : u ∈ c.target) : ↑c.symm u = ↑u

The inverse of a local lift of AddCircle p to ℝ is the quotient map on its target.

theorem AddCircle.mem_maximalAtlas_of_coe_apply {p : ℝ} [Fact (0 < p)] {n : WithTop ℕ∞} {c : OpenPartialHomeomorph (AddCircle p) ℝ} (hc : ∀ x ∈ c.source, ↑(↑c x) = x) : c ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℝ ℝ) n (AddCircle p)

A local lift of AddCircle p to ℝ, a partial homeomorphism sending each point of its source to a real number representing it, is a chart of the maximal atlas of AddCircle p.

theorem AddCircle.exists_eventuallyEq_add_zsmul {p : ℝ} {c c' : OpenPartialHomeomorph (AddCircle p) ℝ} (hc : ∀ x ∈ c.source, ↑(↑c x) = x) (hc' : ∀ x ∈ c'.source, ↑(↑c' x) = x) {x : AddCircle p} (hx : x ∈ c.source) (hx' : x ∈ c'.source) : ∃ (k : ℤ), ↑c' =ᶠ[nhds x] fun (y : AddCircle p) => ↑c y + k • p

Two local lifts of AddCircle p to ℝ differ, near each point of their common source, by a fixed integer multiple of p.

The additive Lie group structure

instance AddCircle.instLieAddGroup (p : ℝ) [Fact (0 < p)] {n : WithTop ℕ∞} : LieAddGroup (modelWithCornersSelf ℝ ℝ) n (AddCircle p)

The circle AddCircle p is an analytic additive Lie group: the quotient map ℝ → AddCircle p is a surjective additive local diffeomorphism.

theorem AddCircle.hasMFDerivAt_coe (p : ℝ) [Fact (0 < p)] (t : ℝ) : HasMFDerivAt% QuotientAddGroup.mk t (ContinuousLinearMap.id ℝ ℝ)

The quotient map ℝ → AddCircle p has derivative the identity of ℝ, the tangent spaces of AddCircle p being read in its charts, which are local real lifts.

@[simp]

theorem AddCircle.mfderiv_coe (p : ℝ) [Fact (0 < p)] (t : ℝ) : mfderiv% QuotientAddGroup.mk t = ContinuousLinearMap.id ℝ ℝ

The derivative of the quotient map ℝ → AddCircle p is the identity of ℝ.

theorem AddCircle.hasMFDerivAt_add_coe_comp {p : ℝ} [Fact (0 < p)] {f : ℝ → ℝ} {f' t : ℝ} (hf : HasDerivAt f f' t) (x : AddCircle p) : HasMFDerivAt% (fun (s : ℝ) => x + ↑(f s)) t (ContinuousLinearMap.smulRight 1 f')

If f : ℝ → ℝ has derivative f' at t, the curve s ↦ x + [f s] of AddCircle p has velocity f' at t, read in the tangent line of AddCircle p.

theorem AddCircle.mfderiv_comp_coe {p : ℝ} [Fact (0 < p)] {E' : Type u_1} {H' : Type u_2} {N : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace N] [ChartedSpace H' N] {g : AddCircle p → N} {t : ℝ} : mfderiv% (g ∘ QuotientAddGroup.mk) t = mfderiv% g ↑t

At the image of t, a map out of AddCircle p has the derivative of its periodic lift at t.

theorem AddCircle.mfderiv_of_coe_apply {p : ℝ} [Fact (0 < p)] {c : OpenPartialHomeomorph (AddCircle p) ℝ} (hc : ∀ x ∈ c.source, ↑(↑c x) = x) {x : AddCircle p} (hx : x ∈ c.source) : mfderiv% ↑c x = ContinuousLinearMap.id ℝ ℝ

A local lift of AddCircle p to ℝ has derivative the identity of ℝ at each point of its source.

theorem AddCircle.coe_extChartAt_apply {p : ℝ} [Fact (0 < p)] (x : AddCircle p) {y : AddCircle p} (hy : y ∈ (extChartAt (modelWithCornersSelf ℝ ℝ) x).source) : ↑(↑(extChartAt (modelWithCornersSelf ℝ ℝ) x) y) = y

The extended charts of AddCircle p are local lifts to ℝ: an extended chart sends each point of its source to a real number representing it.

theorem AddCircle.coe_extChartAt_self {p : ℝ} [Fact (0 < p)] (x : AddCircle p) : ↑(↑(extChartAt (modelWithCornersSelf ℝ ℝ) x) x) = x

The extended chart of AddCircle p at x sends x to a real number representing it.

theorem AddCircle.extChartAt_symm_apply {p : ℝ} [Fact (0 < p)] (x : AddCircle p) {z : ℝ} (hz : z ∈ (extChartAt (modelWithCornersSelf ℝ ℝ) x).target) : ↑(extChartAt (modelWithCornersSelf ℝ ℝ) x).symm z = ↑z

On its target, the inverse of an extended chart of AddCircle p is the quotient map ℝ → AddCircle p.

theorem AddCircle.mfderiv_extChartAt_symm {p : ℝ} [Fact (0 < p)] (x : AddCircle p) {z : ℝ} (hz : z ∈ (extChartAt (modelWithCornersSelf ℝ ℝ) x).target) : mfderiv% ↑(extChartAt (modelWithCornersSelf ℝ ℝ) x).symm z = ContinuousLinearMap.id ℝ ℝ

At each point of its target, the inverse of an extended chart of AddCircle p has derivative the identity of ℝ: near that point it is the quotient map ℝ → AddCircle p.

Maps between circles lifting maps of ℝ

theorem AddCircle.contMDiff_of_comp_coe_eq {p : ℝ} [Fact (0 < p)] {q : ℝ} [Fact (0 < q)] {n : WithTop ℕ∞} {g : AddCircle p → AddCircle q} {f : ℝ → ℝ} (h : g ∘ QuotientAddGroup.mk = QuotientAddGroup.mk ∘ f) (hf : ContDiff ℝ n f) : ContMDiff (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) n g

A map g : AddCircle p → AddCircle q lifting a C^n map f : ℝ → ℝ, in the sense that g ∘ (↑) = (↑) ∘ f, is C^n.

theorem AddCircle.contDiff_of_comp_coe_eq {p : ℝ} [Fact (0 < p)] {q : ℝ} [Fact (0 < q)] {n : WithTop ℕ∞} {g : AddCircle p → AddCircle q} {f : ℝ → ℝ} (h : g ∘ QuotientAddGroup.mk = QuotientAddGroup.mk ∘ f) (hf : Continuous f) (hg : ContMDiff (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) n g) : ContDiff ℝ n f

Conversely, a continuous lift f : ℝ → ℝ of a C^n map g : AddCircle p → AddCircle q, in the sense that g ∘ (↑) = (↑) ∘ f, is C^n, since the quotient map is a local diffeomorphism.

theorem AddCircle.hasMFDerivAt_of_comp_coe_eq {p : ℝ} [Fact (0 < p)] {q : ℝ} [Fact (0 < q)] {g : AddCircle p → AddCircle q} {f : ℝ → ℝ} {f' : ℝ →L[ℝ] ℝ} {t : ℝ} (h : g ∘ QuotientAddGroup.mk = QuotientAddGroup.mk ∘ f) (hf : HasFDerivAt f f' t) : HasMFDerivAt% g (↑t) f'

A map g : AddCircle p → AddCircle q lifting a map f : ℝ → ℝ, in the sense that g ∘ (↑) = (↑) ∘ f, has at the image of t the derivative of f at t.

@[simp]

theorem AddCircle.mfderiv_add_right (p : ℝ) [Fact (0 < p)] (a x : AddCircle p) : (mfderiv% fun (x : AddCircle p) => x + a) x = ContinuousLinearMap.id ℝ ℝ

Every translation of AddCircle p has derivative the identity of ℝ.

@[simp]

theorem AddCircle.mfderiv_zsmul (p : ℝ) [Fact (0 < p)] (k : ℤ) (x : AddCircle p) : (mfderiv% fun (y : AddCircle p) => k • y) x = k • ContinuousLinearMap.id ℝ ℝ

Multiplication by an integer k on AddCircle p has derivative multiplication by k, with its sign, at every point.

Rescaling the period

noncomputable def AddCircle.diffeomorphAddCircle (p : ℝ) [Fact (0 < p)] (q : ℝ) [Fact (0 < q)] (n : WithTop ℕ∞) : Diffeomorph (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) (AddCircle p) (AddCircle q) n

The rescaling AddCircle p ≃ AddCircle q sending the class of t to the class of t * (p⁻¹ * q), as an analytic diffeomorphism. It is AddCircle.equivAddCircle, the descent of multiplication by p⁻¹ * q on ℝ.

theorem AddCircle.coe_diffeomorphAddCircle (p : ℝ) [Fact (0 < p)] (q : ℝ) [Fact (0 < q)] (n : WithTop ℕ∞) : ⇑(diffeomorphAddCircle p q n) = ⇑(equivAddCircle p q ⋯ ⋯)

The underlying map of diffeomorphAddCircle p q n is AddCircle.equivAddCircle.

@[simp]

theorem AddCircle.diffeomorphAddCircle_apply_mk (p : ℝ) [Fact (0 < p)] (q : ℝ) [Fact (0 < q)] (n : WithTop ℕ∞) (t : ℝ) : (diffeomorphAddCircle p q n) ↑t = ↑(t * (p⁻¹ * q))

The rescaling sends the class of t to the class of t * (p⁻¹ * q).

@[simp]

theorem AddCircle.toHomeomorph_diffeomorphAddCircle (p : ℝ) [Fact (0 < p)] (q : ℝ) [Fact (0 < q)] (n : WithTop ℕ∞) : (diffeomorphAddCircle p q n).toHomeomorph = homeomorphAddCircle p q ⋯ ⋯

The underlying homeomorphism of diffeomorphAddCircle p q n is AddCircle.homeomorphAddCircle.

@[simp]

theorem AddCircle.diffeomorphAddCircle_symm (p : ℝ) [Fact (0 < p)] (q : ℝ) [Fact (0 < q)] (n : WithTop ℕ∞) : (diffeomorphAddCircle p q n).symm = diffeomorphAddCircle q p n

The inverse of the rescaling from AddCircle p to AddCircle q is the rescaling back.

@[simp]

theorem AddCircle.diffeomorphAddCircle_add (p : ℝ) [Fact (0 < p)] (q : ℝ) [Fact (0 < q)] (n : WithTop ℕ∞) (x y : AddCircle p) : (diffeomorphAddCircle p q n) (x + y) = (diffeomorphAddCircle p q n) x + (diffeomorphAddCircle p q n) y

The rescaling is additive.

@[simp]

theorem AddCircle.diffeomorphAddCircle_zsmul (p : ℝ) [Fact (0 < p)] (q : ℝ) [Fact (0 < q)] (n : WithTop ℕ∞) (k : ℤ) (x : AddCircle p) : (diffeomorphAddCircle p q n) (k • x) = k • (diffeomorphAddCircle p q n) x

The rescaling commutes with integer multiplication.

@[simp]

theorem AddCircle.diffeomorphAddCircle_self (p : ℝ) [Fact (0 < p)] (n : WithTop ℕ∞) : diffeomorphAddCircle p p n = Diffeomorph.refl (modelWithCornersSelf ℝ ℝ) (AddCircle p) n

Rescaling AddCircle p to its own period is the identity.

@[simp]

theorem AddCircle.diffeomorphAddCircle_trans (p : ℝ) [Fact (0 < p)] (q r : ℝ) [Fact (0 < q)] [Fact (0 < r)] (n : WithTop ℕ∞) : (diffeomorphAddCircle p q n).trans (diffeomorphAddCircle q r n) = diffeomorphAddCircle p r n

Rescaling from AddCircle p to AddCircle q and then to AddCircle r is the rescaling from AddCircle p to AddCircle r.

@[simp]

theorem AddCircle.mfderiv_diffeomorphAddCircle (p : ℝ) [Fact (0 < p)] (q : ℝ) [Fact (0 < q)] (n : WithTop ℕ∞) (x : AddCircle p) : mfderiv% ⇑(diffeomorphAddCircle p q n) x = (p⁻¹ * q) • ContinuousLinearMap.id ℝ ℝ

The rescaling from AddCircle p to AddCircle q has derivative multiplication by p⁻¹ * q at every point.

The quotient map of a torus of two circles

theorem AddCircle.prodMap_coe_surjective (p q : ℝ) : Function.Surjective (Prod.map QuotientAddGroup.mk QuotientAddGroup.mk)

The quotient map ℝ × ℝ → AddCircle p × AddCircle q is surjective.

theorem AddCircle.isLocalDiffeomorph_prodMap_coe (p : ℝ) [Fact (0 < p)] (q : ℝ) [Fact (0 < q)] (n : WithTop ℕ∞) : IsLocalDiffeomorph (modelWithCornersSelf ℝ (ℝ × ℝ)) ((modelWithCornersSelf ℝ ℝ).prod (modelWithCornersSelf ℝ ℝ)) n (Prod.map QuotientAddGroup.mk QuotientAddGroup.mk)

The quotient map ℝ × ℝ → AddCircle p × AddCircle q is an analytic local diffeomorphism.

theorem AddCircle.hasMFDerivAt_prodMap_coe (p : ℝ) [Fact (0 < p)] (q : ℝ) [Fact (0 < q)] (z : ℝ × ℝ) : HasMFDerivAt% (Prod.map QuotientAddGroup.mk QuotientAddGroup.mk) z (ContinuousLinearMap.id ℝ (ℝ × ℝ))

The quotient map ℝ × ℝ → AddCircle p × AddCircle q has derivative the identity of ℝ × ℝ, the tangent spaces of both circles being read in their charts.

@[simp]

theorem AddCircle.mfderiv_prodMap_coe (p : ℝ) [Fact (0 < p)] (q : ℝ) [Fact (0 < q)] (z : ℝ × ℝ) : mfderiv% (Prod.map QuotientAddGroup.mk QuotientAddGroup.mk) z = ContinuousLinearMap.id ℝ (ℝ × ℝ)

The derivative of the quotient map ℝ × ℝ → AddCircle p × AddCircle q is the identity of ℝ × ℝ.