tensorCotangentSpace — Mathlib

English

Given a formal étale map P → Q of algebras, there is a canonical linear equivalence T ⊗_S P.Cotangent ≅ Q.Cotangent, relating cotangent spaces after base extension along the étale map. This extends the base-change philosophy to cotangent spaces.

Русский

При заданном формально этиальном отображении P → Q алгебр существует каноническое линейное эквивалентство T ⊗_S P.Cotangent ≅ Q.Cotangent, связывающее котангенентальные пространства после базового изменения по этиальному отображению.

LaTeX

$$$T \\otimes_S P.\\Cotangent \\cong_T Q.\\Cotangent$$$

Lean4

/-- If `P → Q` is formally étale, then `T ⊗ₛ (S ⊗ₚ Ω[P/R]) ≃ T ⊗_Q Ω[Q/R]`. -/
noncomputable def tensorCotangentSpace (H : f.toRingHom.FormallyEtale) :
    T ⊗[S] P.CotangentSpace ≃ₗ[T] Q.CotangentSpace :=
  letI := f.toRingHom.toAlgebra
  haveI : IsScalarTower R P.Ring Q.Ring := .of_algebraMap_eq fun r ↦ (f.toRingHom_algebraMap r).symm
  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 ↦ (f.algebraMap_toRingHom r).symm
  haveI : FormallyEtale P.Ring Q.Ring := ‹_›
  { __ := (CotangentSpace.map f).liftBaseChange T
    invFun :=
      LinearMap.liftBaseChange T
        (by
          refine LinearMap.liftBaseChange _ ?_ ∘ₗ (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring).symm.toLinearMap
          exact (TensorProduct.mk _ _ _ 1).restrictScalars P.Ring ∘ₗ (TensorProduct.mk _ _ _ 1).restrictScalars P.Ring)
    left_inv
      x := by
      change (LinearMap.liftBaseChange _ _ ∘ₗ LinearMap.liftBaseChange _ _) x = LinearMap.id (R := T) x
      congr 1
      ext : 4
      refine Derivation.liftKaehlerDifferential_unique (R := R) (S := P.Ring) (M := T ⊗[S] P.CotangentSpace) _ _ ?_
      ext a
      have : (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring).symm ((D R Q.Ring) (f.toRingHom a)) = 1 ⊗ₜ D _ _ a :=
        tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap R P.Ring Q.Ring a
      simp [this]
    right_inv
      x := by
      change (LinearMap.liftBaseChange _ _ ∘ₗ LinearMap.liftBaseChange _ _) x = LinearMap.id (R := T) x
      congr 1
      ext a
      dsimp
      obtain ⟨x, hx⟩ := (tensorKaehlerEquivOfFormallyEtale R P.Ring _).surjective (D R Q.Ring a)
      simp only [one_smul, ← hx, LinearEquiv.symm_apply_apply]
      change
        (((CotangentSpace.map f).liftBaseChange T).restrictScalars Q.Ring ∘ₗ LinearMap.liftBaseChange _ _) x =
          ((TensorProduct.mk _ _ _ 1) ∘ₗ (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring).toLinearMap) x
      congr 1
      ext a
      simp; rfl }

Похожие утверждения