Lean4
/-- The map `KaehlerDifferential f ⟶ (ModuleCat.restrictScalars g').obj (KaehlerDifferential f')`
induced by a commutative square (given by an equality `g ≫ f' = f ≫ g'`)
in the category `CommRingCat`. -/
noncomputable def map : KaehlerDifferential f ⟶ (ModuleCat.restrictScalars g'.hom).obj (KaehlerDifferential f') :=
letI := f.hom.toAlgebra
letI := f'.hom.toAlgebra
letI := g.hom.toAlgebra
letI := g'.hom.toAlgebra
letI := (g ≫ f').hom.toAlgebra
have : IsScalarTower A A' B' := IsScalarTower.of_algebraMap_eq' rfl
have :=
IsScalarTower.of_algebraMap_eq'
(congrArg Hom.hom fac)
-- TODO: after https://github.com/leanprover-community/mathlib4/pull/19511 we need to hint `(Y := ...)`.
-- This suggests `restrictScalars` needs to be redesigned.
ModuleCat.ofHom (Y := (ModuleCat.restrictScalars g'.hom).obj (KaehlerDifferential f'))
{ toFun := fun x ↦ _root_.KaehlerDifferential.map A A' B B' x
map_add' := by simp
map_smul' := by simp }
