Centrality and inner derivations

This file contains the noncommutative derivation facts used by the algebraic-analysis stages. Mathlib's Derivation is specialized to commutative coefficient rings, so the Leibniz and innerness predicates are recorded directly for additive maps on arbitrary rings.

The fraction-presentation lemma is deliberately stated with all hypotheses visible. It does not assert that a particular localization has those properties.

def AlgebraicAnalysis.NoncommutativeDerivation.IsDerivation {E : Type u_1} [Ring E] (d : E →+ E) : Prop

Leibniz rule for an additive derivation of a possibly noncommutative ring.

Equations

• AlgebraicAnalysis.NoncommutativeDerivation.IsDerivation d = ∀ (a b : E), d (a * b) = a * d b + d a * b

def AlgebraicAnalysis.NoncommutativeDerivation.IsInnerDerivation {E : Type u_1} [Ring E] (d : E →+ E) : Prop

An additive derivation is inner when it is a commutator with one element.

Equations

• AlgebraicAnalysis.NoncommutativeDerivation.IsInnerDerivation d = ∃ (e : E), ∀ (y : E), d y = e * y - y * e

theorem AlgebraicAnalysis.NoncommutativeDerivation.not_isInnerDerivation_of_central {E : Type u_1} [Ring E] [Nontrivial E] (d : E →+ E) (x : E) (hxcentral : ∀ (y : E), x * y = y * x) (hdx : d x = 1) : ¬IsInnerDerivation d

theorem AlgebraicAnalysis.NoncommutativeDerivation.commute_of_mem_subring_closure {E : Type u_1} [Ring E] (x : E) (G : Set E) (hG : ∀ g ∈ G, Commute x g) (y : E) : y ∈ Subring.closure G → Commute x y

Commutation with a set propagates through the subring it generates.

theorem AlgebraicAnalysis.NoncommutativeDerivation.commute_map_of_right_fraction_representation {E : Type u_1} [Ring E] {R : Type u_2} [Ring R] (ι : R →+* E) (x : R) (hcentral : ∀ (y : R), Commute x y) (hunit : ∀ (s : R), IsUnit (ι s)) (hrep : ∀ (z : E), ∃ (c : R) (s : R), z * ι s = ι c) (z : E) : Commute (ι x) z

A central element of a source ring remains central in a target ring when every target element has a right-fraction presentation and every denominator maps to a unit. No commutativity of either ring is assumed.

theorem AlgebraicAnalysis.NoncommutativeDerivation.not_inner_of_central_coordinate {E : Type u_1} [Ring E] [Nontrivial E] (d : E →+ E) (_hd : IsDerivation d) (x : E) (hxcentral : ∀ (y : E), Commute x y) (hdx : d x = 1) : ¬IsInnerDerivation d

A derivation that sends a central coordinate to 1 cannot be inner. This is the form consumed by differential-Ore stage arguments.