Theorems · Definition · category theory

CategoryTheory.Subobject.Classifier.ofIso

{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

Being a subobject classifier is preserved under isomorphism.

Defined in: Mathlib.CategoryTheory.Subobject.Classifier.Defs
Cited by: 5 results in Mathlib
Foundations: Depth 38 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
CategoryTheory.Iso.homstatement and proof · cited by 7,684
CategoryTheory.Iso.invstatement and proof · cited by 6,514
CategoryTheory.Isostatement and proof · cited by 3,963
CategoryTheory.Monoproof · cited by 893
CategoryTheory.Subobject.Classifierstatement and proof · cited by 46
CategoryTheory.Subobject.Classifier.Ωstatement and proof · cited by 33
CategoryTheory.Subobject.Classifier.Ω₀statement and proof · cited by 26
CategoryTheory.Subobject.Classifier.truthstatement and proof · cited by 19
CategoryTheory.Subobject.Classifier.χproof · cited by 17

Cited by6

Results whose statement or proof uses this declaration.

CategoryTheory.Subobject.Classifier.ofIso_Ωstatement and proof · cited by 0
CategoryTheory.Subobject.Classifier.ofIso_Ω₀statement and proof · cited by 0
CategoryTheory.Subobject.Classifier.ofIso_χstatement and proof · cited by 0
CategoryTheory.Subobject.Classifier.ofIso_χ₀statement and proof · cited by 0
CategoryTheory.Classifier.ofIsoproof · cited by 0
CategoryTheory.Subobject.Classifier.ofIso_truthstatement and proof · cited by 0