Full

📁 Source: Mathlib/CategoryTheory/Galois/Full.lean

Statistics

Metric	Count
Definitions Full	1
Theorems exists_lift_of_mono, exists_lift_of_mono_of_isConnected, functorToAction_full	3
Total	4

CategoryTheory.Functor

Definitions

Name	Category	Theorems
Full 📖	CompData	217 math math: ModuleCat.instFullUliftFunctor, CategoryTheory.StructuredArrow.instFullUnderToUnder, CommMonCat.instFullMonCatForget₂MonoidHomCarrierCarrier, CategoryTheory.ULiftYoneda.instFullFunctorOppositeTypeUliftYoneda, CategoryTheory.CommGrp.instFullCommMonForget₂CommMon, CommRingCat.instFullRingCatForget₂RingHomCarrierCarrier, CategoryTheory.Grpd.forgetToCat_full, CategoryTheory.nerve.instFullCatTruncatedOfNatNatNerveFunctor₂, CommMonCat.forget₂_full, SSet.Truncated.sk.full, CategoryTheory.instFullMonFunctorOppositeMonCatYonedaMon, instFullFintypeCatProfiniteToProfinite, full_whiskeringRight_obj, SheafOfModules.instFullPresheafOfModulesValRingCatForget, CategoryTheory.IsFiltered.SmallFilteredIntermediate.instFullInclusion, CategoryTheory.instFullSheafSheafComposeOfFaithful, CategoryTheory.instFullCatTypeToCat, CondensedMod.LocallyConstant.instFullModuleCatFunctor, CategoryTheory.ObjectProperty.full_ιOfLE, CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, CategoryTheory.SimplicialObject.Truncated.cosk.full, IsEquivalence.full, CategoryTheory.Equivalence.full_functor, CategoryTheory.Abelian.freyd_mitchell, CategoryTheory.MorphismProperty.Comma.instFullChangeProp, instFullOppositeTypeRestrictedULiftYonedaOfIsDense, CategoryTheory.GrothendieckTopology.instFullSheafTypeYoneda, CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.full, compactumToCompHaus.full, CategoryTheory.Quotient.full_functor, HomotopyCategory.instFullHomologicalComplexQuotient, CategoryTheory.CostructuredArrow.instFullOverToOver, ModuleCat.forget₂_addCommGroup_full, CategoryTheory.Coreflective.comparison_full, CategoryTheory.Adjunction.full_R_of_isSplitMono_counit_app, instFullCompHausCondensedTypeCompHausToCondensed', CategoryTheory.Coyoneda.ULiftCoyoneda.instFullOppositeFunctorTypeUliftCoyoneda, ComplexShape.Embedding.instFullHomotopyCategoryExtendHomotopyFunctor, CategoryTheory.ObjectProperty.full_ι, IsOpenMap.functorFullOfMono, AlgebraicGeometry.instFullOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace, CategoryTheory.Localization.instFullFunctorWhiskeringLeftFunctor', CompHausLike.instFullTopCatCompHausLikeToTop, CategoryTheory.instFullAlgebraToMonadAdjComparison, Full.mapCommGrp, instFullProdCurry₃, instFullFunctor, CategoryTheory.MorphismProperty.Comma.instFullTopCommaForget, CategoryTheory.Types.instFullForgetTypeHom, CategoryTheory.Cat.FreeRefl.instFullPathsQuotientFunctor, AlgebraicGeometry.instFullModuleCatCarrierModulesSpecOfFunctor, CategoryTheory.instFullDecomposedDecomposedTo, Full.id, CategoryTheory.Pseudofunctor.CoGrothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.StructuredArrow.full_map₂, CategoryTheory.instFullIndYoneda, CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete, CategoryTheory.ObjectProperty.instFullFullSubcategoryLift, CommGrpCat.instFullGrpCatForget₂MonoidHomCarrierCarrier, instFullCompHausCondensedSetCompHausToCondensed, CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, AlgebraicGeometry.Scheme.Modules.instFullPushforward, CategoryTheory.GrothendieckTopology.instFullSheafTypeUliftYoneda, AddCommMonCat.forget₂_full, CategoryTheory.Idempotents.instFullKaroubiToKaroubi, CategoryTheory.WithInitial.instFullIncl, AlgebraicGeometry.Spec.full, SSet.Truncated.HomotopyCategory.instFullFreeReflOneTruncation₂QuotientFunctor, LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, CategoryTheory.uliftFunctor_full, AddCommMonCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier, HomotopicalAlgebra.FibrantObject.instFullHoCatToHoCat, CategoryTheory.Abelian.full_comp_preadditiveCoyonedaObj, AugmentedSimplexCategory.instFullSimplexCategoryInclusion, CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.full_embedding, CategoryTheory.instFullSubterminalsSubterminalInclusion, CommGrpCat.instFullUliftFunctor, CategoryTheory.Comma.instFullCompPreLeft, HomotopicalAlgebra.CofibrantObject.instFullHoCatToHoCat, HomotopyCategory.instFullFunctorHomologicalComplexObjWhiskeringLeftQuotient, Semigrp.forget₂_full, CategoryTheory.Localization.full_whiskeringLeft, CategoryTheory.SimplicialObject.Truncated.sk.full, CategoryTheory.CostructuredArrow.instFullCompPre, CategoryTheory.full_linearCoyoneda, DerivedCategory.instFullSingleFunctor, AlgebraicGeometry.AffineScheme.forgetToScheme_full, CategoryTheory.Idempotents.instFullKaroubiFunctorKaroubiFunctorCategoryEmbedding, rightOp_full, FullyFaithful.full, CategoryTheory.MorphismProperty.instFullUnderTopUnderForget, CategoryTheory.Limits.Bicones.functoriality_full, AlgebraicGeometry.Scheme.instFullOppositeIdealSheafDataOverSubschemeFunctor, CategoryTheory.CostructuredArrow.full_map₂, instFullActionMapActionOfFaithful, CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instFullInclusion, CategoryTheory.full_preadditiveCoyoneda, instFullLightDiagram'LightDiagramToLightFunctor, instFullPreordCatPreordToCat, leftOp_full, Full.mapCommMon, ComplexShape.Embedding.instFullHomologicalComplexExtendFunctor, CategoryTheory.Adjunction.full_L_of_isSplitEpi_unit_app, CategoryTheory.Limits.Cones.functoriality_full, instFullProdUncurry, CategoryTheory.Sigma.instFullSigmaIncl, AddCommGrpCat.instFullAddGrpCatForget₂AddMonoidHomCarrierCarrier, LightCondSet.LocallyConstant.instFullLightCondensedTypeDiscrete, CategoryTheory.Yoneda.yoneda_full, AddSemigrp.forget₂_full, Full.mapMon, CategoryTheory.Comma.full_map, CategoryTheory.instFullGrpFunctorOppositeGrpCatYonedaGrp, FintypeCat.instFullIncl, CategoryTheory.Join.inclRightFull, CategoryTheory.instFullSkeletonFromSkeleton, DeltaGenerated.instFullTopCatDeltaGeneratedToTop, CategoryTheory.Comma.instFullCompPreRight, CategoryTheory.Comma.instFullCompPostOfFaithful, MonCat.toCat_full, CategoryTheory.nerveFunctor.full, FintypeCat.Skeleton.instFullIncl, instFullProdUncurry₃, CategoryTheory.full_preadditiveYoneda, CategoryTheory.Limits.Cocones.functoriality_full, GrpCat.instFullMonCatForget₂MonoidHomCarrierCarrier, CategoryTheory.Reflective.comparison_full, RingCat.instFullSemiRingCatForget₂RingHomCarrierCarrier, CategoryTheory.MorphismProperty.instFullOverTopOverForget, Full.mapGrp, CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor, FGModuleCat.instFullUlift, AlexDisc.forgetToTop_full, CategoryTheory.instFullFunctorConstOfIsConnected, instFullSkeletonMapSkeleton, Action.full_res, instFullFGAlgCatUliftFunctor, instFullProdCurry, LightCondMod.LocallyConstant.instFullModuleCatFunctor, CochainComplex.instFullIntSingleFunctor, TopCat.Sheaf.forget_full, CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete, CategoryTheory.Quotient.full_whiskeringLeft_functor, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full, CategoryTheory.Coyoneda.coyoneda_full, CategoryTheory.full_linearYoneda, instFullOppositeOp, CategoryTheory.Under.instFullObjPostOfFaithful, CategoryTheory.CommMon.instFullMonForget₂Mon, CategoryTheory.CostructuredArrow.instFullCompObjPostOfFaithful, LightCondSet.LocallyConstant.instFullFunctor, CategoryTheory.WithTerminal.instFullIncl, instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet, Full.of_comp_faithful_iso, AlgebraicGeometry.Scheme.Modules.instFullPresheafOfModulesToPresheafOfModules, SSet.Truncated.cosk.full, instFullLightDiagramProfiniteLightDiagramToProfinite, CategoryTheory.Over.instFullObjPostOfFaithful, CategoryTheory.Limits.FormalCoproduct.instFullIncl, HomotopicalAlgebra.CofibrantObject.instFullHoCatHoCatιCofibrantObject, Full.of_iso, CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf, CategoryTheory.Abelian.FreydMitchell.instFullModuleCatEmbeddingRingFunctor, CategoryTheory.Mat.instFullMat_SingleObjMulOppositeEquivalenceSingleObjInverse, AlgebraicGeometry.Scheme.instFullEtaleOverForget, LightCondMod.LocallyConstant.instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf, CategoryTheory.MorphismProperty.instFullCostructuredArrowTopOverToOver, CompHausLike.instFullToCompHausLike, AddCommGrpCat.instFullUliftFunctor, DerivedCategory.instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, TopCat.instFullUliftFunctor, FinBoolAlg.forgetToBoolAlg_full, LightCondMod.LocallyConstant.instFullModuleCatLightCondensedDiscrete, CategoryTheory.MonoOver.full_map, CategoryTheory.instFullSheafFunctorOppositeCompSheafComposeSheafToPresheafOfFaithful, CategoryTheory.instFullFunctorOppositeTypeShrinkYoneda, FGModuleCat.instFullModuleCatForget₂LinearMapIdCarrierObjIsFG, instFullTriangleMapTriangleOfFaithful, CategoryTheory.Mat_.Embedding.instFullEmbedding, CategoryTheory.Limits.BinaryBicones.functoriality_full, AlgebraicGeometry.Scheme.instFullLocallyRingedSpaceForgetToLocallyRingedSpace, AddGrpCat.instFullUliftFunctor, PresheafOfModules.instFullRestrictScalarsIdFunctorOppositeRingCat, CategoryTheory.StructuredArrow.instFullCompPre, CategoryTheory.Equivalence.full_inverse, AddGrpCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier, CondensedSet.LocallyConstant.instFullFunctor, Full.of_comp_faithful, CompactlyGenerated.instFullTopCatCompactlyGeneratedToTop, CategoryTheory.instFullSheafFunctorOppositeSheafToPresheaf, Full.comp, CategoryTheory.instFullCoalgebraToComonadAdjComparison, HomologicalComplex.instFullSingle, CommAlgCat.instFullUliftFunctor, CategoryTheory.StructuredArrow.instFullObjCompPostOfFaithful, IsDenseSubsite.full_sheafPushforwardContinuous, Full.toEssImage, AlgebraicGeometry.AffineScheme.Spec_full, HomotopicalAlgebra.BifibrantObject.instFullHoCatToHoCat, instFullFintypeCatLightProfiniteToLightProfinite, CategoryTheory.Join.inclLeftFull, SimplexCategory.SkeletalFunctor.instFullNonemptyFinLinOrdSkeletalFunctor, CommSemiRingCat.instFullSemiRingCatForget₂RingHomCarrierCarrier, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, Sequential.instFullTopCatSequentialToTop, CategoryTheory.PreGaloisCategory.functorToAction_full, CategoryTheory.Coreflective.toFull, FintypeCat.instFullForgetHomCarrier, CategoryTheory.Grp.instFullMonForget₂Mon, CategoryTheory.instFullIndFunctorOppositeTypeInclusion, instFullCondensedTypeCondensedSetUlift, CategoryTheory.Reflective.toFull, GrpCat.instFullUliftFunctor, IsCoverDense.full_sheafPushforwardContinuous, instFullWitness, CategoryTheory.InducedCategory.full, CategoryTheory.CommGrp.instFullGrpForget₂Grp

