Composition

📁 Source: Mathlib/CategoryTheory/MorphismProperty/Composition.lean

Statistics

Metric	Count
Definitions ContainsIdentities, HasOfPostcompProperty, HasOfPrecompProperty, HasTwoOutOfThreeProperty, IsMultiplicative, IsStableUnderComposition, StableUnderInverse, multiplicativeClosure, multiplicativeClosure', naturalityProperty	10
Theorems eqToHom, id_mem, inf, inverseImage, of_op, of_unop, op, unop, of_le, of_postcomp, of_le, of_precomp, toHasOfPostcompProperty, toHasOfPrecompProperty, toIsStableUnderComposition, inf, instEpimorphisms, instInverseImage, instIsomorphisms, instMonomorphisms, instTop, naturalityProperty, of_op, of_unop, op, toContainsIdentities, toIsStableUnderComposition, unop, comp_mem, inf, inverseImage, op, unop, containsIdentities, containsIdentities, op, unop, comp_mem, id_mem, instHasOfPostcompPropertyIsomorphismsOfRespectsIso, instHasOfPostcompPropertyMin, instHasOfPostcompPropertyOppositeOpOfHasOfPrecompProperty, instHasOfPostcompPropertyTop, instHasOfPostcompPropertyUnopOfHasOfPrecompPropertyOpposite, instHasOfPrecompPropertyIsomorphismsOfRespectsIso, instHasOfPrecompPropertyMin, instHasOfPrecompPropertyOppositeOpOfHasOfPostcompProperty, instHasOfPrecompPropertyTop, instHasOfPrecompPropertyUnopOfHasOfPostcompPropertyOpposite, instHasTwoOutOfThreePropertyInverseImage, instHasTwoOutOfThreePropertyIsomorphisms, instHasTwoOutOfThreePropertyMin, instHasTwoOutOfThreePropertyOppositeOp, instHasTwoOutOfThreePropertyTop, instHasTwoOutOfThreePropertyUnopOfOpposite, instIsMultiplicativeMultiplicativeClosure, instIsMultiplicativeMultiplicativeClosure', instRespectsOfIsStableUnderComposition, isomorphisms_le_of_containsIdentities, le_multiplicativeClosure, multiplicativeClosure_eq_multiplicativeClosure', multiplicativeClosure_eq_self, multiplicativeClosure_eq_self_iff, multiplicativeClosure_le_iff, multiplicativeClosure_monotone, isStableUnderComposition, stableUnderInverse, of_isIso, of_postcomp, of_precomp, postcomp_iff, precomp_iff, respectsIso_of_isStableUnderComposition, strictMap_multiplicativeClosure_le	74
Total	84

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
ContainsIdentities 📖	CompData	17 math math: ContainsIdentities.inf, AlgebraicGeometry.HasRingHomProperty.containsIdentities, regularEpi.containsIdentities, AlgebraicGeometry.IsLocalIso.eq_iInf, ContainsIdentities.unop, Prod.containsIdentities, IsMultiplicative.toContainsIdentities, AlgebraicGeometry.sourceLocalClosure.instContainsIdentitiesScheme, regularMono.containsIdentities, ContainsIdentities.op, ContainsIdentities.inverseImage, ContainsIdentities.of_op, CategoryTheory.ObjectProperty.instContainsIdentitiesTrWOfContainsZero, AlgebraicGeometry.HasAffineProperty.affineAnd_containsIdentities, instContainsIdentitiesInd, AlgebraicGeometry.IsFinite.instContainsIdentitiesScheme, ContainsIdentities.of_unop
HasOfPostcompProperty 📖	CompData	24 math math: AlgebraicGeometry.instHasOfPostcompPropertySchemeUniversallyClosedIsSeparated, hasOfPostcompProperty_iff_le_diagonal, HasOfPostcompProperty.of_le, AlgebraicGeometry.instHasOfPostcompPropertySchemeIsClosedImmersionIsSeparated, AlgebraicGeometry.Etale.instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified, AlgebraicGeometry.instHasOfPostcompPropertySchemeQuasiSeparatedTopMorphismProperty, AlgebraicGeometry.hasOfPostcompProperty_isOpenImmersion_of_morphismRestrict, instHasOfPostcompPropertyOppositeOpOfHasOfPrecompProperty, instHasOfPostcompPropertyUnopOfHasOfPrecompPropertyOpposite, AlgebraicGeometry.instHasOfPostcompPropertySchemeQuasiCompactQuasiSeparated, instHasOfPostcompPropertyTop, AlgebraicGeometry.IsOpenImmersion.instHasOfPostcompPropertyScheme, AlgebraicGeometry.IsIntegralHom.instHasOfPostcompPropertySchemeIsSeparated, IsStableUnderBaseChange.hasOfPostcompProperty_monomorphisms, AlgebraicGeometry.instHasOfPostcompPropertySchemeIsProperIsSeparated, instHasOfPostcompPropertyMin, instHasOfPostcompPropertyIsomorphismsOfRespectsIso, AlgebraicGeometry.instHasOfPostcompPropertySchemeIsSeparatedTopMorphismProperty, AlgebraicGeometry.IsImmersion.instHasOfPostcompPropertySchemeTopMorphismProperty, HasTwoOutOfThreeProperty.toHasOfPostcompProperty, AlgebraicGeometry.Etale.instHasOfPostcompPropertyScheme, AlgebraicGeometry.instHasOfPostcompPropertySchemeIsAffineHomIsSeparated, AlgebraicGeometry.instHasOfPostcompPropertySchemeIsOpenImmersionOfIsStableUnderBaseChange, AlgebraicGeometry.IsFinite.instHasOfPostcompPropertySchemeIsSeparated
HasOfPrecompProperty 📖	CompData	9 math math: instHasOfPrecompPropertyOppositeOpOfHasOfPostcompProperty, IsStableUnderCobaseChange.hasOfPrecompProperty_epimorphisms, HasOfPrecompProperty.of_le, HasTwoOutOfThreeProperty.toHasOfPrecompProperty, AlgebraicGeometry.instHasOfPrecompPropertySchemeSurjective, instHasOfPrecompPropertyTop, instHasOfPrecompPropertyUnopOfHasOfPostcompPropertyOpposite, instHasOfPrecompPropertyMin, instHasOfPrecompPropertyIsomorphismsOfRespectsIso
HasTwoOutOfThreeProperty 📖	CompData	14 math math: instHasTwoOutOfThreePropertyUnopOfOpposite, CategoryTheory.ObjectProperty.instHasTwoOutOfThreePropertyIsLocal, CategoryTheory.ObjectProperty.instHasTwoOutOfThreePropertyIsoModSerre, instHasTwoOutOfThreePropertyOppositeOp, HomotopicalAlgebra.instHasTwoOutOfThreePropertyFullSubcategoryWeakEquivalences, instHasTwoOutOfThreePropertyIsomorphisms, HomologicalComplex.instHasTwoOutOfThreePropertyQuasiIso, HomotopicalAlgebra.ModelCategory.cm2, CategoryTheory.ObjectProperty.instHasTwoOutOfThreePropertyIsColocal, HomotopicalAlgebra.instHasTwoOutOfThreePropertyOverWeakEquivalences, instHasTwoOutOfThreePropertyTop, instHasTwoOutOfThreePropertyMin, HomotopicalAlgebra.instHasTwoOutOfThreePropertyOppositeWeakEquivalences, instHasTwoOutOfThreePropertyInverseImage
IsMultiplicative 📖	CompData	72 math math: instIsMultiplicativeBijective, AlgebraicGeometry.sourceLocalClosure.instIsMultiplicativeSchemeOfIsStableUnderBaseChange, IsMultiplicative.of_unop, AlgebraicGeometry.instIsMultiplicativeSchemeQuasiCompact, IsMultiplicative.instInverseImage, AlgebraicGeometry.UniversallyOpen.instIsMultiplicativeScheme, CategoryTheory.ObjectProperty.instIsMultiplicativeTrWOfIsTriangulatedOfIsTriangulated, AlgebraicGeometry.instIsMultiplicativeSchemeIsSchemeTheoreticallyDominant, IsMultiplicative.instTop, IsMultiplicative.inf, HomotopicalAlgebra.instIsMultiplicativeTrivialCofibrations, CategoryTheory.ObjectProperty.instIsMultiplicativeIsoModSerre, CategoryTheory.ObjectProperty.instIsMultiplicativeMonoModSerre, AlgebraicGeometry.instIsMultiplicativeSchemeSurjective, CategoryTheory.Functor.relativelyRepresentable.isMultiplicative, AlgebraicGeometry.Flat.instIsMultiplicativeScheme, HomotopicalAlgebra.instIsMultiplicativeFullSubcategoryWeakEquivalences, HomotopicalAlgebra.instIsMultiplicativeFibrations, AlgebraicGeometry.Etale.instIsMultiplicativeScheme, IsMonoidal.toIsMultiplicative, rlp_isMultiplicative, HomologicalComplex.instIsMultiplicativeQuasiIso, AlgebraicGeometry.HasRingHomProperty.isMultiplicative, AlgebraicGeometry.instIsMultiplicativeSchemeQuasiSeparated, IsMultiplicative.op, multiplicativeClosure_eq_self_iff, AlgebraicGeometry.isOpenImmersion_isMultiplicative, HomotopicalAlgebra.instIsMultiplicativeTrivialFibrations, AlgebraicGeometry.instIsMultiplicativeSchemeUniversallyInjective, AlgebraicGeometry.instIsMultiplicativeSchemeLocallyOfFiniteType, llp_isMultiplicative, AlgebraicGeometry.IsIntegralHom.instIsMultiplicativeScheme_1, AlgebraicGeometry.IsClosedImmersion.instIsMultiplicativeScheme, CategoryTheory.ObjectProperty.instIsMultiplicativeIsColocal, AlgebraicGeometry.IsImmersion.instIsMultiplicativeScheme, CategoryTheory.Abelian.instIsMultiplicativeEpiWithInjectiveKernel, AlgebraicGeometry.instIsMultiplicativeSchemeLocallyQuasiFinite, AlgebraicGeometry.IsFinite.instIsMultiplicativeScheme, AlgebraicGeometry.IsLocalIso.instIsMultiplicativeScheme, HasLeftCalculusOfFractions.toIsMultiplicative, CategoryTheory.ObjectProperty.instIsMultiplicativeIsLocal, AlgebraicGeometry.FormallyUnramified.instIsMultiplicativeScheme, AlgebraicGeometry.IsProper.instIsMultiplicativeScheme, AlgebraicGeometry.instIsMultiplicativeSchemeUniversallyClosed, IsMultiplicative.ind_of_preIndSpreads, instIsMultiplicativeMultiplicativeClosure', AlgebraicGeometry.SurjectiveOnStalks.instIsMultiplicativeScheme, instIsMultiplicativeInjective, AlgebraicGeometry.instIsMultiplicativeSchemeIsDominant, instIsMultiplicativeSurjective, IsMultiplicative.naturalityProperty, AlgebraicGeometry.instIsMultiplicativeSchemeSmoothOfRelativeDimensionOfNatNat, AlgebraicGeometry.IsPreimmersion.instIsMultiplicativeScheme, AlgebraicGeometry.IsSeparated.instIsMultiplicativeScheme, HomotopicalAlgebra.instIsMultiplicativeCofibrations, CategoryTheory.NatTrans.instIsMultiplicativeFunctorEquifibered, AlgebraicGeometry.instIsMultiplicativeSchemeIsAffineHom, AlgebraicGeometry.IsIntegralHom.instIsMultiplicativeScheme, HomotopicalAlgebra.instIsMultiplicativeWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition, CategoryTheory.ObjectProperty.instIsMultiplicativeEpiModSerre, HasRightCalculusOfFractions.toIsMultiplicative, IsMultiplicative.instEpimorphisms, IsMultiplicative.instIsomorphisms, CategoryTheory.NatTrans.instIsMultiplicativeFunctorCoequifibered, relative_isMultiplicative, IsMultiplicative.unop, CochainComplex.instIsMultiplicativeIntDegreewiseEpiWithInjectiveKernel, IsStableUnderTransfiniteComposition.instIsMultiplicative, IsMultiplicative.of_op, TopCat.instIsMultiplicativeIsOpenEmbedding, IsMultiplicative.instMonomorphisms, instIsMultiplicativeMultiplicativeClosure
IsStableUnderComposition 📖	CompData	34 math math: AlgebraicGeometry.injective_isStableUnderComposition, AlgebraicGeometry.isOpenImmersion_isStableUnderComposition, AlgebraicGeometry.instIsStableUnderCompositionSchemeSmooth, IsStableUnderComposition.unop, relative_isStableUnderComposition, IsStableUnderComposition.inverseImage, AlgebraicGeometry.IsIntegralHom.instIsStableUnderCompositionScheme, AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderComposition, IsStableUnderComposition.op, AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyQuasiFinite, AlgebraicGeometry.universallyClosed_isStableUnderComposition, AlgebraicGeometry.HasRingHomProperty.stableUnderComposition, AlgebraicGeometry.sourceLocalClosure.instIsStableUnderCompositionSchemeOfIsStableUnderBaseChange, AlgebraicGeometry.quasiCompact_isStableUnderComposition, AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyOfFinitePresentation, AlgebraicGeometry.IsProper.stableUnderComposition, AlgebraicGeometry.UniversallyOpen.instIsStableUnderCompositionSchemeTopologicallyIsOpenMap, AlgebraicGeometry.universallyInjective_isStableUnderComposition, AlgebraicGeometry.isClosedMap_isStableUnderComposition, naturalityProperty.isStableUnderComposition, AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyOfFiniteType, diagonal_isStableUnderComposition, AlgebraicGeometry.IsSeparated.stableUnderComposition, IsStableUnderComposition.inf, IsMultiplicative.toIsStableUnderComposition, AlgebraicGeometry.topologically_isStableUnderComposition, AlgebraicGeometry.UniversallyOpen.instIsStableUnderCompositionScheme, AlgebraicGeometry.Flat.instIsStableUnderCompositionScheme, AlgebraicGeometry.IsFinite.instIsStableUnderCompositionScheme, IsStableUnderComposition.universally, AlgebraicGeometry.FormallyUnramified.instIsStableUnderCompositionScheme, AlgebraicGeometry.quasiSeparated_isStableUnderComposition, IsStableUnderComposition.ind_of_preIndSpreads, HasTwoOutOfThreeProperty.toIsStableUnderComposition
StableUnderInverse 📖	MathDef	1 math math: naturalityProperty.stableUnderInverse
multiplicativeClosure 📖	CompData	11 math math: multiplicativeClosure_eq_self, SimplexCategoryGenRel.multiplicativeClosure_isGenerator_eq_top, SSet.Truncated.HomotopyCategory.multiplicativeClosure_morphismPropertyHomMk, multiplicativeClosure_monotone, CategoryTheory.Cat.FreeRefl.multiplicativeClosure_morphismPropertyHomMk, strictMap_multiplicativeClosure_le, multiplicativeClosure_eq_self_iff, multiplicativeClosure_eq_multiplicativeClosure', le_multiplicativeClosure, multiplicativeClosure_le_iff, instIsMultiplicativeMultiplicativeClosure
multiplicativeClosure' 📖	CompData	2 math math: instIsMultiplicativeMultiplicativeClosure', multiplicativeClosure_eq_multiplicativeClosure'
naturalityProperty 📖	CompOp	3 math math: naturalityProperty.stableUnderInverse, naturalityProperty.isStableUnderComposition, IsMultiplicative.naturalityProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_mem 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	IsStableUnderComposition.comp_mem
id_mem 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	ContainsIdentities.id_mem
instHasOfPostcompPropertyIsomorphismsOfRespectsIso 📖	mathematical	—	HasOfPostcompProperty isomorphisms	—	cancel_right_of_respectsIso
instHasOfPostcompPropertyMin 📖	mathematical	—	HasOfPostcompProperty CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra	—	of_postcomp
instHasOfPostcompPropertyOppositeOpOfHasOfPrecompProperty 📖	mathematical	—	HasOfPostcompProperty Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct	—	of_precomp
instHasOfPostcompPropertyTop 📖	mathematical	—	HasOfPostcompProperty Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra	—	—
instHasOfPostcompPropertyUnopOfHasOfPrecompPropertyOpposite 📖	mathematical	—	HasOfPostcompProperty unop CategoryTheory.Category.toCategoryStruct	—	of_precomp
instHasOfPrecompPropertyIsomorphismsOfRespectsIso 📖	mathematical	—	HasOfPrecompProperty isomorphisms	—	cancel_left_of_respectsIso
instHasOfPrecompPropertyMin 📖	mathematical	—	HasOfPrecompProperty CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra	—	of_precomp
instHasOfPrecompPropertyOppositeOpOfHasOfPostcompProperty 📖	mathematical	—	HasOfPrecompProperty Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct	—	of_postcomp
instHasOfPrecompPropertyTop 📖	mathematical	—	HasOfPrecompProperty Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra	—	—
instHasOfPrecompPropertyUnopOfHasOfPostcompPropertyOpposite 📖	mathematical	—	HasOfPrecompProperty unop CategoryTheory.Category.toCategoryStruct	—	of_postcomp
instHasTwoOutOfThreePropertyInverseImage 📖	mathematical	—	HasTwoOutOfThreeProperty inverseImage	—	IsStableUnderComposition.inverseImage HasTwoOutOfThreeProperty.toIsStableUnderComposition of_postcomp HasTwoOutOfThreeProperty.toHasOfPostcompProperty CategoryTheory.Functor.map_comp of_precomp HasTwoOutOfThreeProperty.toHasOfPrecompProperty
instHasTwoOutOfThreePropertyIsomorphisms 📖	mathematical	—	HasTwoOutOfThreeProperty isomorphisms	—	IsMultiplicative.toIsStableUnderComposition IsMultiplicative.instIsomorphisms CategoryTheory.Category.assoc CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.IsIso.comp_isIso CategoryTheory.IsIso.inv_isIso CategoryTheory.IsIso.inv_hom_id_assoc
instHasTwoOutOfThreePropertyMin 📖	mathematical	—	HasTwoOutOfThreeProperty CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra	—	HasOfPostcompProperty.of_le HasTwoOutOfThreeProperty.toHasOfPostcompProperty inf_le_left HasOfPrecompProperty.of_le HasTwoOutOfThreeProperty.toHasOfPrecompProperty inf_le_right IsStableUnderComposition.inf HasTwoOutOfThreeProperty.toIsStableUnderComposition instHasOfPostcompPropertyMin instHasOfPrecompPropertyMin
instHasTwoOutOfThreePropertyOppositeOp 📖	mathematical	—	HasTwoOutOfThreeProperty Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct	—	IsStableUnderComposition.op HasTwoOutOfThreeProperty.toIsStableUnderComposition instHasOfPostcompPropertyOppositeOpOfHasOfPrecompProperty HasTwoOutOfThreeProperty.toHasOfPrecompProperty instHasOfPrecompPropertyOppositeOpOfHasOfPostcompProperty HasTwoOutOfThreeProperty.toHasOfPostcompProperty
instHasTwoOutOfThreePropertyTop 📖	mathematical	—	HasTwoOutOfThreeProperty Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra	—	IsMultiplicative.toIsStableUnderComposition IsMultiplicative.instTop instHasOfPostcompPropertyTop instHasOfPrecompPropertyTop
instHasTwoOutOfThreePropertyUnopOfOpposite 📖	mathematical	—	HasTwoOutOfThreeProperty unop CategoryTheory.Category.toCategoryStruct	—	IsStableUnderComposition.unop HasTwoOutOfThreeProperty.toIsStableUnderComposition instHasOfPostcompPropertyUnopOfHasOfPrecompPropertyOpposite HasTwoOutOfThreeProperty.toHasOfPrecompProperty instHasOfPrecompPropertyUnopOfHasOfPostcompPropertyOpposite HasTwoOutOfThreeProperty.toHasOfPostcompProperty
instIsMultiplicativeMultiplicativeClosure 📖	mathematical	—	IsMultiplicative multiplicativeClosure	—	CategoryTheory.Category.comp_id CategoryTheory.Category.assoc
instIsMultiplicativeMultiplicativeClosure' 📖	mathematical	—	IsMultiplicative multiplicativeClosure'	—	CategoryTheory.Category.id_comp CategoryTheory.Category.assoc
instRespectsOfIsStableUnderComposition 📖	mathematical	—	Respects CategoryTheory.Category.toCategoryStruct	—	comp_mem
isomorphisms_le_of_containsIdentities 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra isomorphisms	—	of_isIso
le_multiplicativeClosure 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra multiplicativeClosure	—	—
multiplicativeClosure_eq_multiplicativeClosure' 📖	mathematical	—	multiplicativeClosure multiplicativeClosure'	—	le_antisymm multiplicativeClosure_le_iff instIsMultiplicativeMultiplicativeClosure' comp_mem IsMultiplicative.toIsStableUnderComposition instIsMultiplicativeMultiplicativeClosure
multiplicativeClosure_eq_self 📖	mathematical	—	multiplicativeClosure	—	le_antisymm id_mem IsMultiplicative.toContainsIdentities comp_mem IsMultiplicative.toIsStableUnderComposition le_multiplicativeClosure
multiplicativeClosure_eq_self_iff 📖	mathematical	—	multiplicativeClosure IsMultiplicative	—	instIsMultiplicativeMultiplicativeClosure multiplicativeClosure_eq_self
multiplicativeClosure_le_iff 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra multiplicativeClosure	—	LE.le.trans le_multiplicativeClosure id_mem IsMultiplicative.toContainsIdentities comp_mem IsMultiplicative.toIsStableUnderComposition
multiplicativeClosure_monotone 📖	mathematical	—	Monotone CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra multiplicativeClosure	—	instIsMultiplicativeMultiplicativeClosure LE.le.trans le_multiplicativeClosure
of_isIso 📖	—	—	—	—	RespectsIso.postcomp id_mem CategoryTheory.Category.id_comp
of_postcomp 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—	HasOfPostcompProperty.of_postcomp
of_precomp 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—	HasOfPrecompProperty.of_precomp
postcomp_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	of_postcomp RespectsRight.postcomp
precomp_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	of_precomp RespectsLeft.precomp
respectsIso_of_isStableUnderComposition 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra isomorphisms	RespectsIso	—	comp_mem isomorphisms.infer_property CategoryTheory.Iso.isIso_hom
strictMap_multiplicativeClosure_le 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra strictMap multiplicativeClosure	—	le_multiplicativeClosure CategoryTheory.Functor.map_id CategoryTheory.Functor.map_comp

