NatIso

📁 Source: Mathlib/CategoryTheory/NatIso.lean

Statistics

Metric	Count
Definitions copyObj, isoCopyObj, app, hcomp, ofComponents	5
Theorems copyObj_obj, isoCopyObj_hom_app, isoCopyObj_inv_app, app_hom, app_inv, hom_inv_id_app, hom_inv_id_app_app, hom_inv_id_app_app_app, hom_inv_id_app_app_app_assoc, hom_inv_id_app_app_assoc, hom_inv_id_app_assoc, inv_hom_id_app, inv_hom_id_app_app, inv_hom_id_app_app_app, inv_hom_id_app_app_app_assoc, inv_hom_id_app_app_assoc, inv_hom_id_app_assoc, cancel_natIso_hom_left, cancel_natIso_hom_right, cancel_natIso_hom_right_assoc, cancel_natIso_inv_left, cancel_natIso_inv_right, cancel_natIso_inv_right_assoc, hcomp_hom, hcomp_inv, hom_app_isIso, inv_app_isIso, inv_inv_app, inv_map_inv_app, isIso_app_of_isIso, isIso_inv_app, isIso_map_iff, isIso_of_isIso_app, naturality_1, naturality_1', naturality_1'_assoc, naturality_1_assoc, naturality_2, naturality_2', naturality_2'_assoc, naturality_2_assoc, app, ofComponents_hom_app, ofComponents_inv_app, trans_app, isIso_iff_isIso_app, naturality_1, naturality_1_assoc, naturality_2, naturality_2_assoc	50
Total	55

CategoryTheory.Functor

Definitions

Name	Category	Theorems
copyObj 📖	CompOp	3 math math: isoCopyObj_inv_app, copyObj_obj, isoCopyObj_hom_app
isoCopyObj 📖	CompOp	2 math math: isoCopyObj_inv_app, isoCopyObj_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
copyObj_obj 📖	mathematical	—	obj copyObj	—	—
isoCopyObj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app copyObj CategoryTheory.Iso.hom CategoryTheory.Functor category isoCopyObj obj	—	—
isoCopyObj_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app copyObj CategoryTheory.Iso.inv CategoryTheory.Functor category isoCopyObj obj	—	—

CategoryTheory.Iso

Definitions

