eq_liftCycles_homologyπ_up_to_refinements

English

There exists A', π, epi, z, hz with γ factoring through liftCycles and homology map as in the previous statement, under a refined setting.

Русский

Существуют A', π, epi, z, hz такие, что γ факторизуется через liftCycles и гомология отображения в уточненном виде.

LaTeX

$$$\\exists A',\\pi:A'\\to A\\; (\\pi\\ epi)\\; (z:A'\\to S.X_2),\\; hz: z\\, S.g = 0,\\; \\pi\\, \\gamma = S.liftCycles z hz \\; S.homologyπ$$$

Lean4

theorem eq_liftCycles_homologyπ_up_to_refinements {A : C} (γ : A ⟶ S.homology) :
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ S.X₂) (hz : z ≫ S.g = 0), π ≫ γ = S.liftCycles z hz ≫ S.homologyπ :=
  by
  obtain ⟨A', π, hπ, z, hz⟩ := surjective_up_to_refinements_of_epi S.homologyπ γ
  refine ⟨A', π, hπ, z ≫ S.iCycles, by simp, ?_⟩
  rw [hz]
  congr 1
  rw [← cancel_mono S.iCycles, liftCycles_i]

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