mkH1OfIsTrivial — Mathlib

English

For trivial A, π A 0 ≫ (H0IsoOfIsTrivial A).hom = (cyclesIso₀ A).hom.

Русский

Для тривиального A: композиция π_A0 с (H0IsoOfIsTrivial A).hom равна (cyclesIso₀ A).hom.

LaTeX

$$$\\pi A 0 \\;\\circ\\; (H0IsoOfIsTrivial A).hom = (cyclesIso_0 A).hom$$$

Lean4

/-- If a `G`-representation on `A` is trivial, this is the natural map `Gᵃᵇ → A → H₁(G, A)`
sending `⟦g⟧, a` to `⟦single g a⟧`. -/
def mkH1OfIsTrivial : Additive (Abelianization G) →ₗ[ℤ] A →ₗ[ℤ] H1 A :=
  AddMonoidHom.toIntLinearMap <|
    AddMonoidHom.toMultiplicativeRight.symm <|
      Abelianization.lift
        { toFun
            g :=
            Multiplicative.ofAdd
              (AddMonoidHom.toIntLinearMap
                (AddMonoidHomClass.toAddMonoidHom ((H1π A).hom ∘ₗ (cycles₁IsoOfIsTrivial A).inv.hom ∘ₗ lsingle g)))
          map_one' :=
            Multiplicative.toAdd.injective <|
              LinearMap.ext fun _ => (H1π_eq_zero_iff _).2 <| single_one_mem_boundaries₁ _
          map_mul' g
            h :=
            Multiplicative.toAdd.injective <|
              LinearMap.ext fun a => by
                simpa [← map_add] using
                  ((H1π_eq_iff _ _).2
                      ⟨single (g, h) a, by
                        simp [cycles₁IsoOfIsTrivial, sub_add_eq_add_sub, add_comm (single h a),
                          d₂₁_single (A := A)]⟩).symm }

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