EtaleDerivatives.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Derivations on étale coordinate charts

Formally étale coordinate derivations satisfy the coordinate chain rule and commute with expansion in multivariate power series. These are the regular differential operators used in the logarithmic jet estimate for uniform Cartier sections.

def OAI.CartierSections.extendEtaleDerivation line 24
theorem OAI.CartierSections.extendEtaleDerivation_algebraMap line 29
theorem OAI.CartierSections.etale_derivation_ext line 39
Source documentation
Formally étale coordinates determine a derivation, not only its values on coordinate polynomials.
```
theorem etale_derivation_ext (D E : Derivation k T M)
    (h : ∀ a : A, D (algebraMap A T a) = E (algebraMap A T a)) : D = E := by
…
```
theorem OAI.CartierSections.derivation_sum_apply line 64
def OAI.CartierSections.etalePartial line 81
Source documentation
The partial derivatives on a formally étale coordinate chart, obtained from the cotangent-space base-change isomorphism.
```
noncomputable def etalePartial (i : ι) : Derivation k T T :=
…
```
theorem OAI.CartierSections.etalePartial_coordinate line 85
theorem OAI.CartierSections.etale_coordinate_chain_rule line 94
Source documentation
The ordinary chain rule holds for all functions on the étale chart, not just for coordinate polynomials.
```
theorem etale_coordinate_chain_rule [Fintype ι] (D : Derivation k T T) (f : T) :
    D f = ∑ i : ι, D (algebraMap (MvPolynomial ι k) T (MvPolynomial.X i)) *
        etalePartial (k := k) (T := T) i f := by
…
```
Mentions: OAI.CartierSections.etalePartial

theorem OAI.CartierSections.etale_coordinate_chain_rule_to line 110

Source documentation

Coordinate chain rule with values in an algebra over the coordinate chart. This is the form needed after pullback to the DVR of a divisor on a model.

theorem etale_coordinate_chain_rule_to [Fintype ι] {R : Type*} [CommRing R]
    [Algebra k R] [Algebra T R] [IsScalarTower k T R]
    (D : Derivation k T R) (f : T) :
    D f = ∑ i : ι, D (algebraMap (MvPolynomial ι k) T (MvPolynomial.X i)) *
        algebraMap T R (etalePartial (k := k) (T := T) i f) := by
…

Mentions: OAI.CartierSections.etalePartial

theorem OAI.CartierSections.etalePartial_series_natural line 140

Source documentation

The coordinate derivatives commute with formal expansion by formal unramifiedness.

theorem etalePartial_series_natural
    {k T ι : Type*} [Field k] [CommRing T]
    [Algebra k T] [Algebra (MvPolynomial ι k) T]
    [IsScalarTower k (MvPolynomial ι k) T]
    [Algebra.FormallyEtale (MvPolynomial ι k) T]
    (θ : T →ₐ[k] MvPowerSeries ι k)
    (hz : ∀ i, θ (algebraMap (MvPolynomial ι k) T (MvPolynomial.X i)) = MvPowerSeries.X i)
    (i : ι) (f : T) :
    θ (etalePartial (k := k) (T := T) i f) = MvPowerSeries.pderiv (R := k) i (θ f) := by
…

Mentions: OAI.CartierSections.etalePartial