English
The inverse of the cotangent equivalence sends a class represented by x modulo I^2 back to the cotangent element corresponding to x in I.
Русский
Обратное котантгентовому эквивалентному отображению отображает класс, заданный x по модулю I^2, в соответствующий котантентный элемент в I.
LaTeX
$$I.cotangentEquivIdeal.symm( ⟨(I^2).mkQ x, proof⟩ ) = I.toCotangent( ⟨x, hx⟩ )$$
Lean4
theorem cotangentEquivIdeal_symm_apply (x : R) (hx : x ∈ I) :
-- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specify `(R₂ := R)` because `I.toCotangent` suggested `R ⧸ I^2` instead
I.cotangentEquivIdeal.symm
⟨(I ^ 2).mkQ x,
-- timeout (200000 heartbeats) without `by exact`
by exact Submodule.mem_map_of_mem (F := R →ₗ[R] R ⧸ I ^ 2) (f := (I ^ 2).mkQ) hx⟩ =
I.toCotangent (R := R) ⟨x, hx⟩ :=
by
apply I.cotangentEquivIdeal.injective
rw [I.cotangentEquivIdeal.apply_symm_apply]
ext
rfl
