English
There is a canonical, finite-type linear isomorphism between the cotangent module of an ideal I in a commutative ring R and the cotangent ideal of I inside R; equivalently, I/I^2 can be identified with the corresponding ideal in R/I^2 via this isomorphism.
Русский
Существует каноническое линейное изоморфизм между котантентной модулей-I и котантентной идеалом I в кольце R; эквивалентно, I/I^2 можно естественным образом идентифицировать с соответствующим котантентным идеалом внутри R/I^2 через этот изоморфизм.
LaTeX
$$$I^{\mathrm{Cotangent}} \cong_R I^{\mathrm{cotangentIdeal}}$$$
Lean4
/-- The equivalence of the two definitions of `I / I ^ 2`, either as the quotient of `I` or the
ideal of `R / I ^ 2`. -/
noncomputable def cotangentEquivIdeal : I.Cotangent ≃ₗ[R] I.cotangentIdeal :=
by
refine
{
LinearMap.codRestrict (I.cotangentIdeal.restrictScalars R) I.cotangentToQuotientSquare fun x => by
rw [← range_cotangentToQuotientSquare]; exact LinearMap.mem_range_self _ _,
Equiv.ofBijective _ ⟨?_, ?_⟩ with }
· rintro x y e
replace e := congr_arg Subtype.val e
obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
obtain ⟨y, rfl⟩ := I.toCotangent_surjective y
rw [I.toCotangent_eq]
dsimp only [toCotangent_to_quotient_square, Submodule.mkQ_apply] at e
rwa [Submodule.Quotient.eq] at e
· rintro ⟨_, x, hx, rfl⟩
exact ⟨I.toCotangent ⟨x, hx⟩, Subtype.ext rfl⟩
