Profinite

📁 Source: Mathlib/RingTheory/Invariant/Profinite.lean

Statistics

Metric	Count
Definitions stabilizerHomSurjectiveAuxFunctor	1
Theorems exists_smul_of_under_eq_of_profinite, isIntegral_of_profinite, stabilizerHomSurjectiveAuxFunctor_aux, stabilizerHom_surjective_of_profinite, instFiniteObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor, instNonemptyObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor	6
Total	7

Algebra.IsInvariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_smul_of_under_eq_of_profinite 📖	mathematical	Ideal.under CommRing.toCommSemiring CommSemiring.toSemiring	Ideal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid Ideal.pointwiseDistribMulAction	—	Subgroup.smulCommClass_left OpenNormalSubgroup.instNormal CategoryTheory.leOfHom QuotientGroup.mk_surjective RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHom.instRingHomClass Ideal.pointwise_smul_eq_comap Ideal.comap_coe Ideal.comap.congr_simp CategoryTheory.types_ext exists_smul_of_under_eq instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient Subgroup.instFiniteQuotientOfContinuousMulOfCompactSpace IsTopologicalGroup.toContinuousMul instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra Ideal.IsPrime.under nonempty_sections_of_finite_cofiltered_system CategoryTheory.isCofilteredOrEmpty_of_directed_ge SemilatticeInf.instIsCodirectedOrder Subtype.finite ProfiniteGrp.comp_apply CategoryTheory.Iso.inv_hom_id Ideal.ext ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one stabilizer_isOpen OneMemClass.one_mem SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass CanLift.prf Subtype.canLift RingHom.ext RingHomClass.toRingHom.congr_simp
isIntegral_of_profinite 📖	mathematical	—	Algebra.IsIntegral CommRing.toRing	—	ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one stabilizer_isOpen OneMemClass.one_mem SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass Subgroup.smulCommClass_left Algebra.IsIntegral.isIntegral isIntegral OpenNormalSubgroup.instNormal instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient Subgroup.instFiniteQuotientOfContinuousMulOfCompactSpace IsTopologicalGroup.toContinuousMul IsIntegral.map Subalgebra.instIsScalarTowerSubtypeMem IsScalarTower.left AlgHom.algHomClass

Ideal.Quotient

Definitions

Name	Category	Theorems
stabilizerHomSurjectiveAuxFunctor 📖	CompOp	2 math math: instFiniteObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor, instNonemptyObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stabilizerHomSurjectiveAuxFunctor_aux 📖	mathematical	OpenNormalSubgroup Preorder.toLE PartialOrder.toPreorder OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup OpenSubgroup.toSubgroup OpenNormalSubgroup.toOpenSubgroup QuotientGroup.Quotient.group OpenNormalSubgroup.instNormal SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Ideal Subalgebra CommRing.toCommSemiring Ring.toSemiring CommRing.toRing Subalgebra.instSetLike FixedPoints.subalgebra DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.mulSemiringAction Subgroup.smulCommClass_left DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MulSemiringAction.toDistribMulAction Algebra.toSMul Subalgebra.toCommSemiring Submodule.instAddCommMonoidWithOne Semiring.toModule Ideal.pointwiseDistribMulAction instMulSemiringActionQuotientSubgroupSubtypeMemSubalgebraSubalgebra Ideal.under Subalgebra.toAlgebra Algebra.id	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike QuotientGroup.map MonoidHom.id	—	OpenNormalSubgroup.instNormal Subgroup.smulCommClass_left QuotientGroup.mk_surjective AlgHomClass.toRingHomClass AlgHom.algHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHom.instRingHomClass Ideal.pointwise_smul_eq_comap Ideal.comap_coe Ideal.comap.congr_simp
stabilizerHom_surjective_of_profinite 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Ideal CommSemiring.toSemiring CommRing.toCommSemiring DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule Ideal.pointwiseDistribMulAction AlgEquiv HasQuotient.Quotient Ideal.instHasQuotient_1 commSemiring semiring algebraOfLiesOver DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Subgroup.toGroup AlgEquiv.aut MonoidHom.instFunLike stabilizerHom	—	nonempty_sections_of_finite_cofiltered_system CategoryTheory.isCofilteredOrEmpty_of_directed_ge SemilatticeInf.instIsCodirectedOrder instFiniteObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor instNonemptyObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor OpenNormalSubgroup.instNormal Ideal.instIsTwoSided_1 CategoryTheory.ConcreteCategory.congr_hom CategoryTheory.Iso.inv_hom_id Ideal.ext ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one stabilizer_isOpen OneMemClass.one_mem SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass Subgroup.smulCommClass_left CanLift.prf Subtype.canLift RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHom.instRingHomClass Ideal.pointwise_smul_eq_comap Ideal.comap_coe RingHom.ext AlgEquiv.ext mk_surjective DFunLike.congr_fun

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiniteObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor 📖	mathematical	—	Finite CategoryTheory.Functor.obj OpenNormalSubgroup Preorder.smallCategory PartialOrder.toPreorder OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup CategoryTheory.types Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor	—	OpenNormalSubgroup.instNormal Ideal.instIsTwoSided_1 AlgHomClass.toRingHomClass AlgHom.algHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Subtype.finite Subgroup.instFiniteSubtypeMem Subgroup.instFiniteQuotientOfContinuousMulOfCompactSpace IsTopologicalGroup.toContinuousMul
instNonemptyObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor 📖	mathematical	—	CategoryTheory.Functor.obj OpenNormalSubgroup Preorder.smallCategory PartialOrder.toPreorder OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup CategoryTheory.types Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor	—	Subgroup.smulCommClass_left Ideal.under_liesOver_of_liesOver IsScalarTower.subalgebra' IsScalarTower.right RingHom.instRingHomClass IsScalarTower.of_algebraMap_eq Ideal.Quotient.exists_algEquiv_fixedPoint_quotient_under Subgroup.instFiniteQuotientOfContinuousMulOfCompactSpace IsTopologicalGroup.toContinuousMul OpenNormalSubgroup.instNormal instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient Ideal.Quotient.isDomain Ideal.instIsTwoSided_1 Ideal.Quotient.instFaithfulSMul Ideal.over_under instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra Ideal.Quotient.stabilizerHom_surjective Ideal.IsPrime.under AlgHom.ext Ideal.Quotient.mk_surjective

---

← Back to Index