English
Under a localization M of S and with a base change along an étale map, the localized module structure transfers along the base-change functor, giving an IsLocalizedModule for the map that respects localization. This ensures that localization preserves the Kähler-based module structures in étale settings.
Русский
При локализации M алгебры S и базовом изменении вдоль этиального отображения, локализованная модульная структура переносится через отображатель локализации, образуя IsLocalizedModule для отображения, сохраняющего локализацию. Это гарантирует, что локализация сохраняет модули на базе Каэлера в условиях этиальности.
LaTeX
$$$\\text{IsLocalizedModule}~M\\ (\\text{map}_{R,R,S,T})$$$
Lean4
/-- If `J ≃ Q ⊗ₚ I` (e.g. when `T = Q ⊗ₚ S` and `P → Q` is flat), then `T ⊗ₛ I/I² ≃ J/J²`. -/
noncomputable def tensorCotangent [alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom)
(H : Function.Bijective ((f.mapKer halg).liftBaseChange Q.Ring)) : T ⊗[S] P.Cotangent ≃ₗ[T] Q.Cotangent :=
{ __ := (Cotangent.map f).liftBaseChange T
invFun := tensorCotangentInvFun f halg H
left_inv
x := by
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom]
induction x with
| zero => simp only [map_zero]
| add x y _ _ => simp only [map_add, *]
| tmul a b =>
obtain ⟨b, rfl⟩ := Cotangent.mk_surjective b
obtain ⟨a, rfl⟩ := Q.algebraMap_surjective a
simp only [LinearMap.liftBaseChange_tmul, Cotangent.map_mk, Hom.toAlgHom_apply, algebraMap_smul]
refine (tensorCotangentInvFun_smul_mk f halg H a b).trans ?_
simp [algebraMap_eq_smul_one, TensorProduct.smul_tmul']
right_inv
x := by
obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
obtain ⟨x, rfl⟩ := H.surjective x
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom]
induction x with
| zero => simp only [map_zero]
| add x y _ _ => simp only [map_add, *]
| tmul a b =>
simp only [LinearMap.liftBaseChange_tmul, map_smul]
simp [Hom.mapKer, tensorCotangentInvFun_smul_mk] }
