OAI/Topology/EilenbergGanea/Regularization.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EilenbergGanea.complex_smul_decompose line 25
2. theorem OAI.EilenbergGanea.realLinear_map_complex_smul line 34

   Source documentation

   Commuting with a non-real scalar forces a real-linear map to be complex-linear.

   theorem realLinear_map_complex_smul (f : V →ₗ[ℝ] V) (z : ℂ) (hz : z.im ≠ 0)
       (hf : ∀ x, f (z • x) = z • f x) (w : ℂ) (x : V) :
       f (w • x) = w • f x := by
   …

3. theorem OAI.EilenbergGanea.complexLinear_of_commutes_nonreal line 45
4. theorem OAI.EilenbergGanea.rotation_commutant_blocks line 62

   Source documentation

   A real derivative commuting with the fixed-plus-rotating representation has no mixed blocks. Its normal block is complex-linear.

   theorem rotation_commutant_blocks (L : A × V →ₗ[ℝ] A × V)
       (z : ℂ) (hz : z.im ≠ 0)
       (h : ∀ a v, L (a, z • v) = ((L (a, v)).1, z • (L (a, v)).2)) :
       ∃ (T : A →ₗ[ℝ] A) (N : V →ₗ[ℂ] V),
         L = T.prodMap (N.restrictScalars ℝ) := by
   …

5. theorem OAI.EilenbergGanea.complex_real_det_nonneg line 115
6. theorem OAI.EilenbergGanea.complex_real_det_pos line 120
7. theorem OAI.EilenbergGanea.exists_small_simultaneous_regular_shift line 132

   Source documentation

   A single real scalar regularizes any finite collection of normal blocks.

   theorem exists_small_simultaneous_regular_shift {ι : Type*} [Fintype ι]
       (N : ι → Module.End ℂ V) {ε : ℝ} (hε : 0 < ε) :
       ∃ s : ℝ, |s| < ε ∧ ∀ i, IsUnit (N i + algebraMap ℂ (Module.End ℂ V) (s : ℂ)) := by
   …

8. theorem OAI.EilenbergGanea.equivariant_fderiv line 157
9. theorem OAI.EilenbergGanea.equivariant_fderiv_det line 168
10. def OAI.EilenbergGanea.normalProjection line 183

    Source documentation

    The complement of the fixed subspace.

    def normalProjection : (A × V) →L[ℝ] (A × V) :=
    …

11. theorem OAI.EilenbergGanea.normalProjection_apply line 186
12. def OAI.EilenbergGanea.normalShift line 188
13. theorem OAI.EilenbergGanea.normalShift_contDiff line 190
14. theorem OAI.EilenbergGanea.normalShift_fderiv line 195
15. theorem OAI.EilenbergGanea.normalShift_fixed line 199
16. def OAI.EilenbergGanea.scalarRotation line 204
17. theorem OAI.EilenbergGanea.scalarRotation_apply line 208
18. theorem OAI.EilenbergGanea.fixed_fderiv_blocks line 212

    Source documentation

    At a fixed point the derivative splits with a complex-linear normal block.

    theorem fixed_fderiv_blocks (f : A × V → A × V) (hf : Differentiable ℝ f)
        (z : ℂˣ) (hz : (z : ℂ).im ≠ 0)
        (he : ∀ q, f (scalarRotation z q) = scalarRotation z (f q)) (a : A) :
        ∃ (T : A →ₗ[ℝ] A) (N : V →ₗ[ℂ] V),
          (fderiv ℝ f (a, 0)).toLinearMap = T.prodMap (N.restrictScalars ℝ) := by
    …

    Mentions: OAI.EilenbergGanea.scalarRotation

19. theorem OAI.EilenbergGanea.normalShift_fixed_det line 225

    Source documentation

    Scalar shifts have the claimed fixed-block Jacobian, with no chart convention.

    theorem normalShift_fixed_det (f : A × V → A × V) (hf : Differentiable ℝ f)
        (a : A) (T : A →ₗ[ℝ] A) (N : V →ₗ[ℂ] V)
        (h : (fderiv ℝ f (a, 0)).toLinearMap = T.prodMap (N.restrictScalars ℝ)) (s : ℝ) :
        (fderiv ℝ (normalShift f s) (a, 0)).det =
          T.det * ((N + algebraMap ℂ (Module.End ℂ V) (s : ℂ)).restrictScalars ℝ).det := by
    …

    Mentions: OAI.EilenbergGanea.normalShift

