H1AddEquivOfIsTrivial — Mathlib

English

If A is trivial, there is a group additive equivalence H1 A ≃+ (Abelianization G) ⊗ℤ A.

Русский

Если A тривиально, существует групповая аддитивная эквивалентность H1 A ≃+ (Abelianization G) ⊗ℤ A.

LaTeX

$$def H1AddEquivOfIsTrivial : H1 A ≃+ (Additive <| Abelianization G) ⊗[ℤ] A$$

Lean4

/-- If a `G`-representation on `A` is trivial, this is the group isomorphism between
`H₁(G, A) ≃+ Gᵃᵇ ⊗[ℤ] A` defined by `⟦single g a⟧ ↦ ⟦g⟧ ⊗ a`. -/
@[simps! -isSimp]
def H1AddEquivOfIsTrivial : H1 A ≃+ (Additive <| Abelianization G) ⊗[ℤ] A :=
  LinearEquiv.toAddEquiv <|
    LinearEquiv.ofLinear (H1ToTensorOfIsTrivial A) (lift <| mkH1OfIsTrivial A)
      (ext <|
        LinearMap.toAddMonoidHom_injective <| by
          ext g a
          simp [TensorProduct.mk_apply, TensorProduct.lift.tmul, mkH1OfIsTrivial_apply,
            H1ToTensorOfIsTrivial_H1π_single g a])
      (LinearMap.toAddMonoidHom_injective <|
        (H1Iso A).symm.toLinearEquiv.toAddEquiv.comp_left_injective <|
          QuotientAddGroup.addMonoidHom_ext _ <|
            (cycles₁IsoOfIsTrivial A).symm.toLinearEquiv.toAddEquiv.comp_left_injective <|
              by
              ext
              simp only [H1ToTensorOfIsTrivial, Iso.toLinearEquiv, AddMonoidHom.coe_comp, LinearMap.toAddMonoidHom_coe,
                LinearMap.coe_comp, AddMonoidHom.coe_toIntLinearMap]
              change TensorProduct.lift _ (QuotientAddGroup.lift _ _ _ ((H1Iso A).hom _)) = _
              simpa [AddSubgroup.subtype, cycles₁IsoOfIsTrivial_inv_apply (A := A), -π_comp_H1Iso_inv_apply] using
                (π_comp_H1Iso_inv_apply A _).symm)

Похожие утверждения