equivOfFormallySmooth_symm — Mathlib

English

If P1 and P2 are extensions of S over R and formally smooth, then the symmetry of the H1Cotangent equivalence holds, providing a canonical isomorphism between P1.H1Cotangent and P2.H1Cotangent in both directions.

Русский

Если P1 и P2 — расширения S над R и формально гладкие, то симметрия эквивалентности H1Cotangent обеспечивает каноническое изоморфизм между P1.H1Cotangent и P2.H1Cotangent в обоих направлениях.

LaTeX

$$P1.H1Cotangent ≃_S P2.H1Cotangent$$

Lean4

theorem equivOfFormallySmooth_symm (P₁ P₂ : Extension R S) [FormallySmooth R P₁.Ring] [FormallySmooth R P₂.Ring] :
    (equivOfFormallySmooth P₁ P₂).symm = equivOfFormallySmooth P₂ P₁ :=
  rfl

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