equivOfFormallySmooth_apply — Mathlib

English

The symmetry property of the equivalence between two formal smooth extensions: the inverse of the equivalence equals the equivalence in the reverse order.

Русский

Симметрия эквивалентности между двумя формально гладкими расширениями: обратная эквивалентность равна эквивалентности в обратном порядке.

LaTeX

$$(equivOfFormallySmooth P1 P2).symm = equivOfFormallySmooth P2 P1$$

Lean4

theorem equivOfFormallySmooth_apply {P₁ P₂ : Extension R S} (f : P₁.Hom P₂) [FormallySmooth R P₁.Ring]
    [FormallySmooth R P₂.Ring] (x) : H1Cotangent.equivOfFormallySmooth P₁ P₂ x = map f x := by
  rw [← equivOfFormallySmooth_toLinearMap]; rfl

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