Documentation

TauCeti.Geometry.Manifold.Instances.Torus

Euclidean charts on the two-dimensional torus #

TauCeti.torusChartedSpace charts Circle × Circle on EuclideanSpace ℝ (Fin 2). It is the specialisation of TauCeti.prodEuclideanChartedSpace to two circles, which identifies Mathlib's product model of the two circle charts with ℝ², and TauCeti.torusChartedSpace_chartAt describes its charts. It is a definition rather than an instance, so that the Euclidean model can be chosen explicitly alongside Mathlib's product model.

source
@[instance_reducible]
noncomputable def TauCeti.torusChartedSpace :
ChartedSpace (EuclideanSpace ℝ (Fin 2)) (Circle × Circle)

The torus S¹ × S¹, charted on ℝ² through the product of the circle charts.

Instances For
    source
    @[simp]
    theorem TauCeti.torusChartedSpace_chartAt (x : Circle × Circle) :
    chartAt (EuclideanSpace ℝ (Fin 2)) x = ((chartAt (EuclideanSpace ℝ (Fin 1)) x.1).prod (chartAt (EuclideanSpace ℝ (Fin 1)) x.2)).trans EuclideanSpace.finAddEquivProd.symm.toHomeomorph.toOpenPartialHomeomorph

    The chart of TauCeti.torusChartedSpace at x is the product of the circle charts at x.1 and x.2, followed by EuclideanSpace.finAddEquivProd.symm.