English
The symmetry of the infinitesimal map is: the symm of the bijection established between H1Cotangent maps also yields a bijection in the opposite order, reflecting the equivalence of the two directions of transport along a formally smooth extension.
Русский
Симметрия биекции инфинитезимального отображения: симметричная пара линеек отображений между H1Cotangent обеспечивает биекция в обратном порядке, отражая эквивалентность двух направлений переноса вдоль формально гладкого расширения.
LaTeX
$$(equivOfFormallySmooth P₁ P₂).symm = equivOfFormallySmooth P₂ P₁$$
Lean4
theorem map_toInfinitesimal_bijective (P : Extension.{u} R S) : Function.Bijective (Cotangent.map P.toInfinitesimal) :=
by
constructor
· rw [injective_iff_map_eq_zero]
intro x hx
obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
have hx : x.1 ∈ P.ker ^ 2 := by
apply_fun Cotangent.val at hx
simp only [map_mk, Hom.toAlgHom_apply, val_mk, val_zero, Ideal.toCotangent_eq_zero,
Extension.ker_infinitesimal] at hx
rw [Ideal.cotangentIdeal_square] at hx
simpa only [toInfinitesimal, Ideal.mem_bot, infinitesimal, Ideal.Quotient.eq_zero_iff_mem] using hx
ext
simpa [Ideal.toCotangent_eq_zero]
· intro x
obtain ⟨⟨x, hx⟩, rfl⟩ := Cotangent.mk_surjective x
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
rw [ker_infinitesimal, Ideal.mk_mem_cotangentIdeal] at hx
exact ⟨.mk ⟨x, hx⟩, rfl⟩
