Documentation

Hironaka.Algebra.Derivative.Equiv

The derivative ideal along an algebra isomorphism #

D(e(J)) = e(D(J)) for a k-algebra isomorphism e : A ≃ₐ[k] B, and Dʳ(e(J)) = e(Dʳ(J)) for the iterates: the k-derivations of B are the conjugates e ∘ δ ∘ e⁻¹ of those of A (Derivation.conjAlgEquiv), so the generators δ f of D(J) correspond. This is the case of an isomorphism of [Kol07, Lemma 74 (4)], the compatibility of D with smooth pull-back; it is used on manifolds for the stalk maps of local analytic isomorphisms (Hironaka/Resolution/Analytic/MaximalContact/StalkEquiv.lean, Hironaka/Resolution/Analytic/OrderReduction/BDLemmas.lean). The derivative ideal is Ideal.derivative of Hironaka/Algebra/Derivative/Basic.lean.

source
def Derivation.conjAlgEquiv {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] (e : A ≃ₐ[k] B) (δ : Derivation k A A) :
Derivation k B B

The conjugate e ∘ δ ∘ e⁻¹ of a k-derivation of A along a k-algebra isomorphism e : A ≃ₐ[k] B, a k-derivation of B.

Equations
Instances For
    source
    theorem Derivation.conjAlgEquiv_apply {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] (e : A ≃ₐ[k] B) (δ : Derivation k A A) (b : B) :
    (conjAlgEquiv e δ) b = e (δ (e.symm b))
    source
    theorem Ideal.derivative_map_algEquiv {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] (e : A ≃ₐ[k] B) (J : Ideal A) :
    derivative k (map e J) = map e (derivative k J)

    The case of an isomorphism of [Kol07, Lemma 74 (4)]: the derivative of the image ideal is the image of the derivative.

    source
    theorem Ideal.derivativeIter_map_algEquiv {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] (e : A ≃ₐ[k] B) (r : ℕ) (J : Ideal A) :
    derivativeIter k r (map e J) = map e (derivativeIter k r J)

    The iterated derivatives along an isomorphism.