English
There is an equivalence between derivations and lifts consistent with the quotient identifications, i.e., the equivalence respects the quotient construction.
Русский
Существует эквивалентность между деривациями и лифтами, согласованными с идентификациями по факторкольцу.
LaTeX
$$$\text{Equiv } Derivation(R,A,I) \simeq \{ f : A \to_{R} B \mid (Ideal.Quotient.mk) \circ f = IsScalarTower.toAlgHom R A (HasQuotient.Quotient B I) \}$$$
Lean4
/-- Given a tower of algebras `R → A → B`, and a square-zero `I : Ideal B`,
there is a 1-1 correspondence between `R`-derivations from `A` to `I` and
lifts `A →ₐ[R] B` of the canonical map `A →ₐ[R] B ⧸ I`. -/
@[simps!]
def derivationToSquareZeroEquivLift [IsScalarTower R A B] :
Derivation R A I ≃ { f : A →ₐ[R] B // (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I) } :=
by
refine
⟨fun d => ⟨liftOfDerivationToSquareZero I hI d, ?_⟩, fun f => (derivationToSquareZeroOfLift I hI f.1 f.2 :), ?_, ?_⟩
· ext x; exact liftOfDerivationToSquareZero_mk_apply I hI d x
· intro d; ext x; exact add_sub_cancel_right (d x : B) (algebraMap A B x)
· rintro ⟨f, hf⟩; ext x; exact sub_add_cancel (f x) (algebraMap A B x)
