English
If R and R₂ are commutative rings equipped with differential structures and are A-algebras, and h is an A-algebra isomorphism between R and R₂, then the differential algebra structure on R₂ can be transferred to R along h, yielding a differential algebra structure on R making h an isomorphism of differential algebras.
Русский
Если R и R₂ — коммутативные кольца с дифференциальной структурой и структурами A-алгебр, и есть изоморфизм A-алгебр h: R ≃ₐ[A] R₂, то структура дифференциальной алгебры на R₂ может быть перенесена на R по h, образуя структуру дифференциальной алгебры на R, превращающую h в изоморфизм дифференциальных алгебр.
LaTeX
$$$\text{There exists a differential } A\text{-algebra structure on } R \text{ such that } h: R \to R_2 \text{ is a differential-algebra isomorphism.}$$$
Lean4
/-- Transfer a `DifferentialAlgebra` instance across a `AlgEquiv`.
-/
theorem equiv {A : Type*} [CommRing A] [Differential A] {R R₂ : Type*} [CommRing R] [CommRing R₂] [Differential R₂]
[Algebra A R] [Algebra A R₂] [DifferentialAlgebra A R₂] (h : R ≃ₐ[A] R₂) :
letI := Differential.equiv h.toRingEquiv
DifferentialAlgebra A R :=
letI := Differential.equiv h.toRingEquiv
⟨fun a ↦ by
change (LinearMap.comp ..) _ = _
simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.toAddMonoidHom_eq_coe, RingEquiv.toRingHom_eq_coe,
AlgEquiv.toRingEquiv_toRingHom, LinearMap.coe_comp, AddMonoidHom.coe_toIntLinearMap, AddMonoidHom.coe_coe,
RingHom.coe_coe, Derivation.coeFn_coe, Function.comp_apply, AlgEquiv.commutes, deriv_algebraMap]
apply h.symm.commutes⟩