20. def OAI.EilenbergGanea.fixedRestriction line 249
21. theorem OAI.EilenbergGanea.fixedRestriction_fderiv line 252
22. theorem OAI.EilenbergGanea.exists_normalShift_regular_fixed line 267

    Source documentation

    Simultaneously regularize the finite fixed fiber, retaining its tangent sign.

    theorem exists_normalShift_regular_fixed (f : A × V → A × V) (hf : Differentiable ℝ f)
        (z : ℂˣ) (hz : (z : ℂ).im ≠ 0)
        (he : ∀ q, f (scalarRotation z q) = scalarRotation z (f q))
        (S : Finset A) (c : ℝ) (hc : c ≠ 0)
        (hT : ∀ a ∈ S, (fderiv ℝ (fixedRestriction f) a).det = c)
        (ε : ℝ) (hε : 0 < ε) :
        ∃ s : ℝ, |s| < ε ∧ ∀ a ∈ S,
          (fderiv ℝ (normalShift f s) (a, 0)).det ≠ 0 ∧
          (0 < (fderiv ℝ (normalShift f s) (a, 0)).det ↔ 0 < c) := by
    …

    Mentions: OAI.EilenbergGanea.scalarRotation, OAI.EilenbergGanea.fixedRestriction, OAI.EilenbergGanea.normalShift

23. def OAI.EilenbergGanea.linearPerturbation line 298
24. def OAI.EilenbergGanea.linearPerturbationDerivative line 301
25. theorem OAI.EilenbergGanea.linearPerturbation_hasFDerivAt line 306
26. def OAI.EilenbergGanea.linearSolvedParameter line 315
27. theorem OAI.EilenbergGanea.linearSolvedParameter_outside line 320
28. theorem OAI.EilenbergGanea.inverse_apply_cancel line 326
29. theorem OAI.EilenbergGanea.apply_inverse_cancel line 330
30. theorem OAI.EilenbergGanea.linearSolvedParameter_root line 334
31. theorem OAI.EilenbergGanea.linearSolvedParameter_differentiableAt line 350
32. theorem OAI.EilenbergGanea.linearSolvedParameter_fderiv_outside line 368
33. theorem OAI.EilenbergGanea.linearSolvedParameter_differential_relation line 380
34. theorem OAI.EilenbergGanea.linearSolvedParameter_recovers_root line 409
35. theorem OAI.EilenbergGanea.linearSolvedParameter_critical line 429
36. theorem OAI.EilenbergGanea.ae_regular_linear_parameters line 469

    Source documentation

    Transversality with source-dependent linear parameter blocks, including finite equivariant bump perturbations. Only invertibility of a single active block is required at each root.

    theorem ae_regular_linear_parameters [MeasurableSpace E] [BorelSpace E]
        (μ : MeasureTheory.Measure (ι → E)) [μ.IsAddHaarMeasure]
        (f : E → E) (T : ι → E → (E →L[ℝ] E)) (s : Set E)
        (hf : ∀ x ∈ s, DifferentiableAt ℝ f x)
        (hT : ∀ i x, x ∈ s → DifferentiableAt ℝ (T i) x) :
        ∀ᵐ p ∂μ, ∀ x ∈ s, linearPerturbation f T x p = 0 →
          (∃ i, IsUnit (T i x)) → (linearPerturbationDerivative f T x p).det ≠ 0 := by
    …

    Mentions: OAI.EilenbergGanea.linearPerturbation, OAI.EilenbergGanea.linearPerturbationDerivative

37. def OAI.EilenbergGanea.equivariantBumpOperator line 514
38. theorem OAI.EilenbergGanea.representation_cancel line 518
39. theorem OAI.EilenbergGanea.representation_mul_apply line 525
40. theorem OAI.EilenbergGanea.equivariantBumpOperator_equivariant line 528
41. theorem OAI.EilenbergGanea.equivariantBumpOperator_contDiff line 542
42. theorem OAI.EilenbergGanea.unit_smul_equiv line 548
43. theorem OAI.EilenbergGanea.equivariantBumpOperator_isUnit line 556
44. theorem OAI.EilenbergGanea.free_orbit_disjoint_neighborhood line 574

    Source documentation

    A free orbit for a finite linear action has a neighborhood with pairwise disjoint translates. No isometry hypothesis or metric constants are needed.

    theorem free_orbit_disjoint_neighborhood (ρ : G →* E ≃L[ℝ] E) (x : E)
        (hx : ∀ g : G, ρ g x = x → g = 1) (W : Set E) (hW : IsOpen W) (hxW : x ∈ W) :
        ∃ V : Set E, IsOpen V ∧ x ∈ V ∧ V ⊆ W ∧
          Pairwise fun g h : G => Disjoint (ρ g '' V) (ρ h '' V) := by
    …