CategoryTheory.MorphismProperty.ContainsIdentities

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqToHom 📖	mathematical	—	CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.eqToHom_refl id_mem
id_mem 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inf 📖	mathematical	—	CategoryTheory.MorphismProperty.ContainsIdentities CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	CategoryTheory.MorphismProperty.id_mem
inverseImage 📖	mathematical	—	CategoryTheory.MorphismProperty.ContainsIdentities CategoryTheory.MorphismProperty.inverseImage	—	CategoryTheory.Functor.map_id CategoryTheory.MorphismProperty.id_mem
of_op 📖	mathematical	—	CategoryTheory.MorphismProperty.ContainsIdentities	—	unop
of_unop 📖	mathematical	—	CategoryTheory.MorphismProperty.ContainsIdentities Opposite CategoryTheory.Category.opposite	—	op
op 📖	mathematical	—	CategoryTheory.MorphismProperty.ContainsIdentities Opposite CategoryTheory.Category.opposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.MorphismProperty.id_mem
unop 📖	mathematical	—	CategoryTheory.MorphismProperty.ContainsIdentities CategoryTheory.MorphismProperty.unop CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.MorphismProperty.id_mem

CategoryTheory.MorphismProperty.HasOfPostcompProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_le 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	CategoryTheory.MorphismProperty.HasOfPostcompProperty	—	CategoryTheory.MorphismProperty.of_postcomp
of_postcomp 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—	—

