English
The map of the identity morphism on P is the identity map on H1Cotangent: map(id P) = id.
Русский
Отображение для идентичности на P равно тождественному отображению на H1Cotangent: map(id P) = id.
LaTeX
$$$\\text{map}(.\\mathrm{id}\u200b P) = \\mathrm{LinearMap.id}$$$
Lean4
/-- Maps `P₁ → P₂` and `P₂ → P₁` between extensions
induce an isomorphism between `H¹(L_P₁)` and `H¹(L_P₂)`. -/
@[simps! apply]
noncomputable def equiv {P₁ P₂ : Extension R S} (f₁ : P₁.Hom P₂) (f₂ : P₂.Hom P₁) : P₁.H1Cotangent ≃ₗ[S] P₂.H1Cotangent
where
__ := map f₁
invFun := map f₂
left_inv
x :=
show (map f₂ ∘ₗ map f₁) x = LinearMap.id x by
rw [← Extension.H1Cotangent.map_id, eq_comm, map_eq _ (f₂.comp f₁), Extension.H1Cotangent.map_comp]; rfl
right_inv
x :=
show (map f₁ ∘ₗ map f₂) x = LinearMap.id x by
rw [← Extension.H1Cotangent.map_id, eq_comm, map_eq _ (f₁.comp f₂), Extension.H1Cotangent.map_comp]; rfl
