Revision #1842 → #3557 · back to history
modifiedMöbius transformation52def74d1ecf
| Field | From #1842 | To #3557 |
|---|
| note | The action of `GL (Fin 2) K` on `OnePoint K` (extended Riemann sphere) is defined as Möbius/fractional-linear transformations, generalizing the complex case. | The action of `GL (Fin 2) K` on `OnePoint K` is defined as fractional-linear/Möbius transformations, generalizing the complex case. |
modifiedMöbius group as PGL(2,C)712a24c62299
| Field | From #1842 | To #3557 |
|---|
| note | `PGL(n, R)` is defined as `GL n R ⧸ center`, but the Möbius group is not introduced as a named object identified with `PGL(2, ℂ)`. | `PGL(n, R) = GL n R ⧸ center` is defined, but the Möbius group is not introduced as a named object identified with `PGL(2, ℂ)`. |
modifiedKernel of the Schwarzian derivative4520162824dd
| Field | From #1842 | To #3557 |
|---|
| note | The Schwarzian derivative is not defined in Mathlib. | The Schwarzian derivative is not defined in Mathlib (loogle finds no `Schwarzian`). |
modifiedSimple transformations: translation, rotation, homothety, inversionec492fad7c53
| Field | From #1842 | To #3557 |
|---|
| note | Some special elements (translations via `upperRightHom`, `ModularGroup.S` for inversion, `ModularGroup.T`) appear, but no systematic catalogue. | Some special elements (translations via `upperRightHom`, `ModularGroup.S`/`T` for inversion and translation) appear, but no systematic catalogue. |
modifiedCross-ratios are invariant4481c6c5a2f1
| Field | From #1842 | To #3557 |
|---|
| note | Cross-ratio is not defined in Mathlib. | Cross-ratio is not defined in Mathlib (loogle finds no `crossRatio`). |
modifiedNatural action of PGL(2,C) equals Möbius action8ba22f7a66c5
| Field | From #1842 | To #3557 |
|---|
| note | `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`. | `GL(2,K)` acts via Möbius formulas on `OnePoint K`, and `equivProjectivization_smul` says this matches the projective-line action; the descent to PGL is implicit. |
modifiedAction of PGL(2,C) on the projective lined92e154c15af
| Field | From #1842 | To #3557 |
|---|
| note | 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. | The action of any group acting K-linearly (including GL n K) on `ℙ K V` is given by `Projectivization.instMulAction`; passing to PGL is implicit. |
modifiedSL(2,C) → PGL(2,C) surjection with kernel ±I5d26ea81d558
| Field | From #1842 | To #3557 |
|---|
| note | `PSL(n, R) = SL(n,R) ⧸ center` is defined, and over a field with characteristic ≠ 2 the center is `{±I}`, but the map `PSL(2,ℂ) → PGL(2,ℂ)` as an isomorphism is not constructed. | `PSL(n, R) = SL(n,R) ⧸ center` is defined, but the map `PSL(2,ℂ) → PGL(2,ℂ)` as an isomorphism is not constructed. |
modifiedTrace invariant under conjugation; conjugacy criterion6e2e11cc1f82
| Field | From #1842 | To #3557 |
|---|
| note | 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. | Conjugation invariance of these classes is proved (`isParabolic_conj_iff` and analogues); the trace-based criterion is implicit via the discriminant but not packaged. |
modifiedLoxodromic transformation0bf2636b1452
| Field | From #1842 | To #3557 |
|---|
| note | There is no `IsLoxodromic` class in Mathlib. | There is no `IsLoxodromic` class in Mathlib (loogle finds no such name). |
addedCayley transform between R^n ∪ {∞} and S^nf28e3e7d7058
addedAlternative names: homographies, LFTs, bilinear, spin transformationsc7d28b23202f
addedFundamental group of Riemann surface is a discrete subgroup43bb2e02fd71
addedLorentz group acts on celestial sphere as Möbius group1fe838346583