English
Isomorphic algebras S ≅ S' induce isomorphic H1Cotangent spaces H1Cotangent R S ≃ H1Cotangent R S'.
Русский
Изоморфизмы алгебра S ≅ S' порождают изоморфизмы пространств H1Cotangent: H1Cotangent R S ≃ H1Cotangent R S'.
LaTeX
$$Equiv R S S' : H1Cotangent R S ≃ₗ[S] H1Cotangent R S'$$
Lean4
/-- Isomorphic algebras induce isomorphic `H¹(L_{S/R})`. -/
noncomputable def mapEquiv (e : S ≃ₐ[R] S') : H1Cotangent R S ≃ₗ[R] H1Cotangent R S' :=
-- we are constructing data, so we do not use `algebraize`
letI := e.toRingHom.toAlgebra
letI := e.symm.toRingHom.toAlgebra
have : IsScalarTower R S S' := .of_algebraMap_eq' e.toAlgHom.comp_algebraMap.symm
have : IsScalarTower R S' S := .of_algebraMap_eq' e.symm.toAlgHom.comp_algebraMap.symm
have : IsScalarTower S S' S := .of_algebraMap_eq fun _ ↦ (e.symm_apply_apply _).symm
have : IsScalarTower S' S S' := .of_algebraMap_eq fun _ ↦ (e.apply_symm_apply _).symm
{ toFun := map R R S S'
invFun := map R R S' S
left_inv
x := by
change ((map R R S' S).restrictScalars S ∘ₗ map R R S S') x = x
rw [map, map, ← Extension.H1Cotangent.map_comp, Extension.H1Cotangent.map_eq, Extension.H1Cotangent.map_id,
LinearMap.id_apply]
right_inv
x := by
change ((map R R S S').restrictScalars S' ∘ₗ map R R S' S) x = x
rw [map, map, ← Extension.H1Cotangent.map_comp, Extension.H1Cotangent.map_eq, Extension.H1Cotangent.map_id,
LinearMap.id_apply]
map_add' := LinearMap.map_add (map R R S S')
map_smul' := LinearMap.CompatibleSMul.map_smul (map R R S S') }
