English
Each inclusion ι_i is a mono morphism in the glued category (i.e., left-cancellable).
Русский
Каждое вложение ι_i является монообразованием в слитом пространстве (левая отменяемость).
LaTeX
$$$\forall i, \text{Mono}(\iota_i)$$$
Lean4
theorem rel_equiv : Equivalence D.Rel :=
⟨fun x =>
⟨inv (D.f _ _) x.2, IsIso.inv_hom_id_apply (D.f x.fst x.fst) _,
-- Use `elementwise_of%` elaborator instead of `IsIso.inv_hom_id_apply` to work around
-- `ConcreteCategory`/`HasForget` mismatch:
by simp [elementwise_of% IsIso.inv_hom_id (D.f x.fst x.fst)]⟩,
by
rintro a b ⟨x, e₁, e₂⟩
exact ⟨D.t _ _ x, e₂, by rw [← e₁, D.t_inv_apply]⟩,
by
rintro ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ ⟨x, e₁, e₂⟩
rintro ⟨y, e₃, e₄⟩
let z := (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv ⟨⟨_, _⟩, e₂.trans e₃.symm⟩
have eq₁ : (D.t j i) ((pullback.fst _ _ : _ /-(D.f j k)-/ ⟶ D.V (j, i)) z) = x :=
by
dsimp only [coe_of, z]
rw [pullbackIsoProdSubtype_inv_fst_apply, D.t_inv_apply]
have eq₂ : (pullback.snd _ _ : _ ⟶ D.V _) z = y := pullbackIsoProdSubtype_inv_snd_apply _ _ _
clear_value z
use (pullback.fst _ _ : _ ⟶ D.V (i, k)) (D.t' _ _ _ z)
dsimp only at *
substs eq₁ eq₂ e₁ e₃ e₄
have h₁ : D.t' j i k ≫ pullback.fst _ _ ≫ D.f i k = pullback.fst _ _ ≫ D.t j i ≫ D.f i j := by rw [← 𝖣.t_fac_assoc];
congr 1; exact pullback.condition
have h₂ : D.t' j i k ≫ pullback.fst _ _ ≫ D.t i k ≫ D.f k i = pullback.snd _ _ ≫ D.t j k ≫ D.f k j :=
by
rw [← 𝖣.t_fac_assoc]
apply @Epi.left_cancellation _ _ _ _ (D.t' k j i)
rw [𝖣.cocycle_assoc, 𝖣.t_fac_assoc, 𝖣.t_inv_assoc]
exact pullback.condition.symm
exact ⟨CategoryTheory.congr_fun h₁ z, CategoryTheory.congr_fun h₂ z⟩⟩
