English
If P1 and P2 are extensions over S, both formally smooth over R, then there is a linear equivalence between P1.H1Cotangent and P2.H1Cotangent as S-modules, given by the composition of the corresponding equivalences arising from the formality of the extensions.
Русский
Если P1 и P2 — расширения над S, оба формально гладкие над R, тогда существует линейное эквивалентное отображение между P1.H1Cotangent и P2.H1Cotangent как модули над S, задаваемое композициями эквивалентностей, возникающих из формальности расширений.
LaTeX
$$P1.H1Cotangent ≃_S P2.H1Cotangent$$
Lean4
theorem map_toInfinitesimal_bijective (P : Extension.{u} R S) :
Function.Bijective (H1Cotangent.map P.toInfinitesimal) :=
by
constructor
· intro x y e
ext1
exact (Cotangent.map_toInfinitesimal_bijective P).1 (congr_arg Subtype.val e)
· intro ⟨x, hx⟩
obtain ⟨x, rfl⟩ := (Cotangent.map_toInfinitesimal_bijective P).2 x
refine ⟨⟨x, ?_⟩, rfl⟩
simpa [← CotangentSpace.map_cotangentComplex,
map_eq_zero_iff _ (CotangentSpace.map_toInfinitesimal_bijective P).injective] using hx
