Revision #1413 → #2466 · back to history
modifiedMonodromy (informal)2b056e7600be
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | IsCoveringMap.monodromy |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Topology.Homotopy.Lifting |
| note | — | Mathlib formalises the covering-space instance of monodromy via `IsCoveringMap.monodromy`, but not the informal umbrella concept spanning analysis/algebra/geometry. |
| status | — | partial |
modifiedMonodromy group (informal)95fe5261a30c
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | IsCoveringMap.monodromyPerm |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Topology.Homotopy.Lifting |
| note | — | The `monodromyPerm` homomorphism packages the fundamental-group action as permutations, whose image is the covering-space monodromy group; no general 'monodromy group' abstraction exists. |
| status | — | partial |
modifiedBase fiber of a covering005b5c39e08d
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | IsCoveringMap.monodromy |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.Topology.Homotopy.Lifting |
| note | — | Mathlib uses the raw preimage `p ⁻¹' {x}` (as in the codomain of `IsCoveringMap.monodromy`) rather than a named 'base fiber' abstraction. |
| status | — | partial |
modifiedLift of a loop through a coveringe6c89495d5dc
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | IsCoveringMap.liftPath |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Topology.Homotopy.Lifting |
| note | — | `IsCoveringMap.liftPath` lifts any path (hence any loop) given a lift of the starting point, with `liftPath_lifts`/`liftPath_zero` witnessing the covering property. |
| status | — | formalized |
modifiedWell-definedness of monodromy action on homotopy classesa9a3791e4835
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | IsCoveringMap.liftPath_apply_one_eq_of_homotopicRel |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Topology.Homotopy.Lifting |
| note | — | Lifting two paths that are homotopic rel `{0,1}` from the same start-point yields lifts with the same endpoint, exactly the well-definedness invoked by `IsCoveringMap.monodromy` on `Path.Homotopic.Quotient`. |
| status | — | formalized |
modifiedMonodromy action on the base fiber54db7cd05554
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | IsCoveringMap.fundamentalGroupMulAction |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Topology.Homotopy.Lifting |
| note | — | `IsCoveringMap.fundamentalGroupMulAction` supplies the `MulAction (FundamentalGroup X x) (p ⁻¹' {x})` directly from `IsCoveringMap.monodromy`. |
| status | — | formalized |
modifiedStabilizer of a point under monodromy7ceabf7b5500
| Field | From #1413 | To #2466 |
|---|
| anchor.snippet | an element | The stabilizer of |
| mathlib.decl | — | IsQuotientCoveringMap.ker_monodromyPerm |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Topology.Homotopy.Lifting |
| note | — | For quotient covering maps Mathlib identifies `ker (monodromyPerm x) = range (mapOfEq p e.2)`; the general 'stabilizer of a fiber point equals image of `π₁(Y,ỹ)`' statement is not stated for arbitrary covers. |
| provenance | ai-agent1 | ai-moderated |
| status | — | partial |
modifiedTopological monodromy group3fab9bfbbee5
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | IsCoveringMap.monodromyPerm |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.Topology.Homotopy.Lifting |
| note | — | The image of `monodromyPerm x` is the topological monodromy group, but Mathlib does not name it as a distinct subgroup. |
| status | — | partial |
modifiedAlgebraic monodromy group8db1dc9e2550
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Zariski-closure/algebraic-group notion of a monodromy representation exists in Mathlib. |
| status | — | not_formalized |
modifiedAnalytic continuation around a puncture (logarithm)31bdabe5e860
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has `Complex.log` and continuation lemmas for L-series but not this monodromy-of-logarithm example. |
| status | — | not_formalized |
addedMonodromy group of the logarithm is infinite cyclicffbef82f2870
modifiedUniversal cover of the punctured plane as helicoid34bfd236486c
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib contains no `helicoid` construction nor an explicit universal cover of the punctured plane. |
| status | — | not_formalized |
modifiedMonodromy group of a linear differential equation2fddf496a215
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib does not develop the monodromy representation attached to solutions of a linear ODE on a complex domain. |
| status | — | not_formalized |
addedRiemann–Hilbert problem (inverse monodromy)64d2b10a60bb
modifiedGenerator relation for Fuchsian monodromy15eea61348f4
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The Fuchsian relation M₁···Mₙ = 1 among loop monodromies is not stated in Mathlib. |
| status | — | not_formalized |
modifiedDeligne–Simpson realisation problemdef36a1a2ad0
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The Deligne–Simpson realisability problem is absent from Mathlib. |
| status | — | not_formalized |
modifiedMonodromy as permutation action on the fiber1acf9c27ac5e
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | IsCoveringMap.monodromyPerm |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Topology.Homotopy.Lifting |
| note | — | `IsCoveringMap.monodromyPerm x : FundamentalGroup X x →* Equiv.Perm (p ⁻¹' {x})` is exactly the permutation-action encoding. |
| status | — | formalized |
modifiedHolonomy group from parallel transport9b5eb2d10ac2
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Grep for `olonomy` in `Mathlib/` returned no files — Mathlib has no holonomy/parallel-transport formalisation. |
| status | — | not_formalized |
modifiedMonodromy groupoid0a50d6e63e36
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | IsCoveringMap.monodromyFunctor |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.Topology.Homotopy.Lifting |
| note | — | `monodromyFunctor : FundamentalGroupoid X ⥤ Type _` records the covering's monodromy as a groupoid representation but is not itself the monodromy groupoid as an object. |
| status | — | partial |
modifiedMonodromy of a foliation via germs086914895d90
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has no geometric-foliation library (only a fleeting mention in `LieRinehartAlgebra`), so germ-based foliation monodromy is absent. |
| status | — | not_formalized |
modifiedField of rational functions and finite extensione60dbe4b6d9e
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | RatFunc |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.FieldTheory.RatFunc.Basic |
| note | — | Mathlib has `RatFunc` and general finite field extensions but no packaged 'function field of a branched cover → finite extension' construction. |
| status | — | partial |
modifiedMonodromy group via Galois closured0ca96584fdb
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | General Galois-theoretic monodromy of a branched cover (as `Gal(L̃/K(X))`) is not stated in Mathlib, though `Gal` and normal closure are available. |
| status | — | not_formalized |
modifiedGroup of deck transformations8a62b6f49c4f
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Grep for `deck`/`DeckTransformation` in `Mathlib/` shows no covering-space deck-transformation group. |
| status | — | not_formalized |
modifiedRiemann existence theorem (connection)98fa0402a5ba
| Field | From #1413 | To #2466 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The Riemann existence theorem linking finite étale covers of a Riemann surface and finite extensions of its function field is not in Mathlib. |
| status | — | not_formalized |