CategoryTheory.MorphismProperty.HasOfPrecompProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_le 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	CategoryTheory.MorphismProperty.HasOfPrecompProperty	—	CategoryTheory.MorphismProperty.of_precomp
of_precomp 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—	—

CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toHasOfPostcompProperty 📖	mathematical	—	CategoryTheory.MorphismProperty.HasOfPostcompProperty	—	—
toHasOfPrecompProperty 📖	mathematical	—	CategoryTheory.MorphismProperty.HasOfPrecompProperty	—	—
toIsStableUnderComposition 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderComposition	—	—

CategoryTheory.MorphismProperty.IsMultiplicative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inf 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	CategoryTheory.MorphismProperty.ContainsIdentities.inf toContainsIdentities CategoryTheory.MorphismProperty.IsStableUnderComposition.inf toIsStableUnderComposition
instEpimorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative CategoryTheory.MorphismProperty.epimorphisms	—	CategoryTheory.MorphismProperty.epimorphisms.infer_property CategoryTheory.instEpiId CategoryTheory.MorphismProperty.epimorphisms.iff CategoryTheory.epi_comp
instInverseImage 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative CategoryTheory.MorphismProperty.inverseImage	—	CategoryTheory.MorphismProperty.ContainsIdentities.inverseImage toContainsIdentities CategoryTheory.MorphismProperty.IsStableUnderComposition.inverseImage toIsStableUnderComposition
instIsomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative CategoryTheory.MorphismProperty.isomorphisms	—	CategoryTheory.MorphismProperty.isomorphisms.infer_property CategoryTheory.IsIso.id CategoryTheory.MorphismProperty.isomorphisms.iff CategoryTheory.IsIso.comp_isIso
instMonomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative CategoryTheory.MorphismProperty.monomorphisms	—	CategoryTheory.MorphismProperty.monomorphisms.infer_property CategoryTheory.instMonoId CategoryTheory.MorphismProperty.monomorphisms.iff CategoryTheory.mono_comp
instTop 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	—
naturalityProperty 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative CategoryTheory.MorphismProperty.naturalityProperty	—	CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.MorphismProperty.naturalityProperty.isStableUnderComposition
of_op 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative	—	unop
of_unop 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative Opposite CategoryTheory.Category.opposite	—	op
op 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative Opposite CategoryTheory.Category.opposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.MorphismProperty.ContainsIdentities.op toContainsIdentities CategoryTheory.MorphismProperty.comp_mem toIsStableUnderComposition
toContainsIdentities 📖	mathematical	—	CategoryTheory.MorphismProperty.ContainsIdentities	—	—
toIsStableUnderComposition 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderComposition	—	—
unop 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative CategoryTheory.MorphismProperty.unop CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.MorphismProperty.id_mem toContainsIdentities CategoryTheory.MorphismProperty.comp_mem toIsStableUnderComposition

