Revision #1409 → #1842 · back to history
modifiedMöbius transformation52def74d1ecf
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"(Lead)","snippet":"a Möbius transformation of the complex plane is a rational function of the form"},{"type":"math_alttext","value":"{\\displaystyle f(z)={\\frac {az+b}{cz+d}}}"}] | — |
modifiedGeneral form of a Möbius transformationa594be4c9bb5
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Definition","snippet":"The general form of a Möbius transformation is given by"},{"type":"math_alttext","value":"{\\displaystyle f(z)={\\frac {az+b}{cz+d}},}"}] | — |
modifiedExtension when c ≠ 0c2036d104512
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Definition","snippet":"this definition is extended to the whole Riemann sphere by defining"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}f\\left({\\frac {-d}{c}}\\right)&=\\infty ,\\\\f(\\infty )&={\\frac {a}{c}}.\\end{aligned}}}"}] | — |
modifiedExtension when c = 00cd7416a337a
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Definition","snippet":"If c = 0 , we define"},{"type":"math_alttext","value":"{\\displaystyle f(\\infty )=\\infty .}"}] | — |
modifiedDegenerate case ad = bc749b317ccbfa
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Definition","snippet":"the rational function defined above is a constant"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {az+b}{cz+d}}={\\frac {a}{c}}={\\frac {b}{d}},}"}] | — |
modifiedFixed-point formula via quadratic90c6ee8003f3
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Determining the fixed points","snippet":"The fixed points of the transformation"},{"type":"math_alttext","value":"{\\displaystyle f(z)={\\frac {az+b}{cz+d}}}"},{"type":"math_alttext","value":"{\\displaystyle c\\gamma ^{2}-(a-d)\\gamma -b=0\\ ,}"},{"type":"math_alttext","value":"{\\displaystyle \\gamma _{1,2}={\\frac {(a-d)\\pm {\\sqrt {(a-d)^{2}+4bc}}}{2c}}={\\frac {(a-d)\\pm {\\sqrt {\\Delta }}}{2c}}}"},{"type":"math_alttext","value":"{\\displaystyle \\Delta =(\\operatorname {tr} {\\mathfrak {H}})^{2}-4\\det {\\mathfrak {H}}=(a+d)^{2}-4(ad-bc),}"},{"type":"math_alttext","value":"{\\displaystyle {\\mathfrak {H}}={\\begin{pmatrix}a&b\\\\c&d\\end{pmatrix}}}"}] | — |
modifiedLinear case when c = 021679a930f59
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Determining the fixed points","snippet":"When c = 0 , the quadratic equation degenerates into a linear equation and the transform is linear"},{"type":"math_alttext","value":"{\\displaystyle \\gamma =-{\\frac {b}{a-d}}.}"}] | — |
modifiedSimple transformation: translations, rotations, dilationsc23d1cd183dd
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Determining the fixed points","snippet":"In this case the transformation will be a simple transformation composed of translations"},{"type":"math_alttext","value":"{\\displaystyle z\\mapsto \\alpha z+\\beta .}"}] | — |
modifiedPure translation when c = 0 and a = d1045915e877a
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Determining the fixed points","snippet":"then both fixed points are at infinity, and the Möbius transformation corresponds to a pure translation"},{"type":"math_alttext","value":"{\\displaystyle z\\mapsto z+\\beta .}"}] | — |
modifiedTopological proof via Euler characteristica4b93ef5b57c
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Topological proof","snippet":"Topologically, the fact that (non-identity) Möbius transformations fix 2 points"},{"type":"math_alttext","value":"{\\displaystyle \\chi ({\\hat {\\mathbb {C} }})=2.}"}] | — |
modifiedNon-parabolic conjugate to dilation/rotation4b66e8228f76
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Normal form","snippet":"Every non-parabolic transformation is conjugate to a dilation/rotation"},{"type":"math_alttext","value":"{\\displaystyle z\\mapsto kz}"},{"type":"math_alttext","value":"{\\displaystyle g(z)={\\frac {z-\\gamma _{1}}{z-\\gamma _{2}}}}"}] | — |
modifiedCharacteristic constant (multiplier)9d76e4ed974b
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Normal form","snippet":"we can distinguish one of the multipliers"},{"type":"math_alttext","value":"{\\displaystyle {\\mathfrak {H}}(k;\\gamma _{1},\\gamma _{2})={\\mathfrak {H}}(1/k;\\gamma _{2},\\gamma _{1}).}"}] | — |
modifiedParabolic normal form as translation12852f99645a
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Normal form","snippet":"In the parabolic case there is only one fixed point"},{"type":"math_alttext","value":"{\\displaystyle g(z)={\\frac {1}{z-\\gamma }}}"},{"type":"math_alttext","value":"{\\displaystyle gfg^{-1}(z)=z+\\beta \\,.}"}] | — |
modifiedTranslation length6c11b07b0a43
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Normal form","snippet":"Here, β is called the translation length"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {1}{f(z)-\\gamma }}={\\frac {1}{z-\\gamma }}+\\beta .}"}] | — |
modifiedInverse poleb712175ffb22
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Poles of the transformation","snippet":"is that point to which the point at infinity is transformed"},{"type":"math_alttext","value":"{\\displaystyle \\gamma _{1}+\\gamma _{2}=z_{\\infty }+Z_{\\infty }.}"}] | — |
modifiedExplicit composition decompositiona54deffb267f
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Composition of simple transformations","snippet":"Then these functions can be composed"},{"type":"math_alttext","value":"{\\displaystyle f(z)={\\frac {az+b}{cz+d}},}"},{"type":"math_alttext","value":"{\\displaystyle f=f_{4}\\circ f_{3}\\circ f_{2}\\circ f_{1}.}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {az+b}{cz+d}}={\\frac {a}{c}}+{\\frac {e}{z+{\\frac {d}{c}}}},}"},{"type":"math_alttext","value":"{\\displaystyle e={\\frac {bc-ad}{c^{2}}}.}"}] | — |
modifiedFormula for inverse via composition73f96302f203
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Formula for the inverse transformation","snippet":"The existence of the inverse Möbius transformation and its explicit formula are easily derived"},{"type":"math_alttext","value":"{\\displaystyle g_{1}\\circ g_{2}\\circ g_{3}\\circ g_{4}(z)=f^{-1}(z)={\\frac {dz-b}{-cz+a}}}"}] | — |
modifiedGeneralized circles mapped to generalized circles329967d9cd0d
| Field | From #1409 | To #1842 |
|---|
| mathlib.decl | EuclideanGeometry.inversion_mapsTo_sphere | EuclideanGeometry.image_inversion_sphere_dist_center |
| note | Inversion-of-sphere statements exist, but no Möbius-level theorem that generalized circles map to generalized circles. | The image of a sphere under Euclidean inversion is described, but no Möbius-level theorem that generalized circles map to generalized circles is stated. |
modifiedCross-ratios are invariant4481c6c5a2f1
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Cross-ratio preservation","snippet":"Cross-ratios are invariant under Möbius transformations"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {(z_{1}-z_{3})(z_{2}-z_{4})}{(z_{2}-z_{3})(z_{1}-z_{4})}}={\\frac {(w_{1}-w_{3})(w_{2}-w_{4})}{(w_{2}-w_{3})(w_{1}-w_{4})}}.}"}] | — |
modifiedCross-ratio at infinity by limitf0f964e9e8e0
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Cross-ratio preservation","snippet":"then the cross-ratio has to be defined by taking the appropriate limit"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {(z_{1}-z_{3})}{(z_{2}-z_{3})}}.}"}] | — |
modifiedNatural action of PGL(2,C) equals Möbius action8ba22f7a66c5
| Field | From #1409 | To #1842 |
|---|
| mathlib.decl | OnePoint.instGLAction | OnePoint.equivProjectivization_smul |
| note | `GL(2,K)` acts via Möbius formulas on `OnePoint K` (and scalars act trivially, so this descends to `PGL`), but the equivalence with the action on `ℙ K (Fin 2 → K)` is given via `equivProjectivization_smul`. | `GL(2,K)` acts via Möbius formulas on `OnePoint K` (and scalars act trivially, so this descends to `PGL`); the equivalence with the action on `ℙ K (Fin 2 → K)` is given via `equivProjectivization_smul`. |
modifiedIdentification of CP^1 with the Riemann spherea34c72d70416
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Correspondence between the complex projective line and the Riemann sphere","snippet":"the projective line CP 1 and the Riemann sphere are identified as follows"},{"type":"math_alttext","value":"{\\displaystyle [z_{1}:z_{2}]\\ \\thicksim {\\frac {z_{1}}{z_{2}}}.}"}] | — |
modifiedAction of PGL(2,C) on the projective lined92e154c15af
| Field | From #1409 | To #1842 |
|---|
| mathlib.decl | Projectivization.action | Projectivization.instMulAction |
| note | The action of `GL n K` on `ℙ K (Fin n → K)` is defined via `Projectivization.Action`; passing to `PGL` would use `ProjGenLinGroup.mulActionOfGL`. | The action of any group acting K-linearly (including GL n K) on `ℙ K V` is given by `Projectivization.instMulAction`; passing to PGL uses the `SL_mulAction_ker` result. |
modifiedMapping three points to 0, 1, ∞0db7ec6cfb14
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Mapping first to 0, 1, ∞","snippet":"It is easy to check that the Möbius transformation"},{"type":"math_alttext","value":"{\\displaystyle f_{1}(z)={\\frac {(z-z_{1})(z_{2}-z_{3})}{(z-z_{3})(z_{2}-z_{1})}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\mathfrak {H}}_{1}={\\begin{pmatrix}z_{2}-z_{3}&-z_{1}(z_{2}-z_{3})\\\\z_{2}-z_{1}&-z_{3}(z_{2}-z_{1})\\end{pmatrix}}}"}] | — |
modifiedExplicit determinant formula via hyperbola785aa696e716
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Explicit determinant formula","snippet":"is equivalent to the equation of a standard hyperbola"},{"type":"math_alttext","value":"{\\displaystyle w={\\frac {az+b}{cz+d}}}"},{"type":"math_alttext","value":"{\\displaystyle cwz-az+dw-b=0}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{vmatrix}zw&z&w&1\\\\z_{1}w_{1}&z_{1}&w_{1}&1\\\\z_{2}w_{2}&z_{2}&w_{2}&1\\\\z_{3}w_{3}&z_{3}&w_{3}&1\\end{vmatrix}}\\,}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}a&=z_{1}w_{1}(w_{2}-w_{3})+z_{2}w_{2}(w_{3}-w_{1})+z_{3}w_{3}(w_{1}-w_{2}),\\\\[5mu]b&=z_{1}w_{1}(z_{2}w_{3}-z_{3}w_{2})+z_{2}w_{2}(z_{3}w_{1}-z_{1}w_{3})+z_{3}w_{3}(z_{1}w_{2}-z_{2}w_{1}),\\\\[5mu]c&=w_{1}(z_{3}-z_{2})+w_{2}(z_{1}-z_{3})+w_{3}(z_{2}-z_{1}),\\\\[5mu]d&=z_{1}w_{1}(z_{2}-z_{3})+z_{2}w_{2}(z_{3}-z_{1})+z_{3}w_{3}(z_{1}-z_{2})\\end{aligned}}}"}] | — |
modifiedPSL(2,R) as upper half-plane stabilizer8e4382b7fd7f
| Field | From #1409 | To #1842 |
|---|
| note | SL(2,ℝ) (and PSL via `FaithfulSMul PGL(2,ℝ) ℍ`) acts on `ℍ`, but the explicit characterization as the upper-half-plane-preserving subgroup of the Möbius group is not stated. | SL(2,ℝ) (and PSL via the faithful action) acts on `ℍ` via `UpperHalfPlane.SLAction`, but the explicit characterization as the upper-half-plane-preserving subgroup of the Möbius group is not stated. |
modifiedOpen-disk-preserving subgroup1a2c6ac1a837
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Subgroups of the Möbius group","snippet":"The subgroup of all Möbius transformations that map the open disk"},{"type":"math_alttext","value":"{\\displaystyle f(z)=e^{i\\phi }{\\frac {z+b}{{\\bar {b}}z+1}}}"}] | — |
modifiedIsomorphism between half-plane and disk subgroups6a1513375da7
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Subgroups of the Möbius group","snippet":"Since both of the above subgroups serve as isometry groups"},{"type":"math_alttext","value":"{\\displaystyle f(z)={\\frac {z+i}{iz+1}}}"}] | — |
modifiedMaximal compact subgroup is PSU(2) ≅ SO(3)d2cf71241065
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Subgroups of the Möbius group","snippet":"A maximal compact subgroup of the Möbius group"},{"type":"math_alttext","value":"{\\displaystyle {\\mathcal {M}}_{0}:=\\left\\{z\\mapsto {\\frac {uz-{\\bar {v}}}{vz+{\\bar {u}}}}:|u|^{2}+|v|^{2}=1\\right\\},}"}] | — |
modifiedModular group PSL(2,Z) and Fuchsian groups7015ebe65815
| Field | From #1409 | To #1842 |
|---|
| mathlib.decl | ModularGroup | ModularGroup.SLOnGLPos |
| mathlib.module | Mathlib.NumberTheory.Modular | Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction |
| note | The modular group action of SL(2,ℤ) on ℍ is formalized in `ModularGroup`, but PSL(2,ℤ) and the general theory of Fuchsian groups are not. | The modular group action of SL(2,ℤ) on the upper half plane is formalized via `ModularGroup.SLOnGLPos`, but PSL(2,ℤ) and Fuchsian groups in general are not packaged. |
modifiedTrace invariant under conjugation; conjugacy criterion6e2e11cc1f82
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Classification","snippet":"The four types can be distinguished by looking at the trace"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {tr} \\,{\\mathfrak {GHG}}^{-1}=\\operatorname {tr} \\,{\\mathfrak {H}},}"}] | — |
| note | Conjugation invariance of these classes is proved (`isParabolic_conj_iff`, `isElliptic_conj_iff`, `isHyperbolic_conj_iff`); the trace-based criterion is implicit via `discr_fin_two` but not packaged. | Conjugation invariance of these classes is proved (`isParabolic_conj_iff`, `isElliptic_conj_iff`, `isHyperbolic_conj_iff`); the trace-based criterion is implicit via the discriminant but not packaged. |
modifiedParabolic transformationb7c44f977099
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Parabolic transforms","snippet":"is said to be parabolic if"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {tr} ^{2}{\\mathfrak {H}}=(a+d)^{2}=4}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{pmatrix}1&1\\\\0&1\\end{pmatrix}}}"}] | — |
modifiedParabolic iff exactly one fixed pointb42329f21a85
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Parabolic transforms","snippet":"A Möbius transform is parabolic if and only if it has exactly one fixed point"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {tr} ^{2}{\\mathfrak {H}}=(a+d)^{2}=4}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{pmatrix}1&1\\\\0&1\\end{pmatrix}}}"}] | — |
modifiedParabolic subgroup as unipotent radicalfdd3e72a9e2e
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Parabolic transforms","snippet":"The set of all parabolic Möbius transformations with a given fixed point"},{"type":"math_alttext","value":"{\\displaystyle \\left\\{{\\begin{pmatrix}1&b\\\\0&1\\end{pmatrix}}\\mid b\\in \\mathbb {C} \\right\\};}"}] | — |
modifiedCharacteristic constant for non-parabolicbf64b4eb974f
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Characteristic constant","snippet":"All non-parabolic transformations have two fixed points and are defined by a matrix conjugate to"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{pmatrix}\\lambda &0\\\\0&\\lambda ^{-1}\\end{pmatrix}}}"}] | — |
modifiedElliptic transformation8b1f51d74b8e
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Elliptic transforms","snippet":"The transformation is said to be elliptic"},{"type":"math_alttext","value":"{\\displaystyle 0\\leq \\operatorname {tr} ^{2}{\\mathfrak {H}}<4.}"}] | — |
modifiedElliptic iff |λ| = 1 and λ ≠ ±15fc54e94f44a
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Elliptic transforms","snippet":"A transform is elliptic if and only if"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{pmatrix}\\cos \\alpha &-\\sin \\alpha \\\\\\sin \\alpha &\\cos \\alpha \\end{pmatrix}}}"}] | — |
modifiedCircular transform and three transpositions fixing {0,1,∞}39938a9f98a4
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Elliptic transforms","snippet":"is also denoted as a circular transform"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{pmatrix}0&-1\\\\1&0\\end{pmatrix}}.}"}] | — |
modifiedHyperbolic transformation4ddc58efdfad
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Hyperbolic transforms","snippet":"The transform is said to be hyperbolic"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {tr} ^{2}{\\mathfrak {H}}>4.}"}] | — |
modifiedLogarithmic form of the characteristic constant951d19ad8918
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Geometric interpretation of the characteristic constant","snippet":"The characteristic constant can be expressed in terms of its logarithm"},{"type":"math_alttext","value":"{\\displaystyle e^{\\rho +\\alpha i}=k.}"}] | — |
modifiedMöbius transformation in higher dimensions0acc606f6462
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Higher dimensions","snippet":"In higher dimensions, a Möbius transformation is a homeomorphism"},{"type":"math_alttext","value":"{\\displaystyle f(x)=b+{\\frac {\\alpha A(x-a)}{|x-a|^{\\varepsilon }}},}"}] | — |
modifiedLiouville's theorem in conformal geometrye50940bb583c
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Higher dimensions","snippet":"Liouville's theorem in conformal geometry states that in dimension at least three"},{"type":"math_alttext","value":"{\\displaystyle f(x)=b+{\\frac {\\alpha A(x-a)}{|x-a|^{\\varepsilon }}},}"}] | — |
modifiedMinkowski space with quadratic form11ee6e07fec5
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Lorentz transformation","snippet":"Minkowski space consists of the four-dimensional real coordinate space"},{"type":"math_alttext","value":"{\\displaystyle Q(x_{0},x_{1},x_{2},x_{3})=x_{0}^{2}-x_{1}^{2}-x_{2}^{2}-x_{3}^{2}.}"}] | — |
modifiedSO+(1,3) ≅ PSL(2,C) via hermitian matrices71a8494311c9
| Field | From #1409 | To #1842 |
|---|
| anchors | [{"section":"Lorentz transformation","snippet":"the group of transformations SO + (1, 3) is identified with the group PSL(2, C )"},{"type":"math_alttext","value":"{\\displaystyle X={\\begin{bmatrix}x_{0}+x_{1}&x_{2}+ix_{3}\\\\x_{2}-ix_{3}&x_{0}-x_{1}\\end{bmatrix}}.}"}] | — |