EssSurj

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

Statistics

Metric	Count
Definitions EssSurj, fiberIsoQuotientStabilizer	2
Theorems exists_lift_of_continuous, exists_lift_of_quotient_openSubgroup, has_decomp_quotients	3
Total	5

CategoryTheory.Functor

Definitions

Name	Category	Theorems
EssSurj 📖	CompData	65 math math: essSurj_of_comp_fully_faithful, SimplexCategory.SkeletalFunctor.instEssSurjNonemptyFinLinOrdSkeletalFunctor, CategoryTheory.Localization.essSurj, essSurj_of_surj, CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, ModuleCat.forget₂_addCommGrp_essSurj, CategoryTheory.Comma.instEssSurjCompPostOfFull, CategoryTheory.StructuredArrow.instEssSurjCompPre, CategoryTheory.StructuredArrow.instEssSurjObjCompPostOfFull, CategoryTheory.RelCat.graphFunctor_essSurj, compactumToCompHaus.essSurj, instEssSurjOppositeOp, CategoryTheory.Localization.essSurj_mapComposableArrows_of_hasRightCalculusOfFractions, CategoryTheory.CostructuredArrow.essSurj_map₂, CategoryTheory.CostructuredArrow.instEssSurjCompPre, CategoryTheory.Mat.instEssSurjMat_SingleObjMulOppositeEquivalenceSingleObjInverse, CategoryTheory.CostructuredArrow.instEssSurjOverToOver, HomotopyCategory.instEssSurjHomologicalComplexQuotient, CategoryTheory.Under.instEssSurjObjPostOfFull, CategoryTheory.instEssSurjCoalgebraToComonadAdjComparison, CategoryTheory.Equivalence.essSurj_functor, CategoryTheory.Idempotents.instEssSurjKaroubiToKaroubiOfIsIdempotentComplete, instEssSurjId, CategoryTheory.instEssSurjAlgebraToMonadAdjComparison, CategoryTheory.instEssSurjSkeletonFromSkeleton, CategoryTheory.instEssSurjDecomposedDecomposedTo, DerivedCategory.instEssSurjHomotopyCategoryIntUpQh, IsEquivalence.essSurj, FintypeCat.Skeleton.instEssSurjIncl, CategoryTheory.CostructuredArrow.instEssSurjCompObjPostOfFull, CategoryTheory.Pseudofunctor.IsStack.essSurj_of_sieve, AlgebraicGeometry.AffineScheme.Spec_essSurj, DerivedCategory.instEssSurjArrowHomotopyCategoryIntUpMapArrowQh, CategoryTheory.LocalizerMorphism.essSurj_of_hasRightResolutions, CategoryTheory.Comma.instEssSurjCompPreLeft, CategoryTheory.Pseudofunctor.CoGrothendieck.instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.Quotient.essSurj_functor, EssSurj.ofUnivLE, CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContActionOfFiberFunctor, CategoryTheory.Pseudofunctor.IsStackFor.essSurj, instEssSurjOppositeRightOp, CategoryTheory.Localization.essSurj_mapArrow_of_hasRightCalculusOfFractions, CategoryTheory.Over.instEssSurjObjPostOfFull, CategoryTheory.Localization.essSurj_mapArrow, CategoryTheory.Comma.essSurj_map, instEssSurjSkeletonMapSkeleton, essSurj_of_iso, CategoryTheory.Comma.instEssSurjCompPreRight, EssSurj.toEssImage, DerivedCategory.instEssSurjCochainComplexIntQ, instEssSurjLightDiagram'LightDiagramToLightFunctor, CategoryTheory.StructuredArrow.essSurj_map₂, CategoryTheory.Reflective.comparison_essSurj, CategoryTheory.StructuredArrow.instEssSurjUnderToUnder, instEssSurjOppositeLeftOp, UnivLE_iff_essSurj, essSurj_comp, CategoryTheory.Join.instEssSurjSumFromSum, CategoryTheory.Localization.Monoidal.instEssSurjLocalizedMonoidalToMonoidalCategory, CategoryTheory.Localization.essSurj_mapComposableArrows, CategoryTheory.ObjectProperty.essSurj_ιOfLE_iff, CategoryTheory.LocalizerMorphism.essSurj_of_hasLeftResolutions, CategoryTheory.Equivalence.essSurjInducedFunctor, CategoryTheory.Coreflective.comparison_essSurj, CategoryTheory.Equivalence.essSurj_inverse

