isRepresentable_hasClassifier_iff

English

A category has a subobject classifier iff the subobjects presheaf is representable.

Русский

Категория имеет классификатор подмножеств тогда и только тогда, когда подмножества-представитель представим.

LaTeX

$$HasClassifier C ↔ (Subobject.presheaf C).IsRepresentable$$

Lean4

/-- A category has a subobject classifier if and only if the subobjects functor is representable. -/
theorem isRepresentable_hasClassifier_iff [HasPullbacks C] : HasClassifier C ↔ (Subobject.presheaf C).IsRepresentable :=
  by
  constructor <;> intro h
  · obtain ⟨⟨𝒞⟩⟩ := h
    apply RepresentableBy.isRepresentable
    exact 𝒞.representableBy
  · obtain ⟨Ω, ⟨h⟩⟩ := h
    constructor; constructor
    exact Classifier.SubobjectRepresentableBy.classifier h

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