English
There is an explicit equivalence between the H1Cotangent modules of two presentations P and P', given by the induced map map and its inverse, making the two H1Cotangent spaces canonically isomorphic.
Русский
Существует явное эквивалентное отображение между H1Cotangent модулей двух презентаций P и P', задаваемое отображением map и его обратным, образующее каноническое изоморождение пространств.
LaTeX
$$Equiv (P : Generators R S ι) (P' : Generators R S ι') : P.toExtension.H1Cotangent ≃ₗ[S] P'.toExtension.H1Cotangent$$
Lean4
/-- `H¹(L_{S/R})` is independent of the presentation chosen. -/
@[simps! apply]
noncomputable def equiv (P : Generators R S ι) (P' : Generators R S ι') :
P.toExtension.H1Cotangent ≃ₗ[S] P'.toExtension.H1Cotangent :=
Extension.H1Cotangent.equiv (Generators.defaultHom P P').toExtensionHom (Generators.defaultHom P' P).toExtensionHom