CategoryTheory.PreGaloisCategory

Definitions

Name	Category	Theorems
fiberIsoQuotientStabilizer 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lift_of_continuous 📖	mathematical	—	CategoryTheory.Iso Action FintypeCat FintypeCat.instCategory CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory CategoryTheory.Functor.obj functorToAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory instIsTopologicalGroupAutFunctorFintypeCat instCompactSpaceAutFunctorFintypeCat MulAction.left_quotientAction CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete Action.instHasFiniteCoproducts CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.FintypeCat.hasFiniteColimits has_decomp_quotients hasFiniteCoproducts CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction exists_lift_of_quotient_openSubgroup
exists_lift_of_quotient_openSubgroup 📖	mathematical	—	CategoryTheory.Iso Action FintypeCat FintypeCat.instCategory CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory CategoryTheory.Functor.obj functorToAction Action.FintypeCat.ofMulAction FintypeCat.of HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup OpenSubgroup.toSubgroup instTopologicalSpaceAutFunctorFintypeCat instIsTopologicalGroupAutFunctorFintypeCat instCompactSpaceAutFunctorFintypeCat MulAction.quotient Monoid.toMulAction MulAction.left_quotientAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory instIsTopologicalGroupAutFunctorFintypeCat instCompactSpaceAutFunctorFintypeCat MulAction.left_quotientAction exists_set_ker_evaluation_subset_of_isOpen OneMemClass.one_mem SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass OpenSubgroup.instSubgroupClass OpenSubgroup.isOpen' CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits instHasFiniteLimits Finite.of_fintype nonempty_fiber_pi_of_nonempty_of_finite nonempty_fiber_of_isConnected exists_hom_from_galois_of_fiber_nonempty IsGalois.toIsConnected stabilizer_isOpen continuousSMul_aut_fiber obj_discreteTopology stabilizer_normal_of_isGalois FintypeCat.hom_ext QuotientGroup.leftRel_apply mul_inv_rev Subgroup.Normal.conj_mem Subgroup.inv_mem CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso Action.instIsIsoHomHom Action.Hom.comm CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp surjective_of_nonempty_fiber_of_isConnected FunctorToFintypeCat.naturality Subgroup.quotient_finite_of_isOpen' OpenSubgroup.isOpen Subgroup.subgroupOf_isOpen Subgroup.normal_subgroupOf CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeSingleObjOfFinite CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite
has_decomp_quotients 📖	mathematical	—	CategoryTheory.Iso Action FintypeCat FintypeCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory CategoryTheory.Limits.sigmaObj Action.FintypeCat.ofMulAction FintypeCat.of HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup OpenSubgroup.toSubgroup MulAction.quotient Monoid.toMulAction MulAction.left_quotientAction CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete Action.instHasFiniteCoproducts CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.FintypeCat.hasFiniteColimits CategoryTheory.Discrete.functor	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts CategoryTheory.GaloisCategory.toPreGaloisCategory CategoryTheory.FintypeCat.instGaloisCategoryActionFintypeCat MulAction.left_quotientAction Action.instHasFiniteCoproducts CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.FintypeCat.hasFiniteColimits has_decomp_connected_components' DFunLike.congr_fun Action.Hom.comm CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomCarrierV CategoryTheory.mono_comp CategoryTheory.Limits.MonoCoprod.mono_ι instMonoCoprod Subtype.finite CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom le_bot_iff isOpen_discrete Set.preimage_image_eq continuous_induced_rng Continuous.comp ContinuousSMul.continuous_smul Continuous.prodMk Continuous.fst continuous_id' Continuous.comp' continuous_of_discreteTopology Continuous.snd nonempty_fiber_of_isConnected CategoryTheory.FintypeCat.instPreGaloisCategoryActionFintypeCat CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomCarrierV stabilizer_isOpen

---

← Back to Index