DerivationOperations.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Transport, scaling, and descent of derivations through algebra homomorphisms.

def OAI.AbhyankarSathaye.CommutingDerivations.LocallyNilpotent line 17
Source documentation
Literal pointwise local nilpotence; there is no uniform exponent requirement.
Distinct definitions of this name: ComparatorChallenges/CommutingDerivations.lean:49 (same statement text; different proof or body). Qualify references as OAI.AbhyankarSathaye.CommutingDerivations.LocallyNilpotent@path.
```
def LocallyNilpotent (D : Derivation K A A) : Prop :=
…
```
def OAI.AbhyankarSathaye.CommutingDerivations.transportDerivation line 21
Source documentation
Pull a derivation back through an actual algebra equivalence.
```
def transportDerivation (e : A ≃ₐ[K] B) (D : Derivation K B B) : Derivation K A A where
…
```
theorem OAI.AbhyankarSathaye.CommutingDerivations.transportDerivation_apply line 30
theorem OAI.AbhyankarSathaye.CommutingDerivations.transportDerivation_iterate line 34
theorem OAI.AbhyankarSathaye.CommutingDerivations.transportDerivation_locallyNilpotent line 42
theorem OAI.AbhyankarSathaye.CommutingDerivations.transportDerivation_commute line 49

theorem OAI.AbhyankarSathaye.CommutingDerivations.scaleDerivation_iterate line 56

Source documentation

Multiplication by a kernel element gives the exact nth-iterate formula.

theorem scaleDerivation_iterate (D : Derivation K A A) (c : A) (hc : D c = 0)
    (n : ℕ) (a : A) :
    ((c • D : Derivation K A A) : A → A)^[n] a = c^n * (D : A → A)^[n] a := by
…

theorem OAI.AbhyankarSathaye.CommutingDerivations.scaleDerivation_locallyNilpotent line 68

theorem OAI.AbhyankarSathaye.CommutingDerivations.scaleDerivation_commute line 75

Source documentation

Different multipliers may be used if both lie in both kernels.

theorem scaleDerivation_commute (D E : Derivation K A A) (a b : A)
    (hDb : D b = 0) (hEa : E a = 0) (hDE : ∀ x, D (E x) = E (D x)) (x : A) :
    (a • D) ((b • E) x) = (b • E) ((a • D) x) := by
…

Mentions: OAI.AbhyankarSathaye.x

theorem OAI.AbhyankarSathaye.CommutingDerivations.scaleDerivation_kernel line 82
def OAI.AbhyankarSathaye.CommutingDerivations.descendDerivation line 88
Source documentation
A specified function whose image intertwines a derivation through an injective algebra map automatically satisfies all derivation laws.
```
def descendDerivation (ι : A →ₐ[K] B) (hι : Function.Injective ι)
    (D : Derivation K B B) (d : A → A) (hd : ∀ a, ι (d a) = D (ι a)) :
    Derivation K A A where
…
```
theorem OAI.AbhyankarSathaye.CommutingDerivations.descendDerivation_apply line 108
theorem OAI.AbhyankarSathaye.CommutingDerivations.descendDerivation_iterate line 112
theorem OAI.AbhyankarSathaye.CommutingDerivations.descendDerivation_locallyNilpotent line 122
theorem OAI.AbhyankarSathaye.CommutingDerivations.descendDerivation_commute line 130

theorem OAI.AbhyankarSathaye.CommutingDerivations.exists_descendDerivation line 140

Source documentation

Existence of descent from the precise closure obligation.

theorem exists_descendDerivation (ι : A →ₐ[K] B) (hι : Function.Injective ι)
    (D : Derivation K B B) (hstable : ∀ a : A, ∃ b : A, ι b = D (ι a)) :
    ∃ d : Derivation K A A, ∀ a, ι (d a) = D (ι a) := by
…