tensorKaehlerEquiv — Mathlib

English

There is a canonical S-linear isomorphism between S ⊗_R Ω_{A/R} and Ω_{B/S} when B is the pushout of R,S,A,B.

Русский

Существует каноническое S-линейное изоморфизм между S ⊗_R Ω_{A/R} и Ω_{B/S} при пуш-ауте B как S ⊗_R A.

LaTeX

$$$(S \\otimes_R \\Omega_{A/R}) \\cong_S \\Omega_{B/S}$$$

Lean4

/-- The canonical isomorphism `(S ⊗[R] Ω[A⁄R]) ≃ₗ[S] Ω[B⁄S]` for `B = S ⊗[R] A`. -/
@[simps! symm_apply]
noncomputable def tensorKaehlerEquiv [h : Algebra.IsPushout R S A B] : (S ⊗[R] Ω[A⁄R]) ≃ₗ[S] Ω[B⁄S]
    where
  __ := ((map R S A B).restrictScalars R).liftBaseChange S
  invFun := (derivationTensorProduct R S A B).liftKaehlerDifferential
  left_inv := LinearMap.congr_fun (tensorKaehlerEquiv_left_inv R S A B)
  right_inv
    x := by
    obtain ⟨x, rfl⟩ := tensorProductTo_surjective _ _ x
    dsimp
    induction x with
    | zero => simp
    | add x y e₁ e₂ => simp only [map_add, e₁, e₂]
    | tmul x y =>
      dsimp
      simp only [Derivation.tensorProductTo_tmul, LinearMap.map_smul, Derivation.liftKaehlerDifferential_comp_D,
        map_liftBaseChange_smul]
      induction y using h.1.inductionOn
      · simp only [map_zero, smul_zero]
      ·
        simp only [AlgHom.toLinearMap_apply, IsScalarTower.coe_toAlgHom', derivationTensorProduct_algebraMap,
          LinearMap.liftBaseChange_tmul, LinearMap.coe_restrictScalars, map_D, one_smul]
      · simp only [Derivation.map_smul, LinearMap.map_smul, *, smul_comm x]
      · simp only [map_add, smul_add, *]

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