Structures · Category theory
CategoryTheory.CatCommSq
CatCommSq T L R B expresses that there is a 2-commutative square of functors, where
the functors T, L, R and B are respectively the left, top, right and bottom functors
of the square.
- Defined in
- Mathlib.CategoryTheory.CatCommSq
- Shape
- 4 explicit arguments · adds iso
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- CategoryTheory.Functor
- CategoryTheory.Arrow
- CategoryTheory.Pretriangulated.Triangle
- CategoryTheory.Limits.CategoricalPullback
- CategoryTheory.Limits.CategoricalPullback.CatCommSqOver
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by30
- CategoryTheory.CatCommSq.iso
- CategoryTheory.CatCommSq.iso_inv_naturality
- CategoryTheory.LocalizerMorphism.fullyFaithful
- CategoryTheory.CatCommSq.vComp
- CategoryTheory.LocalizerMorphism.isEquivalence_iff
- CategoryTheory.Adjunction.localization
- CategoryTheory.CatCommSq.iso_hom_naturality
- CategoryTheory.CatCommSq.hComp
- CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk'
- CategoryTheory.LocalizerMorphism.isEquivalence_imp
- CategoryTheory.Adjunction.Localization.η_app
- CategoryTheory.Adjunction.Localization.ε
- CategoryTheory.LocalizerMorphism.nonempty_fullyFaithful_iff
- CategoryTheory.CatCommSq.hComp_iso_hom_app
- CategoryTheory.CatCommSq.vComp_iso_inv_app
- CategoryTheory.Adjunction.localization_counit_app
- CategoryTheory.Adjunction.Localization.η
- CategoryTheory.Adjunction.Localization.ε_app
- CategoryTheory.CatCommSq.hComp_iso_inv_app
- CategoryTheory.LocalizerMorphism.full
- CategoryTheory.Adjunction.localization_unit_app
- CategoryTheory.LocalizerMorphism.faithful
- CategoryTheory.Arrow.catCommSq
- CategoryTheory.Arrow.catCommSq_iso
- CategoryTheory.Functor.IsLocalization.of_equivalences
- CategoryTheory.CatCommSq.iso_inv_naturality_assoc
- CategoryTheory.CatCommSq.iso_hom_naturality_assoc
- CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful.mk'
- CategoryTheory.CatCommSq.vComp_iso_hom_app
- CategoryTheory.LocalizerMorphism.isEquivalence
Ancestors0
No ancestors.