English
For indices i,j, the preimage under ι_j of the range of ι_i equals the range of f j i.
Русский
Для индексов i,j предобраз диапазона ι_i через ι_j равен диапазону f j i.
LaTeX
$$$\iota_j^{-1}(\mathrm{range}(\iota_i)) = \mathrm{range}(D.f j i)$$$
Lean4
theorem ι_eq_iff_rel (i j : D.J) (x : D.U i) (y : D.U j) : 𝖣.ι i x = 𝖣.ι j y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩ :=
by
constructor
· delta GlueData.ι
simp_rw [← Multicoequalizer.ι_sigmaπ]
intro h
rw [← show _ = Sigma.mk i x from ConcreteCategory.congr_hom (sigmaIsoSigma.{_, u} D.U).inv_hom_id _]
rw [← show _ = Sigma.mk j y from ConcreteCategory.congr_hom (sigmaIsoSigma.{_, u} D.U).inv_hom_id _]
change InvImage D.Rel (sigmaIsoSigma.{_, u} D.U).hom _ _
rw [← (InvImage.equivalence _ _ D.rel_equiv).eqvGen_iff]
refine Relation.EqvGen.mono ?_ (D.eqvGen_of_π_eq h :)
rintro _ _ ⟨x⟩
obtain ⟨⟨⟨i, j⟩, y⟩, rfl⟩ := (ConcreteCategory.bijective_of_isIso (sigmaIsoSigma.{u, u} _).inv).2 x
unfold InvImage MultispanIndex.fstSigmaMap MultispanIndex.sndSigmaMap
rw [sigmaIsoSigma_inv_apply]
-- `rw [← ConcreteCategory.comp_apply]` succeeds but rewrites the wrong expression
erw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, colimit.ι_desc_assoc, ←
ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, colimit.ι_desc_assoc]
-- previous line now `erw` after https://github.com/leanprover-community/mathlib4/pull/13170
erw [sigmaIsoSigma_hom_ι_apply, sigmaIsoSigma_hom_ι_apply]
exact ⟨y, ⟨rfl, rfl⟩⟩
· rintro ⟨z, e₁, e₂⟩
dsimp only at *
-- Porting note: there were `subst e₁` and `subst e₂`, instead of the `rw`
rw [← e₁, ← e₂] at *
rw [D.glue_condition_apply]