45. theorem OAI.EilenbergGanea.free_orbit_smooth_bump line 611

    Source documentation

    The bump family used in the free part of the localized-degree argument. Its complete closed support has disjoint translates, so each active parameter block is invertible.

    theorem free_orbit_smooth_bump (ρ : G →* E ≃L[ℝ] E) (x : E)
        (hx : ∀ g : G, ρ g x = x → g = 1) (W : Set E) (hW : IsOpen W) (hxW : x ∈ W) :
        ∃ b : E → ℝ, ContDiff ℝ ∞ b ∧ HasCompactSupport b ∧ tsupport b ⊆ W ∧ b x = 1 ∧
          Pairwise fun g h : G => Disjoint (ρ g '' tsupport b) (ρ h '' tsupport b) := by
    …

46. theorem OAI.EilenbergGanea.compact_root_good_stability line 631
47. theorem OAI.EilenbergGanea.compact_free_bump_family line 651
48. theorem OAI.EilenbergGanea.linearPerturbation_contDiff line 683
49. theorem OAI.EilenbergGanea.linearPerturbationDerivative_continuous line 692
50. theorem OAI.EilenbergGanea.exists_regular_linear_perturbation line 705

    Source documentation

    A finite linear bump family regularizes all roots on a compact set, provided it has an invertible block at every initially critical root. The parameters can be chosen in any prescribed neighborhood of zero.

    theorem exists_regular_linear_perturbation
        (μ : MeasureTheory.Measure (ι → E)) [μ.IsAddHaarMeasure]
        (f : E → E) (T : ι → E → (E →L[ℝ] E))
        (hf : ContDiff ℝ ∞ f) (hT : ∀ i, ContDiff ℝ ∞ (T i))
        (K : Set E) (hK : IsCompact K)
        (hcover : ∀ x ∈ K, f x = 0 → (fderiv ℝ f x).det = 0 → ∃ i, IsUnit (T i x))
        (U : Set (ι → E)) (hU : U ∈ 𝓝 0) :
        ∃ p ∈ U, ∀ x ∈ K, linearPerturbation f T x p = 0 →
          (linearPerturbationDerivative f T x p).det ≠ 0 := by
    …

    Mentions: OAI.EilenbergGanea.linearPerturbation, OAI.EilenbergGanea.linearPerturbationDerivative

51. theorem OAI.EilenbergGanea.equivariantBumpOperator_eventually_zero_outside line 763
52. theorem OAI.EilenbergGanea.exists_equivariant_regular_perturbation line 787

    Source documentation

    The free-action regularization step. Critical roots must lie in the free locus, but already regular fixed roots need not. The perturbation is unchanged outside any chosen invariant open neighborhood of the critical roots.

    theorem exists_equivariant_regular_perturbation
        (ρ : G →* E ≃L[ℝ] E) (f : E → E) (hf : ContDiff ℝ ∞ f)
        (heq : ∀ g x, f (ρ g x) = ρ g (f x))
        (K W : Set E) (hK : IsCompact K) (hW : IsOpen W)
        (hinv : ∀ g x, x ∈ W → ρ g x ∈ W)
        (hcritical : ∀ x ∈ K, f x = 0 → (fderiv ℝ f x).det = 0 →
          x ∈ W ∧ ∀ g : G, ρ g x = x → g = 1)
        (ε : ℝ) (hε : 0 < ε) :
        ∃ g : E → E, ContDiff ℝ ∞ g ∧ (∀ a x, g (ρ a x) = ρ a (g x)) ∧
          (∀ x ∉ W, g =ᶠ[𝓝 x] f) ∧ (∀ x ∈ K, ‖g x - f x‖ < ε) ∧
          ∀ x ∈ K, g x = 0 → (fderiv ℝ g x).det ≠ 0 := by
    …

