classifier — Mathlib

Lean4
/-- Any representation `Ω` of `Subobject.presheaf C` gives a subobject classifier with truth values
object `Ω`. -/
noncomputable def classifier : Classifier C where
  Ω₀ := ⊤_ C
  Ω := Ω
  truth := h.isoΩ₀.inv ≫ h.Ω₀.arrow
  mono_truth := terminalIsTerminal.mono_from _
  χ₀ := terminalIsTerminal.from
  χ m _ := h.χ m
  isPullback m
    _ :=
    (h.isPullback m).of_iso (Iso.refl _) (Iso.refl _) h.isoΩ₀ (Iso.refl _) (by simp) (Subsingleton.elim _ _) (by simp)
      (by simp)
  uniq {U X} m _ χ₀ χ'
    sq :=
    by
    have : IsPullback m (h.χ₀ U) χ' h.Ω₀.arrow :=
      sq.of_iso (Iso.refl _) (Iso.refl _) (h.isoΩ₀.symm) (Iso.refl _) (by simp) (h.isTerminalΩ₀.hom_ext _ _) (by simp)
        (by simp)
    exact h.uniq this
Похожие утверждения