exists_leftFraction₂ — Mathlib

English

Every RightFraction₂ admits a leftFraction₂ decomposition after localization.

Русский

Каждая RightFraction₂ имеет разложение на LeftFraction₂ после локализации.

LaTeX

$$$\\exists ψ : W.LeftFraction₂ X Y, φ.f ≫ ψ.s = φ.s ≫ ψ.f \\land φ.f' ≫ ψ.s = φ.s ≫ ψ.f'$$$

Lean4

theorem exists_leftFraction₂ [W.HasLeftCalculusOfFractions] :
    ∃ (ψ : W.LeftFraction₂ X Y), φ.f ≫ ψ.s = φ.s ≫ ψ.f ∧ φ.f' ≫ ψ.s = φ.s ≫ ψ.f' :=
  by
  obtain ⟨ψ₁, hψ₁⟩ := φ.fst.exists_leftFraction
  obtain ⟨ψ₂, hψ₂⟩ := φ.snd.exists_leftFraction
  obtain ⟨α, hα⟩ := (RightFraction.mk _ ψ₁.hs ψ₂.s).exists_leftFraction
  dsimp at hψ₁ hψ₂ hα
  refine ⟨LeftFraction₂.mk (ψ₁.f ≫ α.f) (ψ₂.f ≫ α.s) (ψ₂.s ≫ α.s) (W.comp_mem _ _ ψ₂.hs α.hs), ?_, ?_⟩
  · dsimp
    rw [hα, reassoc_of% hψ₁]
  · rw [reassoc_of% hψ₂]

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