Name	Category	Theorems
app 📖	CompOp	86 math math: CategoryTheory.GlueData.diagramIso_app_right, CategoryTheory.Limits.spanCompIso_app_left, CategoryTheory.MonoOver.congr_unitIso, CategoryTheory.Monoidal.transportStruct_associator, CategoryTheory.WithInitial.liftToInitialUnique_hom_app, CategoryTheory.Limits.cospanExt_app_one, app_inv, CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_map_snd, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_map_app_fst, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app, CategoryTheory.Functor.mapContActionCongr_inv, CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionUnitIso, CategoryTheory.IsSifted.factorization_prodComparison_colim, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_zero, CategoryTheory.Functor.mapContActionCongr_hom, CategoryTheory.Localization.equivalence_counitIso_app, AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans, CategoryTheory.Localization.Monoidal.map_hexagon_forward, CategoryTheory.Limits.cospanExt_app_right, CategoryTheory.Limits.spanCompIso_app_zero, CategoryTheory.Localization.Monoidal.map_hexagon_reverse, CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_map_app_snd, AlgebraicGeometry.Scheme.SpecΓIdentity_app, CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom, CategoryTheory.GlueData.diagramIso_app_left, CategoryTheory.Limits.spanCompIso_app_right, CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr_eq, CategoryTheory.Localization.Monoidal.map_hexagon_reverse_assoc, app_hom, CategoryTheory.NatIso.trans_app, CategoryTheory.Under.postEquiv_counitIso, CategoryTheory.WithTerminal.liftToTerminalUnique_inv_app, SimplicialObject.Splitting.ofIso_isColimit', CategoryTheory.Limits.Cones.functorialityEquivalence_unitIso, CategoryTheory.Limits.spanExt_app_one, CategoryTheory.NatIso.ofComponents.app, CategoryTheory.Limits.spanExt_app_left, CategoryTheory.Over.postEquiv_counitIso, CategoryTheory.Functor.RepresentableBy.equivUliftYonedaIso_symm_apply_homEquiv, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app, CategoryTheory.Monoidal.transportStruct_leftUnitor, CategoryTheory.Monoidal.transportStruct_rightUnitor, CategoryTheory.Discrete.natIso_app, CategoryTheory.Limits.cospanExt_app_left, CategoryTheory.MonoOver.congr_inverse, CategoryTheory.Functor.CorepresentableBy.equivUliftCoyonedaIso_symm_apply_homEquiv, CategoryTheory.Limits.Cocones.functorialityEquivalence_counitIso, CategoryTheory.WithInitial.equivComma_unitIso_inv_app_app, CategoryTheory.Functor.mapActionCongr_inv, CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_map_fst, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app, CategoryTheory.Limits.Cones.functorialityEquivalence_counitIso, HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso, CategoryTheory.WithInitial.equivComma_unitIso_hom_app_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_map_snd, CommRingCat.tensorProdIsoPushout_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, CategoryTheory.Functor.mapActionCongr_hom, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, CategoryTheory.PreGaloisCategory.autEmbedding_apply, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_app_app, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_one, CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_map_app_fst, CategoryTheory.Over.postEquiv_unitIso, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_zero, CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionAssocIso, CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso, CategoryTheory.Limits.cospanCompIso_app_one, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_map_app_snd, CategoryTheory.Limits.cospanCompIso_app_left, CategoryTheory.Limits.spanExt_app_right, CategoryTheory.MonoOver.congr_counitIso, CategoryTheory.Under.postEquiv_unitIso, CategoryTheory.yonedaYonedaColimit_app_inv, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_one, CategoryTheory.Localization.SmallShiftedHom.equiv_apply, CategoryTheory.WithInitial.liftToInitialUnique_inv_app, AlgebraicTopology.DoldKan.N₁Γ₀_app, CategoryTheory.WithTerminal.equivComma_unitIso_hom_app_app, CategoryTheory.WithTerminal.liftToTerminalUnique_hom_app, CategoryTheory.WithTerminal.equivComma_unitIso_inv_app_app, CategoryTheory.Limits.Cocones.functorialityEquivalence_unitIso, CategoryTheory.Localization.Monoidal.map_hexagon_forward_assoc, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_map_fst, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app, CategoryTheory.Limits.cospanCompIso_app_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_hom 📖	mathematical	—	hom CategoryTheory.Functor.obj app CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category	—	—
app_inv 📖	mathematical	—	inv CategoryTheory.Functor.obj app CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category	—	—
hom_inv_id_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app hom CategoryTheory.Functor CategoryTheory.Functor.category inv CategoryTheory.CategoryStruct.id	—	—
hom_inv_id_app_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app hom inv CategoryTheory.CategoryStruct.id	—	—
hom_inv_id_app_app_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app hom inv CategoryTheory.CategoryStruct.id	—	—
hom_inv_id_app_app_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app hom inv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' hom_inv_id_app_app_app
hom_inv_id_app_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app hom inv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' hom_inv_id_app_app
hom_inv_id_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app hom CategoryTheory.Functor CategoryTheory.Functor.category inv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' hom_inv_id_app
inv_hom_id_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app inv CategoryTheory.Functor CategoryTheory.Functor.category hom CategoryTheory.CategoryStruct.id	—	—
inv_hom_id_app_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app inv hom CategoryTheory.CategoryStruct.id	—	—
inv_hom_id_app_app_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app inv hom CategoryTheory.CategoryStruct.id	—	—
inv_hom_id_app_app_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app inv hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inv_hom_id_app_app_app
inv_hom_id_app_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app inv hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inv_hom_id_app_app
inv_hom_id_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app inv CategoryTheory.Functor CategoryTheory.Functor.category hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inv_hom_id_app

