English
The symmetry of the base-change isomorphism for Kahler differentials is compatible with change of scalars, yielding a canonical equality between the two ways to view the base change map. This ensures coherence of the base-change operation with scalar restriction.
Русский
Симметрия базового изменения для дифференциалов Каэлера согласуется с ограничением скаляров, образуя каноническое равенство между двумя способами представления отображения базового изменения. Это обеспечивает когерентность базового изменения с ограничением скаляров.
LaTeX
$$$\\ KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale\\_congr_simp$$$
Lean4
/-- (Implementation)
If `J ≃ Q ⊗ₚ I` (e.g. when `T = Q ⊗ₚ S` and `P → Q` is flat), then `T ⊗ₛ I/I² ≃ J/J²`.
This is the inverse. -/
noncomputable def tensorCotangentInvFun [alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom)
(H : Function.Bijective ((f.mapKer halg).liftBaseChange Q.Ring)) : Q.Cotangent →+ T ⊗[S] P.Cotangent :=
letI := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
haveI : IsScalarTower P.Ring S T := .of_algebraMap_eq' rfl
haveI : IsScalarTower P.Ring Q.Ring T := .of_algebraMap_eq fun r ↦ halg ▸ (f.algebraMap_toRingHom r).symm
letI e := LinearEquiv.ofBijective _ H
letI f' : Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
(LinearMap.liftBaseChange _ ((TensorProduct.mk _ _ _ 1).restrictScalars _ ∘ₗ Cotangent.mk)) ∘ₗ e.symm.toLinearMap
QuotientAddGroup.lift _ f' <| by
intro x hx
refine Submodule.smul_induction_on hx ?_ fun _ _ ↦ add_mem
clear x hx
rintro a ha b -
obtain ⟨x, hx⟩ := e.surjective ⟨a, ha⟩
obtain rfl : (e x).1 = a := congr_arg Subtype.val hx
obtain ⟨y, rfl⟩ := e.surjective b
simp only [AddMonoidHom.mem_ker, AddMonoidHom.coe_coe, map_smul, LinearMap.coe_comp, LinearEquiv.coe_coe,
Function.comp_apply, LinearEquiv.symm_apply_apply, f']
clear hx ha
induction x with
| zero => simp only [LinearEquiv.map_zero, ZeroMemClass.coe_zero, zero_smul]
| add x y _ _ => simp only [LinearEquiv.map_add, Submodule.coe_add, add_smul, zero_add, *]
| tmul a b =>
induction y with
| zero => simp only [LinearMap.map_zero, smul_zero]
| add x y hx hy => simp only [LinearMap.map_add, smul_add, hx, hy, zero_add]
| tmul c
d =>
simp only [LinearMap.liftBaseChange_tmul, LinearMap.coe_comp, SetLike.val_smul, LinearMap.coe_restrictScalars,
Function.comp_apply, mk_apply, smul_eq_mul, e, LinearMap.liftBaseChange_tmul, LinearEquiv.ofBijective_apply]
have h₂ : b.1 • Cotangent.mk d = 0 := by ext; simp [Cotangent.smul_eq_zero_of_mem _ b.2]
rw [TensorProduct.smul_tmul', mul_smul, f.mapKer_apply_coe, ← halg, algebraMap_smul, ← TensorProduct.tmul_smul,
h₂, tmul_zero, smul_zero]
