Extending derivations through local Dedekind rings #

Lift derivations uniquely through formally etale maps and apply this to unramified localizations and primes away from the different.

source

def BGS.CorvajaZannier.derivationToRelative {C : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [CommRing C] [CommRing S] [CommRing T] [CommRing U] [Algebra C T] [Algebra S T] [Algebra C U] [Algebra S U] [Algebra T U] [IsScalarTower S T U] (D : Derivation C T U) (hD : ∀ (s : S), D ((algebraMap S T) s) = 0) :

Derivation S T U

A derivation over C which vanishes on S is an S-derivation.

Equations

BGS.CorvajaZannier.derivationToRelative D hD = { toFun := ⇑D, map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

Instances For

source

@[simp]

theorem BGS.CorvajaZannier.derivationToRelative_apply {C : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [CommRing C] [CommRing S] [CommRing T] [CommRing U] [Algebra C T] [Algebra S T] [Algebra C U] [Algebra S U] [Algebra T U] [IsScalarTower S T U] (D : Derivation C T U) (hD : ∀ (s : S), D ((algebraMap S T) s) = 0) (t : T) :

(derivationToRelative D hD) t = D t

source

theorem BGS.CorvajaZannier.derivation_ext_of_formallyUnramified {C : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [CommRing C] [CommRing S] [CommRing T] [CommRing U] [Algebra C T] [Algebra S T] [Algebra C U] [Algebra S U] [Algebra T U] [IsScalarTower S T U] [Algebra.FormallyUnramified S T] (D₁ D₂ : Derivation C T U) (hD : ∀ (s : S), D₁ ((algebraMap S T) s) = D₂ ((algebraMap S T) s)) :

D₁ = D₂

Relative formal unramifiedness makes a C-derivation into a T-module unique once its restriction to S is fixed.

source

noncomputable def BGS.CorvajaZannier.formallyEtaleDerivationLift {C : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [CommRing C] [CommRing S] [CommRing T] [CommRing U] [Algebra C S] [Algebra C T] [Algebra S T] [Algebra C U] [Algebra S U] [Algebra T U] [IsScalarTower C S T] [IsScalarTower C S U] [IsScalarTower C T U] [IsScalarTower S T U] [Algebra.FormallyEtale S T] (D : Derivation C S U) :

Derivation C T U

Lift a C-derivation through a formally étale S-algebra. The target may be any compatible T-algebra.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem BGS.CorvajaZannier.formallyEtaleDerivationLift_algebraMap {C : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [CommRing C] [CommRing S] [CommRing T] [CommRing U] [Algebra C S] [Algebra C T] [Algebra S T] [Algebra C U] [Algebra S U] [Algebra T U] [IsScalarTower C S T] [IsScalarTower C S U] [IsScalarTower C T U] [IsScalarTower S T U] [Algebra.FormallyEtale S T] (D : Derivation C S U) (s : S) :

(formallyEtaleDerivationLift D) ((algebraMap S T) s) = D s

source

theorem BGS.CorvajaZannier.formallyEtaleDerivationLift_unique {C : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [CommRing C] [CommRing S] [CommRing T] [CommRing U] [Algebra C S] [Algebra C T] [Algebra S T] [Algebra C U] [Algebra S U] [Algebra T U] [IsScalarTower C S T] [IsScalarTower C S U] [IsScalarTower C T U] [IsScalarTower S T U] [Algebra.FormallyEtale S T] (D : Derivation C S U) (E : Derivation C T U) (hE : ∀ (s : S), E ((algebraMap S T) s) = D s) :

E = formallyEtaleDerivationLift D

The formally étale lift is the unique extension of the given derivation.

source

noncomputable def BGS.CorvajaZannier.formallyEtaleDerivationExtension {C : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing C] [CommRing S] [CommRing T] [Algebra C S] [Algebra C T] [Algebra S T] [IsScalarTower C S T] [Algebra.FormallyEtale S T] (D : Derivation C S S) :

Derivation C T T

Extend a derivation taking values in the base ring to one taking values in the formally étale algebra.

Equations

BGS.CorvajaZannier.formallyEtaleDerivationExtension D = BGS.CorvajaZannier.formallyEtaleDerivationLift ((Algebra.linearMap S T).compDer D)

Instances For

source

@[simp]

theorem BGS.CorvajaZannier.formallyEtaleDerivationExtension_algebraMap {C : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing C] [CommRing S] [CommRing T] [Algebra C S] [Algebra C T] [Algebra S T] [IsScalarTower C S T] [Algebra.FormallyEtale S T] (D : Derivation C S S) (s : S) :

(formallyEtaleDerivationExtension D) ((algebraMap S T) s) = (algebraMap S T) (D s)

source

theorem BGS.CorvajaZannier.formallyEtale_derivation_preserves {C : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [CommRing C] [CommRing S] [CommRing T] [CommRing U] [Algebra C S] [Algebra C T] [Algebra S T] [Algebra C U] [Algebra S U] [Algebra T U] [IsScalarTower C S T] [IsScalarTower C T U] [IsScalarTower S T U] [Algebra.FormallyEtale S T] (D : Derivation C S S) (E : Derivation C U U) (hE : ∀ (s : S), E ((algebraMap S U) s) = (algebraMap S U) (D s)) :

∃ (D' : Derivation C T T), (∀ (s : S), D' ((algebraMap S T) s) = (algebraMap S T) (D s)) ∧ ∀ (t : T), E ((algebraMap T U) t) = (algebraMap T U) (D' t)

If an ambient derivation preserves the base local ring, then it preserves every formally étale extension ring inside the ambient algebra.

source

theorem BGS.CorvajaZannier.dedekindLocal_formallyEtale_of_isUnramifiedAt {A : Type u_5} {B : Type u_6} [CommRing A] [CommRing B] [IsDedekindDomain A] [Algebra A B] [Module.IsTorsionFree A B] [Module.Finite A B] (p : Ideal A) (Q : Ideal B) [p.IsPrime] [Q.IsPrime] [Algebra (Localization.AtPrime p) (Localization.AtPrime Q)] [IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime Q)] [Algebra.IsUnramifiedAt A Q] :

Algebra.FormallyEtale (Localization.AtPrime p) (Localization.AtPrime Q)

A finite torsion-free extension of Dedekind domains is formally étale on the local branch at every unramified prime.

source

theorem BGS.CorvajaZannier.dedekindLocal_formallyEtale_of_not_dvd_different {A : Type u_5} {B : Type u_6} [CommRing A] [CommRing B] [IsDedekindDomain A] [IsDedekindDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] (p : Ideal A) (Q : Ideal B) [p.IsPrime] [Q.IsPrime] [Algebra (Localization.AtPrime p) (Localization.AtPrime Q)] [IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime Q)] (hQ : ¬Q ∣ differentIdeal A B) :

Algebra.FormallyEtale (Localization.AtPrime p) (Localization.AtPrime Q)

Outside the different ideal, the corresponding map of Dedekind local rings is formally étale.

source

∃ (D' : Derivation C (Localization.AtPrime Q) (Localization.AtPrime Q)), (∀ (s : Localization.AtPrime p), D' ((algebraMap (Localization.AtPrime p) (Localization.AtPrime Q)) s) = (algebraMap (Localization.AtPrime p) (Localization.AtPrime Q)) (D s)) ∧ ∀ (t : Localization.AtPrime Q), E ((algebraMap (Localization.AtPrime Q) U) t) = (algebraMap (Localization.AtPrime Q) U) (D' t)

An ambient derivation preserving the base Dedekind local ring preserves an unramified local branch of a finite torsion-free Dedekind extension.

source

Away from the different, an ambient derivation preserving the base local ring preserves the selected extension DVR. This is the direct local derivation-extension statement used in the Corvaja--Zannier argument.

Documentation

LeanPool.MarkoffModP.BGS.CorvajaZannier.DedekindLocalDerivationExtension

Extending derivations through local Dedekind rings #