6. mapping degree
The mapping degree machine: regular values, critical-value finiteness, fibre counting, well-definedness of the degree (largest unit; contains the ported degree-well-definedness tree).
49 modules, 8,645 lines, under Jacobians/MappingDegree/.
- 6.1. Keystones
- 6.2. Builds on
- 6.3. MappingDegree
- 6.4. MappingDegree.AnalyticContinuationGlobalization
- 6.5. MappingDegree.AnalyticFiberDiscrete
- 6.6. MappingDegree.AnalyticKthRoot
- 6.7. MappingDegree.ChartBallOffCentreWitnessDischarge
- 6.8. MappingDegree.ChartLocalDetour
- 6.9. MappingDegree.ChartOverlapAvoidanceFull
- 6.10. MappingDegree.ChartOverlapPropagationDischarge
- 6.11. MappingDegree.ChartPullbackDataConstruction
- 6.12. MappingDegree.ChartPullbackNotEventuallyConstDischarge
- 6.13. MappingDegree.ChartRestrictionToBall
- 6.14. MappingDegree.ChartedSpaceLocPathConnected
- 6.15. MappingDegree.ClopennessOfLocallyConstDischarge
- 6.16. MappingDegree.ConnectedManifoldPathConnected
- 6.17. MappingDegree.ConnectivityGlobalizationReduction
- 6.18. MappingDegree.CriticalSetDerivBridge
- 6.19. MappingDegree.CriticalSetDiscrete
- 6.20. MappingDegree.CriticalValueSetFinite
- 6.21. MappingDegree.CriticalValuesFiniteGeneral
- 6.22. MappingDegree.Degree
- 6.23. MappingDegree.DegreeWellDefined
- 6.24. MappingDegree.FibreCardLocallyConstantFromNormalForm
- 6.25. MappingDegree.FibreCardOnRegularSubset
- 6.26. MappingDegree.FibreCardWellDefinedAtRegular
- 6.27. MappingDegree.FibresFiniteAssembly
- 6.28. MappingDegree.FibresFiniteUnconditional
- 6.29. MappingDegree.HLcUnconditional
- 6.30. MappingDegree.HPkgUnconditional
- 6.31. MappingDegree.HurwitzPatchingDataConstruction
- 6.32. MappingDegree.HurwitzWellDefinedFromHPath
- 6.33. MappingDegree.HurwitzWellDefinedUnconditionalTopo
- 6.34. MappingDegree.IsPathConnectedBallMinusCountable
- 6.35. MappingDegree.LocalKFoldMultiplicity
- 6.36. MappingDegree.LocalKFoldMultiplicityFullyUnconditional
- 6.37. MappingDegree.LocalKFoldMultiplicityUnconditional
- 6.38. MappingDegree.LocalMultiplicityInvariance
- 6.39. MappingDegree.LocalNormalForm
- 6.40. MappingDegree.LocalSheetDataAtRegularValue
- 6.41. MappingDegree.LocalSheetDataFromContMDiff
- 6.42. MappingDegree.MeromorphicDivisor
- 6.43. MappingDegree.PathConnectedComplFinite
- 6.44. MappingDegree.PathSubdivisionByBallCharts
- 6.45. MappingDegree.PerChartNonConstancyReduction
- 6.46. MappingDegree.PreconnectedFromFiniteComplement
- 6.47. MappingDegree.RegularSubsetPreconnected
- 6.48. MappingDegree.RegularValueExistsRegUnconditional
- 6.49. MappingDegree.RegularValueExistsUnconditional
- 6.50. MappingDegree.RoucheBridge
- 6.51. MappingDegree.WithinChartWitnessReduction