Theorems · Definition · category theory

CategoryTheory.Classifier.ofIso

Deprecated since 2026-03-06Use CategoryTheory.Subobject.Classifier.ofIso instead.

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (𝒞 : CategoryTheory.Subobject.Classifier C) →
      {Ω₀ Ω : C} →
        (eΩ : 𝒞.Ω ≅ Ω) →
          (eΩ₀ : 𝒞.Ω₀ ≅ Ω₀) →
            ((C_1 : C) → C_1 ⟶ Ω₀) →
              (t : Ω₀ ⟶ Ω) →
                autoParam
                    (t = CategoryTheory.CategoryStruct.comp eΩ₀.inv (CategoryTheory.CategoryStruct.comp 𝒞.truth eΩ.hom))
                    CategoryTheory.Subobject.Classifier.ofIso._auto_1 →
                  CategoryTheory.Subobject.Classifier C

Alias of CategoryTheory.Subobject.Classifier.ofIso. Being a subobject classifier is preserved under isomorphism.

Defined in

Mathlib.CategoryTheory.Subobject.Classifier.Defs

Cited by

0 results in Mathlib

Foundations

Depth 39 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category