English
Two LeftFraction₂ elements are equal if and only if their mapped first and second components are equal after localization.
Русский
Два элемента LeftFraction₂ равны тогда и только тогда, когда их отображённые компоненты совпадают после локализации.
LaTeX
$$$\\text{map\_eq\_iff }(L,W) : (\\phi,\\psi) \\mapsto (\\phi.fst.map\,\\psi.fst, \\phi.snd.map\,\\psi.snd)$$$
Lean4
theorem map_eq_iff {X Y : C} (φ ψ : W.LeftFraction₂ X Y) :
(φ.fst.map L (Localization.inverts _ _) = ψ.fst.map L (Localization.inverts _ _) ∧
φ.snd.map L (Localization.inverts _ _) = ψ.snd.map L (Localization.inverts _ _)) ↔
LeftFraction₂Rel φ ψ :=
by
simp only [LeftFraction.map_eq_iff L W]
constructor
· intro ⟨h, h'⟩
obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h
obtain ⟨Z', t₁', t₂', hst', hft', ht'⟩ := h'
dsimp at t₁ t₂ t₁' t₂' hst hft hst' hft' ht ht'
have ⟨α, hα⟩ := (RightFraction.mk _ ht (φ.s ≫ t₁')).exists_leftFraction
simp only [Category.assoc] at hα
obtain ⟨Z'', u, hu, fac⟩ := HasLeftCalculusOfFractions.ext _ _ _ φ.hs hα
have hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u := by
rw [← reassoc_of% hst, ← reassoc_of% hα, ← reassoc_of% hst']
obtain ⟨Z''', u', hu', fac'⟩ := HasLeftCalculusOfFractions.ext _ _ _ ψ.hs hα'
simp only [Category.assoc] at fac fac'
refine ⟨Z''', t₁' ≫ α.s ≫ u ≫ u', t₂' ≫ α.s ≫ u ≫ u', ?_, ?_, ?_, ?_⟩
· rw [reassoc_of% hst']
· rw [reassoc_of% fac, reassoc_of% hft, fac']
· rw [reassoc_of% hft']
· rw [← Category.assoc]
exact W.comp_mem _ _ ht' (W.comp_mem _ _ α.hs (W.comp_mem _ _ hu hu'))
· intro h
exact ⟨h.fst, h.snd⟩
