English
If S ⊂ T is a localization and R → S is an algebra map, then the Kahler differential module map extends to a localized context preserving étale-like behavior; concretely, the localized Kahler differential map is isomorphic to the base-change of the Kahler differential map along the localization.
Русский
Если S ⊂ T является локализацией и R → S — алгебраическая карта, то отображение Каэлера дифференциалов продолжает существование в локализованном контексте и сохраняет подобное этиальному поведению; конкретно, локализованное отображение дифференциалов Каэлера изоморфно базовому изменению отображения дифференциалов Каэлера вдоль локализации.
LaTeX
$$$IsLocalizedModule\\ M (\\text{Kähler map})$$$
Lean4
/-- let `p` be a submonoid of an `R`-algebra `S`. Then `Sₚ ⊗ H¹(L_{S/R}) ≃ H¹(L_{Sₚ/R})`. -/
noncomputable def tensorH1CotangentOfIsLocalization (M : Submonoid S) [IsLocalization M T] :
T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T :=
by
letI P : Extension R S := (Generators.self R S).toExtension
letI M' := M.comap (algebraMap P.Ring S)
letI fQ : Localization M' →ₐ[R] T :=
IsLocalization.liftAlgHom (M := M') (f := (IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S))
(fun ⟨y, hy⟩ ↦ by simpa using IsLocalization.map_units T ⟨algebraMap P.Ring S y, hy⟩)
letI Q : Extension R T :=
.ofSurjective fQ
(by
intro x
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.mk'_surjective M x
obtain ⟨x, rfl⟩ := P.algebraMap_surjective x
obtain ⟨s, rfl⟩ := P.algebraMap_surjective s
refine ⟨IsLocalization.mk' _ x ⟨s, show s ∈ M' from hs⟩, ?_⟩
simp only [fQ, IsLocalization.coe_liftAlgHom, AlgHom.toRingHom_eq_coe]
rw [IsLocalization.lift_mk'_spec]
simp)
letI f : P.Hom Q :=
{ toRingHom := algebraMap P.Ring (Localization M')
toRingHom_algebraMap x := (IsScalarTower.algebraMap_apply R P.Ring (Localization M') _).symm
algebraMap_toRingHom x := @IsLocalization.lift_eq .. }
haveI : FormallySmooth R P.Ring := inferInstanceAs (FormallySmooth R (MvPolynomial _ _))
haveI : FormallySmooth P.Ring (Localization M') := .of_isLocalization M'
haveI : FormallySmooth R Q.Ring := .comp R P.Ring (Localization M')
haveI : Module.Flat S T := IsLocalization.flat T M
letI : Algebra P.Ring Q.Ring := inferInstanceAs (Algebra P.Ring (Localization M'))
letI := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
letI := fQ.toRingHom.toAlgebra
haveI : IsScalarTower P.Ring S T := .of_algebraMap_eq' rfl
haveI : IsScalarTower P.Ring (Localization M') T := .of_algebraMap_eq fun r ↦ (f.algebraMap_toRingHom r).symm
haveI : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap :=
by
rw [isLocalizedModule_iff_isLocalization]
convert ‹IsLocalization M T› using 1
exact Submonoid.map_comap_eq_of_surjective P.algebraMap_surjective _
refine Extension.tensorH1Cotangent f rfl ?_ ?_ ≪≫ₗ Extension.equivH1CotangentOfFormallySmooth _
· exact RingHom.formallyEtale_algebraMap.mpr (FormallyEtale.of_isLocalization (M := M') (Rₘ := Localization M'))
· let F : P.ker →ₗ[P.Ring] RingHom.ker fQ := f.mapKer rfl
refine (isLocalizedModule_iff_isBaseChange M' (Localization M') F).mp ?_
have :
(LinearMap.ker <| Algebra.linearMap P.Ring S).localized' (Localization M') M'
(Algebra.linearMap P.Ring (Localization M')) =
RingHom.ker fQ :=
by
rw [LinearMap.localized'_ker_eq_ker_localizedMap (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
(f' := (IsScalarTower.toAlgHom P.Ring S T).toLinearMap)]
ext x
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.mk'_surjective M' x
simp only [LinearMap.mem_ker, LinearMap.extendScalarsOfIsLocalization_apply', RingHom.mem_ker,
IsLocalization.coe_liftAlgHom, AlgHom.toRingHom_eq_coe, IsLocalization.lift_mk'_spec, RingHom.coe_coe,
AlgHom.coe_comp, IsScalarTower.coe_toAlgHom', Function.comp_apply, mul_zero, fQ]
have :
IsLocalization.mk' (Localization M') x ⟨s, hs⟩ =
IsLocalizedModule.mk' (Algebra.linearMap P.Ring (Localization M')) x ⟨s, hs⟩ :=
by
rw [IsLocalization.mk'_eq_iff_eq_mul, mul_comm, ← Algebra.smul_def, ← Submonoid.smul_def,
IsLocalizedModule.mk'_cancel']
rfl
simp [this, ← IsScalarTower.algebraMap_apply]
have :
F =
((LinearEquiv.ofEq _ _ this).restrictScalars P.Ring).toLinearMap ∘ₗ
P.ker.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) :=
by ext; rfl
rw [this]
exact IsLocalizedModule.of_linearEquiv _ _ _
