Structures · Category theory
CategoryTheory.MorphismProperty.ContainsIdentities
Typeclass expressing that a morphism property contains identities.
- Shape
- One type argument · adds id_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances3
- AlgebraicGeometry.Scheme
- Prod
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by165
- CategoryTheory.MorphismProperty.id_mem
- AlgebraicGeometry.Scheme.coverOfIsIso
- CategoryTheory.MorphismProperty.LeftFraction.ofHom
- CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost
- CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp
- AlgebraicGeometry.IsZariskiLocalAtSource.of_isOpenImmersion
- CategoryTheory.MorphismProperty.RightFraction.ofHom
- CategoryTheory.MorphismProperty.of_isIso
- CategoryTheory.Localization.Monoidal.functorMonoidalOfComp
- AlgebraicGeometry.Scheme.Cover.pushforwardIso
- CategoryTheory.MorphismProperty.overEquivOfIsInitial
- CategoryTheory.Localization.lift₃NatTrans
- CategoryTheory.Localization.lift₂NatTrans
- CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁
- CategoryTheory.Span.id
- CategoryTheory.MorphismProperty.underEquivOfIsTerminal
- CategoryTheory.MorphismProperty.ContainsIdentities.id_mem
- CategoryTheory.Localization.lift₂NatIso
- CategoryTheory.Localization.associator
- CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app
- CategoryTheory.MorphismProperty.LeftFraction.map_ofHom
- CategoryTheory.MorphismProperty.Comma.id
- CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift
- AlgebraicGeometry.IsLocalIso.le_of_isZariskiLocalAtSource
- CategoryTheory.Localization.HasProductsOfShapeAux.adj
- CategoryTheory.Localization.lift₃NatIso
- CategoryTheory.Localization.lift₂
- CategoryTheory.Localization.lift₂NatTrans_app_app
- CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk'
- CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₂
- CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.isConnected
- CategoryTheory.Localization.HasProductsOfShapeAux.compLimitFunctorIso
- CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod
- CategoryTheory.Localization.HasProductsOfShapeAux.isLimitMapCone
- AlgebraicGeometry.Scheme.exists_hom_isAffine_of_isZariskiLocalAtSource
- CategoryTheory.Localization.lift₃NatTrans_app_app_app
- CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor
- CategoryTheory.MorphismProperty.RightFraction.map_ofHom
- CategoryTheory.Localization.preservesProductsOfShape
- CategoryTheory.MorphismProperty.isContinuous_comap_forget
- CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₁
- AlgebraicGeometry.Scheme.zariskiPrecoverage_le_propQCPrecoverage
- CategoryTheory.Localization.associator_hom_app_app_app
- CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε
- CategoryTheory.Localization.hasProductsOfShape
- CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ
- CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology
- AlgebraicGeometry.Scheme.coverOfIsIso_I₀
- CategoryTheory.MorphismProperty.Over.instCreatesLimitsOfShapeTopOverDiscretePEmptyForgetOfContainsIdentitiesOfRespectsIso
- CategoryTheory.Functor.IsLocalization.instDiscreteObjWhiskeringRightFunctorCategoryOfFiniteOfContainsIdentities
Ancestors0
No ancestors.