End_equiv_aux — Mathlib

English

Let R and S be commutative rings with S an R-algebra. For a given algebra homomorphism f: S → S ⊗_R S modulo the square of the Kaehler cotangent ideal, the following two conditions are equivalent: (i) the natural quotient map composed with f equals the canonical base-algebra homomorphism IsScalarTower.toAlgHom, and (ii) the lifted left-multiplication map on tensors, composed with f, is the identity on S.

Русский

Пусть R и S — коммутативные кольца, причём S является R-алгеброй. Для произвольного алгебраического гомоморфизма f: S → S ⊗_R S/KaehlerDifferential.ideal^2 имеется эквивалентность: (i) композиция образа через котангентальный идеал с f равна базовому гомоморфизму IsScalarTower.toAlgHom, и (ii) соответствующее отображение, получаемое из левой операции умножения в тензорном виде и затем подействующее через f, является тождественным по отношению к R-S.

LaTeX

$$$\left(\mathrm{Ideal.Quotient.mk}_{R} (\mathrm{KaehlerDifferential}.ideal R S).cotangentIdeal\right).comp f = \mathrm{IsScalarTower.toAlgHom} R S _ \iff \left( (\mathrm{TensorProduct.lmul'} R) : S \otimes[ R ] S \to_{\!R} S \right).kerSquareLift.comp f = \mathrm{AlgHom.id} R S$$$

Lean4

theorem End_equiv_aux (f : S →ₐ[R] S ⊗ S ⧸ KaehlerDifferential.ideal R S ^ 2) :
    (Ideal.Quotient.mkₐ R (KaehlerDifferential.ideal R S).cotangentIdeal).comp f = IsScalarTower.toAlgHom R S _ ↔
      (TensorProduct.lmul' R : S ⊗[R] S →ₐ[R] S).kerSquareLift.comp f = AlgHom.id R S :=
  by
  rw [AlgHom.ext_iff, AlgHom.ext_iff]
  apply forall_congr'
  intro x
  have e₁ :
    (TensorProduct.lmul' R : S ⊗[R] S →ₐ[R] S).kerSquareLift (f x) =
      KaehlerDifferential.quotientCotangentIdealRingEquiv R S
        (Ideal.Quotient.mk (KaehlerDifferential.ideal R S).cotangentIdeal <| f x) :=
    by generalize f x = y; obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y; rfl
  have e₂ : x = KaehlerDifferential.quotientCotangentIdealRingEquiv R S (IsScalarTower.toAlgHom R S _ x) :=
    (mul_one x).symm
  constructor
  · intro e
    exact
      (e₁.trans
            (@RingEquiv.congr_arg _ _ _ _ _ _ (KaehlerDifferential.quotientCotangentIdealRingEquiv R S) _ _ e)).trans
        e₂.symm
  · intro e; apply (KaehlerDifferential.quotientCotangentIdealRingEquiv R S).injective
    exact
      e₁.symm.trans
        (e.trans e₂)
          /- Note: Lean is slow to synthesize these instances (times out).
            Without them the endEquivDerivation' and endEquivAuxEquiv both have significant timeouts.
            In Mathlib 3, it was slow but not this slow. -/

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