CategoryTheory.PreGaloisCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lift_of_mono 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.CategoryStruct.comp Action FintypeCat FintypeCat.instCategory CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj functorToAction CategoryTheory.Iso.hom CategoryTheory.Functor.map	—	CategoryTheory.GaloisCategory.toPreGaloisCategory CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts CategoryTheory.FintypeCat.instGaloisCategoryActionFintypeCat has_decomp_connected_components' Action.instHasFiniteCoproducts CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.FintypeCat.hasFiniteColimits CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction CategoryTheory.Category.assoc CategoryTheory.Iso.inv_comp_eq CategoryTheory.Limits.Sigma.hom_ext CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Limits.sigmaComparison_map_desc CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.ι_colimMap_assoc CategoryTheory.Functor.mono_of_mono_map instReflectsMonomorphismsActionFintypeCatAutFunctorFunctorToAction CategoryTheory.mono_comp CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.hom_inv_id_assoc exists_lift_of_mono_of_isConnected CategoryTheory.Limits.MonoCoprod.mono_ι instMonoCoprod Subtype.finite CategoryTheory.Iso.isIso_hom
exists_lift_of_mono_of_isConnected 📖	mathematical	—	IsConnected CategoryTheory.Mono CategoryTheory.CategoryStruct.comp Action FintypeCat FintypeCat.instCategory CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj functorToAction CategoryTheory.Iso.hom CategoryTheory.Functor.map	—	CategoryTheory.GaloisCategory.toPreGaloisCategory nonempty_fiber_of_isConnected CategoryTheory.FintypeCat.instPreGaloisCategoryActionFintypeCat CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomCarrierV fiber_in_connected_component PreservesIsConnected.preserves instPreservesIsConnectedActionFintypeCatAutFunctorFunctorToAction connected_component_unique CategoryTheory.FintypeCat.instGaloisCategoryActionFintypeCat CategoryTheory.Functor.map_mono instPreservesMonomorphismsActionFintypeCatAutFunctorFunctorToAction evaluation_injective_of_isConnected CategoryTheory.Functor.map_comp CategoryTheory.comp_apply
functorToAction_full 📖	mathematical	—	CategoryTheory.Functor.Full Action FintypeCat FintypeCat.instCategory CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory functorToAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory CategoryTheory.Limits.instHasBinaryProductObjOfPreservesLimitDiscreteWalkingPairPair CategoryTheory.Limits.hasLimitOfHasLimitsOfShape instHasBinaryProducts CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction CategoryTheory.instMonoId CategoryTheory.Limits.prod.lift_fst CategoryTheory.mono_of_mono CategoryTheory.mono_comp CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv exists_lift_of_mono CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.IsIso.id CategoryTheory.Limits.PreservesLimitPair.iso_inv_fst CategoryTheory.Limits.limit.lift_π CategoryTheory.IsIso.comp_isIso CategoryTheory.isIso_of_reflects_iso instReflectsIsomorphismsActionFintypeCatAutFunctorFunctorToAction CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso Action.hom_ext FintypeCat.hom_ext CategoryTheory.Category.comp_id CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv CategoryTheory.inv.congr_simp CategoryTheory.IsIso.Iso.inv_inv CategoryTheory.Limits.PreservesLimitPair.iso_inv_snd CategoryTheory.Iso.hom_inv_id_assoc

---

← Back to Index