χ_pullback_obj_mk_truth_arrow — Mathlib

English

Hom equivalence homEquiv f equals the pullback of f along Ω₀ with respect to Ω.

Русский

Гом-эквиваленция homEquiv f равна вытягиванию вдоль f через Ω₀ по Ω.

LaTeX

$$$h.homEquiv f = (Subobject.pullback f).obj h.Ω_0$$$

Lean4

@[simp]
theorem χ_pullback_obj_mk_truth_arrow {X : C} (φ : X ⟶ 𝒞.Ω) :
    𝒞.χ ((Subobject.pullback φ).obj 𝒞.truth_as_subobject).arrow = φ :=
  by
  obtain ⟨Z, i, _, rfl⟩ := 𝒞.surjective_χ φ
  refine (𝒞.uniq _ (?_ : IsPullback _ (𝒞.χ₀ _) _ _)).symm
  refine
    (IsPullback.of_hasPullback 𝒞.truth (𝒞.χ i)).flip.of_iso (underlyingIso _).symm (Iso.refl _) (Iso.refl _)
      (Iso.refl _) ?_ (𝒞.isTerminalΩ₀.hom_ext _ _) (by simp) (by simp)
  dsimp
  rw [Iso.eq_inv_comp, comp_id, underlyingIso_hom_comp_eq_mk]
  rfl

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