53. def OAI.EilenbergGanea.scalarRotationRepresentation line 860
54. theorem OAI.EilenbergGanea.scalarRotationRepresentation_apply line 874
55. theorem OAI.EilenbergGanea.scalarRotation_free line 878
56. theorem OAI.EilenbergGanea.normalShift_equivariant line 892
57. theorem OAI.EilenbergGanea.exists_fixed_free_regularization line 904

    Source documentation

    The full fixed-plus-free regularization step in fixed/normal coordinates. Unlike an assumed transversality interface, this is assembled from the finite normal spectrum argument and explicit free-orbit bump parameters above.

    theorem exists_fixed_free_regularization (χ : G →* ℂˣ) (hχ : Function.Injective χ)
        (a₀ : G) (ha₀ : (χ a₀ : ℂ).im ≠ 0)
        (f : A × V → A × V) (hf : ContDiff ℝ ∞ f)
        (he : ∀ g q, f (scalarRotationRepresentation χ g q) =
          scalarRotationRepresentation χ g (f q))
        (K : Set (A × V)) (hK : IsCompact K) (S : Finset A)
        (hS : ∀ a, (a, 0) ∈ K → f (a, 0) = 0 → a ∈ S)
        (c : ℝ) (hc : c ≠ 0)
        (hT : ∀ a ∈ S, (fderiv ℝ (fixedRestriction f) a).det = c)
        (ε : ℝ) (hε : 0 < ε) :
        ∃ g : A × V → A × V, ContDiff ℝ ∞ g ∧
          (∀ a q, g (scalarRotationRepresentation χ a q) =
    …

    Mentions: OAI.EilenbergGanea.scalarRotationRepresentation, OAI.EilenbergGanea.fixedRestriction

58. def OAI.EilenbergGanea.invariantSubtypeAction line 979
59. theorem OAI.EilenbergGanea.signed_finite_action_nonzero line 985
60. theorem OAI.EilenbergGanea.exists_regular_inverse_patch line 1044

    Source comment

    A nonsingular derivative supplies an open inverse patch, without assuming that the map is proper or globally injective.

    theorem exists_regular_inverse_patch (f : E → E) {x : E}
        (hf : ContDiffAt ℝ 1 f x) (hd : (fderiv ℝ f x).det ≠ 0) :
        ∃ V : Set E, IsOpen V ∧ x ∈ V ∧ InjOn f V ∧
          IsOpen (f '' V) := by
    …

61. theorem OAI.EilenbergGanea.regular_fiber_isDiscrete line 1062

    Source comment

    A regular level set is discrete. Only smoothness at the level set is required.

    theorem regular_fiber_isDiscrete (f : E → E) (y : E) (K : Set E)
        (hf : ∀ x ∈ K, f x = y → ContDiffAt ℝ 1 f x)
        (hd : ∀ x ∈ K, f x = y → (fderiv ℝ f x).det ≠ 0) :
        IsDiscrete (K ∩ f ⁻¹' {y}) := by
    …

62. theorem OAI.EilenbergGanea.compact_regular_fiber_finite line 1079

    Source comment

    Compact regular fibers are finite, in the form needed by the signed count formula after regularization.

    theorem compact_regular_fiber_finite (f : E → E) (y : E) (K : Set E)
        (hK : IsCompact K) (hf : ContinuousOn f K)
        (hs : ∀ x ∈ K, f x = y → ContDiffAt ℝ 1 f x)
        (hd : ∀ x ∈ K, f x = y → (fderiv ℝ f x).det ≠ 0) :
        (K ∩ f ⁻¹' {y}).Finite := by
    …

63. theorem OAI.EilenbergGanea.exists_regularization_nonzero_count line 1101

    Source documentation

    The localized noncancellation part of degree, now for actual regular perturbations of a smooth map, not an assumed finite-orbit-count interface.

    theorem exists_regularization_nonzero_count {p : ℕ} [Fact p.Prime]
        (hG : IsPGroup p G) (χ : G →* ℂˣ) (hχ : Function.Injective χ)
        (a₀ : G) (ha₀ : (χ a₀ : ℂ).im ≠ 0)
        (f : A × V → A × V) (hf : ContDiff ℝ ∞ f)
        (he : ∀ a q, f (scalarRotationRepresentation χ a q) =
          scalarRotationRepresentation χ a (f q))
        (K : Set (A × V)) (hK : IsCompact K)
        (hKi : ∀ a q, q ∈ K → scalarRotationRepresentation χ a q ∈ K)
        (L : Set (A × V)) (hL : IsCompact L) (hKL : K ⊆ L)
        (S : Finset A) (hS : ∀ a, (a, 0) ∈ L → f (a, 0) = 0 → a ∈ S)
        (hex : ∃ a, (a, 0) ∈ K ∧ f (a, 0) = 0) (hSp : S.card < p)
        (c : ℝ) (hc : c ≠ 0)
    …

    Mentions: OAI.EilenbergGanea.scalarRotationRepresentation