Theorems · Theorem · category theory

CategoryTheory.HasSubobjectClassifier.comm

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasSubobjectClassifier C] {U X : C}
  (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m],
  CategoryTheory.CategoryStruct.comp m (CategoryTheory.HasSubobjectClassifier.χ m) =
    CategoryTheory.CategoryStruct.comp (⋯.some.χ₀ U) (CategoryTheory.HasSubobjectClassifier.truth C)

The diagram `` U m -> X | | χ₀ U χ m | | v v Ω₀ truth --> Ω `` commutes.

Defined in

Mathlib.CategoryTheory.Subobject.Classifier.Defs

Cited by

2 results in Mathlib

Foundations

Depth 6 from the axioms · uses Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.HasSubobjectClassifierCategoryTheory.Mono