RegularJets.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Isolated jets on regular charts

Euler operators and transverse derivatives isolate a least boundary monomial. Faithful flatness descends the resulting congruence from formal power series to the regular coordinate chart.

theorem OAI.CartierSections.isolated_unit_descends line 24

Source documentation

A unit coefficient modulo a proper extended colon ideal descends along a faithfully flat local algebra map.

theorem isolated_unit_descends
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [IsLocalRing S] [IsLocalHom (algebraMap R S)] [Module.FaithfullyFlat R S]
    (I : Ideal R) (a g : R)
    (ha : algebraMap R S a ∉ I.map (algebraMap R S))
    (u q : S) (hu : IsUnit u) (hq : q ∈ I.map (algebraMap R S))
    (heq : algebraMap R S g = u * algebraMap R S a + q) :
    ∃ v r : R, IsUnit v ∧ r ∈ I ∧ g = v * a + r := by
…

theorem OAI.CartierSections.isolated_unit_descends_from_completion line 70

Source documentation

In the actual maximal-ideal completion, both the locality and faithful flatness needed for descent follow from Noetherian locality.

theorem isolated_unit_descends_from_completion
    {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (I : Ideal R) (a g : R)
    (ha : algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R) a ∉
      I.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)))
    (u q : AdicCompletion (IsLocalRing.maximalIdeal R) R)
    (hu : IsUnit u)
    (hq : q ∈ I.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)))
    (heq : algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R) g =
      u * algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R) a + q) :
    ∃ v r : R, IsUnit v ∧ r ∈ I ∧ g = v * a + r := by
…

def OAI.CartierSections.chartEulerStep line 93
def OAI.CartierSections.chartIterEuler line 97
def OAI.CartierSections.chartIterPartial line 101
theorem OAI.CartierSections.chartIterEuler_series line 110
theorem OAI.CartierSections.chartIterPartial_series line 118
theorem OAI.CartierSections.chart_polynomial_series line 126
def OAI.CartierSections.chartBoundaryWeightIdeal line 137
Source documentation
The monomial ideal of boundary exponents above a given weight in the local chart.
```
noncomputable def chartBoundaryWeightIdeal (B : Finset ι) (w : ι → ℝ) (L : ℝ) : Ideal A :=
…
```
theorem OAI.CartierSections.chartBoundaryWeightIdeal_map line 142

theorem OAI.CartierSections.regular_chart_isolated_jet line 156

Source documentation

Isolation of an initial boundary monomial by regular differential operators. The power series calculation descends to the chart by faithful flatness.

theorem regular_chart_isolated_jet [CharZero k]
    [Algebra A (MvPowerSeries ι k)] [IsScalarTower k A (MvPowerSeries ι k)]
    [Module.FaithfullyFlat A (MvPowerSeries ι k)]
    [IsLocalHom (algebraMap A (MvPowerSeries ι k))]
    (hθ : θ.toRingHom = algebraMap A (MvPowerSeries ι k))
    (f : A) (hf : θ f ≠ 0) (s : Finset ℕ) (p : ℕ → MvPolynomial ι k) (N : ℕ)
    (hdeg : ∀ j ∈ s, (p j).totalDegree ≤ N) (hnonzero : ∃ j ∈ s, p j ≠ 0)
    (hrelation : ∑ j ∈ s, (p j : MvPowerSeries ι k) * (θ f)^j = 0)
    (w : ι → ℝ) (hw : ∀ i, 0 ≤ w i) (B : Finset ι)
    (hB : ∀ i ∈ B, 0 < w i) (hwzero : ∀ i ∉ B, w i = 0) :
    ∃ (γ α β : ι →₀ ℕ) (u q : A),
      IsInitialExponent w (θ f) γ ∧ exponentDegree γ ≤ N ∧
…

Mentions: OAI.CartierSections.IsInitialExponent, OAI.CartierSections.exponentDegree