CategoryTheory.NatIso

Definitions

Name	Category	Theorems
hcomp 📖	CompOp	2 math math: hcomp_inv, hcomp_hom
ofComponents 📖	CompOp	131 math math: CategoryTheory.comonEquiv_unitIso, CategoryTheory.eq_counitIso, CategoryTheory.Limits.coconeEquivalenceOpConeOp_unitIso, CategoryTheory.MonoOver.congr_unitIso, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_unitIso, CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso_inv, CategoryTheory.CostructuredArrow.prodEquivalence_counitIso, CategoryTheory.Under.equivalenceOfIsInitial_counitIso, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_counitIso, CategoryTheory.Over.equivalenceOfIsTerminal_counitIso, CategoryTheory.Comon.Comon_EquivMon_OpOp_counitIso, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_unitIso, CategoryTheory.Comma.opEquiv_counitIso, CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_counitIso, CategoryTheory.Functor.Final.coconesEquiv_unitIso, ofComponents_inv_app, CategoryTheory.Limits.Cocones.whiskeringEquivalence_unitIso, FinPartOrd.dualEquiv_unitIso, CategoryTheory.Cat.opEquivalence_counitIso, CategoryTheory.equivToOverUnit_unitIso, CoalgCat.comonEquivalence_counitIso, CategoryTheory.StructuredArrow.preEquivalence_unitIso, CategoryTheory.Limits.Cocones.precomposeEquivalence_unitIso, CategoryTheory.Over.postAdjunctionLeft_unit_app_left, CategoryTheory.Functor.Initial.conesEquiv_counitIso, CategoryTheory.Functor.opUnopEquiv_counitIso, CategoryTheory.StructuredArrow.ofCommaSndEquivalence_unitIso, CategoryTheory.StructuredArrow.ofCommaSndEquivalence_counitIso, CategoryTheory.skeletonEquivalence_unitIso, CategoryTheory.StructuredArrow.prodEquivalence_unitIso, CategoryTheory.Limits.pullbackConeEquivBinaryFan_counitIso, CategoryTheory.AsSmall.equiv_unitIso, CategoryTheory.ForgetEnrichment.equiv_unitIso, CategoryTheory.AsSmall.equiv_counitIso, CategoryTheory.Limits.Cones.equivalenceOfReindexing_counitIso, FinPartOrd.dualEquiv_counitIso, CategoryTheory.Cat.opEquivalence_unitIso, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_counitIso, CategoryTheory.Limits.Cones.whiskeringEquivalence_unitIso, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_counitIso, CategoryTheory.forgetEnrichmentOppositeEquivalence_unitIso, CategoryTheory.Under.postEquiv_counitIso, TopologicalSpace.Opens.mapMapIso_unitIso, CategoryTheory.Limits.Cones.postcomposeEquivalence_unitIso, CategoryTheory.Limits.Cones.postcomposeEquivalence_counitIso, CategoryTheory.Limits.Cones.functorialityEquivalence_unitIso, CategoryTheory.Limits.Cocone.equivStructuredArrow_unitIso, CategoryTheory.Functor.Initial.conesEquiv_unitIso, ofComponents.app, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_unitIso, CategoryTheory.Over.postEquiv_counitIso, CategoryTheory.equivToOverUnit_counitIso, CategoryTheory.CostructuredArrow.prodEquivalence_unitIso, CategoryTheory.Limits.Cones.whiskeringEquivalence_counitIso, CategoryTheory.skeletonEquivalence_counitIso, OrderIso.equivalence_counitIso, CategoryTheory.Under.equivalenceOfIsInitial_unitIso, CoalgCat.comonEquivalence_unitIso, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_counitIso, CategoryTheory.Functor.equiv_unitIso, CategoryTheory.forgetEnrichmentOppositeEquivalence_counitIso, CategoryTheory.Comon.Comon_EquivMon_OpOp_unitIso, CategoryTheory.coalgebraEquivOver_counitIso, FundamentalGroupoid.punitEquivDiscretePUnit_unitIso, CategoryTheory.Functor.RepresentableBy.uniqueUpToIso_hom, CategoryTheory.Equivalence.symmEquiv_counitIso, CategoryTheory.Limits.Cocones.functorialityEquivalence_counitIso, commAlgCatEquivUnder_unitIso, CategoryTheory.Equivalence.induced_unitIso, CategoryTheory.algebraEquivUnder_unitIso, CategoryTheory.Over.iteratedSliceEquiv_unitIso, CategoryTheory.ShrinkHoms.equivalence_counitIso, CategoryTheory.Equivalence.symmEquiv_unitIso, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_unitIso, alexDiscEquivPreord_unitIso, CategoryTheory.Limits.Cones.functorialityEquivalence_counitIso, CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_counitIso, CategoryTheory.Comma.opEquiv_unitIso, CategoryTheory.Functor.opUnopEquiv_unitIso, CategoryTheory.Limits.Cone.equivCostructuredArrow_counitIso, CategoryTheory.algebraEquivUnder_counitIso, CategoryTheory.Functor.CorepresentableBy.equivUliftCoyonedaIso_apply, CategoryTheory.Subfunctor.equivalenceMonoOver_unitIso, CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso_hom, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_counitIso, CategoryTheory.Over.equivalenceOfIsTerminal_unitIso, CategoryTheory.Over.iteratedSliceEquiv_counitIso, CategoryTheory.Groupoid.invEquivalence_counitIso, CategoryTheory.Functor.RepresentableBy.uniqueUpToIso_inv, CategoryTheory.eq_unitIso, CategoryTheory.subterminalsEquivMonoOverTerminal_unitIso, CategoryTheory.Over.postEquiv_unitIso, CategoryTheory.Functor.Final.coconesEquiv_counitIso, CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso, CategoryTheory.ForgetEnrichment.equiv_counitIso, CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_unitIso, CategoryTheory.Limits.Cones.equivalenceOfReindexing_unitIso, CategoryTheory.Limits.coconeEquivalenceOpConeOp_counitIso, CategoryTheory.Functor.RepresentableBy.equivUliftYonedaIso_apply, Types.monoOverEquivalenceSet_unitIso, CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_unitIso, CategoryTheory.coalgebraEquivOver_unitIso, CategoryTheory.Limits.Cone.equivCostructuredArrow_unitIso, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_unitIso, CategoryTheory.StructuredArrow.preEquivalence_counitIso, alexDiscEquivPreord_counitIso, TopologicalSpace.Opens.mapMapIso_counitIso, CategoryTheory.Under.postAdjunctionRight_counit_app_right, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_counitIso, CategoryTheory.MonoOver.congr_counitIso, CategoryTheory.Groupoid.invEquivalence_unitIso, CategoryTheory.StructuredArrow.prodEquivalence_counitIso, CategoryTheory.equivEssImageOfReflective_counitIso, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_unitIso, CategoryTheory.Under.postEquiv_unitIso, CategoryTheory.Limits.pullbackConeEquivBinaryFan_unitIso, CategoryTheory.ShrinkHoms.equivalence_unitIso, Types.monoOverEquivalenceSet_counitIso, CategoryTheory.Sum.functorEquiv_unitIso, CategoryTheory.Limits.Cocone.equivStructuredArrow_counitIso, OrderIso.equivalence_unitIso, CategoryTheory.piEquivalenceFunctorDiscrete_counitIso, CategoryTheory.Functor.equiv_counitIso, CategoryTheory.Limits.Cocones.whiskeringEquivalence_counitIso, CategoryTheory.Limits.Cocones.functorialityEquivalence_unitIso, CategoryTheory.Subfunctor.equivalenceMonoOver_counitIso, CategoryTheory.Limits.Cocones.precomposeEquivalence_counitIso, CategoryTheory.Sum.functorEquiv_counitIso, CategoryTheory.Equivalence.induced_counitIso, CategoryTheory.comonEquiv_counitIso, ofComponents_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cancel_natIso_hom_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.IsIso.epi_of_iso hom_app_isIso IsPreorder.toRefl IsEquiv.toIsPreorder iff_isEquiv
cancel_natIso_hom_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.IsIso.mono_of_iso hom_app_isIso IsPreorder.toRefl IsEquiv.toIsPreorder iff_isEquiv
cancel_natIso_hom_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.IsIso.mono_of_iso hom_app_isIso IsPreorder.toRefl IsEquiv.toIsPreorder iff_isEquiv
cancel_natIso_inv_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.IsIso.epi_of_iso inv_app_isIso IsPreorder.toRefl IsEquiv.toIsPreorder iff_isEquiv
cancel_natIso_inv_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.IsIso.mono_of_iso inv_app_isIso IsPreorder.toRefl IsEquiv.toIsPreorder iff_isEquiv
cancel_natIso_inv_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.IsIso.mono_of_iso inv_app_isIso IsPreorder.toRefl IsEquiv.toIsPreorder iff_isEquiv
hcomp_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp hcomp CategoryTheory.NatTrans.hcomp	—	—
hcomp_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp hcomp CategoryTheory.NatTrans.hcomp	—	—
hom_app_isIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category	—	—
inv_app_isIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category	—	—
inv_inv_app 📖	mathematical	—	CategoryTheory.inv CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category inv_app_isIso CategoryTheory.Iso.hom	—	—
inv_map_inv_app 📖	mathematical	—	CategoryTheory.inv CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Iso.inv isIso_app_of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.hom	—	—
isIso_app_of_isIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.NatTrans.app	—	—
isIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj isIso_app_of_isIso	—	—
isIso_map_iff 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—
isIso_of_isIso_app 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.NatTrans.app	CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.Iso.isIso_hom CategoryTheory.NatTrans.naturality
naturality_1 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.map CategoryTheory.Iso.hom	—	CategoryTheory.NatTrans.naturality CategoryTheory.Iso.inv_hom_id_app_assoc
naturality_1' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.inv CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	CategoryTheory.NatTrans.naturality CategoryTheory.IsIso.inv_hom_id_assoc
naturality_1'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.inv CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' naturality_1'
naturality_1_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.map CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' naturality_1
naturality_2 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	CategoryTheory.NatTrans.naturality CategoryTheory.Iso.hom_inv_id_app_assoc
naturality_2' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.inv	—	—
naturality_2'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' naturality_2'
naturality_2_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' naturality_2
ofComponents_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category ofComponents CategoryTheory.Functor.obj	—	—
ofComponents_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category ofComponents CategoryTheory.Functor.obj	—	—
trans_app 📖	mathematical	—	CategoryTheory.Iso.app CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj	—	—

CategoryTheory.NatIso.ofComponents

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.hom	CategoryTheory.Iso.app CategoryTheory.NatIso.ofComponents	—	CategoryTheory.Iso.ext

CategoryTheory.NatTrans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_iff_isIso_app 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj app	—	CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.NatIso.isIso_of_isIso_app
naturality_1 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.inv app CategoryTheory.Iso.hom	—	naturality_assoc CategoryTheory.Iso.map_inv_hom_id CategoryTheory.Category.comp_id
naturality_1_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.inv app CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' naturality_1
naturality_2 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.hom app CategoryTheory.Iso.inv	—	naturality_assoc CategoryTheory.Iso.map_hom_inv_id CategoryTheory.Category.comp_id
naturality_2_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.hom app CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' naturality_2

---

← Back to Index