CategoryTheory.MorphismProperty.IsStableUnderComposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_mem 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
inf 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderComposition CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	CategoryTheory.MorphismProperty.comp_mem
inverseImage 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderComposition CategoryTheory.MorphismProperty.inverseImage	—	CategoryTheory.Functor.map_comp CategoryTheory.MorphismProperty.comp_mem
op 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderComposition Opposite CategoryTheory.Category.opposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.MorphismProperty.comp_mem
unop 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderComposition CategoryTheory.MorphismProperty.unop CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.MorphismProperty.comp_mem

CategoryTheory.MorphismProperty.Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
containsIdentities 📖	mathematical	CategoryTheory.MorphismProperty.ContainsIdentities	CategoryTheory.pi CategoryTheory.MorphismProperty.pi	—	CategoryTheory.MorphismProperty.id_mem

CategoryTheory.MorphismProperty.Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
containsIdentities 📖	mathematical	—	CategoryTheory.MorphismProperty.ContainsIdentities CategoryTheory.prod' CategoryTheory.MorphismProperty.prod CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.MorphismProperty.id_mem

CategoryTheory.MorphismProperty.StableUnderInverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op 📖	mathematical	CategoryTheory.MorphismProperty.StableUnderInverse	Opposite CategoryTheory.Category.opposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct	—	—
unop 📖	mathematical	CategoryTheory.MorphismProperty.StableUnderInverse Opposite CategoryTheory.Category.opposite	CategoryTheory.MorphismProperty.unop CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.MorphismProperty.naturalityProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStableUnderComposition 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderComposition CategoryTheory.MorphismProperty.naturalityProperty	—	CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc
stableUnderInverse 📖	mathematical	—	CategoryTheory.MorphismProperty.StableUnderInverse CategoryTheory.MorphismProperty.naturalityProperty	—	CategoryTheory.cancel_epi CategoryTheory.IsIso.epi_of_iso CategoryTheory.Functor.map_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp CategoryTheory.Category.comp_id

---

← Back to Index