Profinite

📁 Source: Mathlib/FieldTheory/Galois/Profinite.lean

Statistics

Metric	Count
Definitions finGaloisGroup, algEquivToLimit, asProfiniteGaloisGroupFunctor, continuousMulEquivToLimit, limitToAlgEquiv, mulEquivToLimit, profiniteGalGrp, profiniteGalGrpIsoLimit, proj, finGaloisGroupFunctor, finGaloisGroupMap	11
Theorems algEquivToLimit_continuous, finGaloisGroupFunctor_map_proj_eq_proj, instCompactSpaceAlgEquivOfIsGalois, isOpen_mulEquivToLimit_image_fixingSubgroup, krullTopology_mem_nhds_one_iff_of_isGalois, limitToAlgEquiv_apply, limitToAlgEquiv_symm_apply, mk_toAlgEquivAux, mulEquivToLimit_symm_continuous, proj_adjoin_singleton_val, proj_of_le, restrictNormalHom_continuous, toAlgEquivAux_eq_liftNormal, toAlgEquivAux_eq_proj_of_mem, map_comp, map_id	16
Total	27

FiniteGaloisIntermediateField

Definitions

Name	Category	Theorems
finGaloisGroup 📖	CompOp	2 math math: finGaloisGroupMap.map_id, finGaloisGroupMap.map_comp

InfiniteGalois

Definitions

Name	Category	Theorems
algEquivToLimit 📖	CompOp	1 math math: algEquivToLimit_continuous
asProfiniteGaloisGroupFunctor 📖	CompOp	10 math math: toAlgEquivAux_eq_proj_of_mem, mulEquivToLimit_symm_continuous, isOpen_mulEquivToLimit_image_fixingSubgroup, proj_adjoin_singleton_val, toAlgEquivAux_eq_liftNormal, finGaloisGroupFunctor_map_proj_eq_proj, mk_toAlgEquivAux, proj_of_le, algEquivToLimit_continuous, limitToAlgEquiv_symm_apply
continuousMulEquivToLimit 📖	CompOp	—
limitToAlgEquiv 📖	CompOp	2 math math: limitToAlgEquiv_apply, limitToAlgEquiv_symm_apply
mulEquivToLimit 📖	CompOp	2 math math: mulEquivToLimit_symm_continuous, isOpen_mulEquivToLimit_image_fixingSubgroup
profiniteGalGrp 📖	CompOp	—
profiniteGalGrpIsoLimit 📖	CompOp	—
proj 📖	CompOp	6 math math: toAlgEquivAux_eq_proj_of_mem, proj_adjoin_singleton_val, toAlgEquivAux_eq_liftNormal, finGaloisGroupFunctor_map_proj_eq_proj, mk_toAlgEquivAux, proj_of_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algEquivToLimit_continuous 📖	mathematical	—	Continuous AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str ProfiniteGrp.toProfinite ProfiniteGrp.limit Opposite FiniteGaloisIntermediateField CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder FiniteGaloisIntermediateField.instPartialOrder asProfiniteGaloisGroupFunctor krullTopology instTopologicalSpaceSubtype Subgroup Pi.group CategoryTheory.Functor.obj ProfiniteGrp instCategoryProfiniteGrp ProfiniteGrp.group SetLike.instMembership Subgroup.instSetLike ProfiniteGrp.limitConePtAux Pi.topologicalSpace DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut Subgroup.toGroup MonoidHom.instFunLike algEquivToLimit	—	continuous_induced_rng continuous_pi IsScalarTower.left IntermediateField.isScalarTower_mid' IsGalois.to_normal FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateField DiscreteTopology.eq_bot krullTopology_discreteTopology_of_finiteDimensional FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateField restrictNormalHom_continuous
finGaloisGroupFunctor_map_proj_eq_proj 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite FiniteGaloisIntermediateField CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder FiniteGaloisIntermediateField.instPartialOrder FiniteGrp FiniteGrp.instCategory finGaloisGroupFunctor Opposite.op CategoryTheory.ConcreteCategory.hom MonoidHom GrpCat.carrier FiniteGrp.toGrp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid GrpCat.str MonoidHom.instFunLike FiniteGrp.instConcreteCategoryMonoidHomCarrierToGrp CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str ProfiniteGrp.toProfinite ProfiniteGrp.limit asProfiniteGaloisGroupFunctor AlgEquiv IntermediateField SetLike.instMembership IntermediateField.instSetLike FiniteGaloisIntermediateField.toIntermediateField Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Module.toDistribMulAction Algebra.toModule Subgroup.toGroup Pi.group ProfiniteGrp instCategoryProfiniteGrp ProfiniteGrp.group ProfiniteGrp.limitConePtAux AlgEquiv.aut proj	—	Subtype.prop
instCompactSpaceAlgEquivOfIsGalois 📖	mathematical	—	CompactSpace AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring krullTopology	—	Homeomorph.compactSpace ProfiniteGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux
isOpen_mulEquivToLimit_image_fixingSubgroup 📖	mathematical	—	IsOpen TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str ProfiniteGrp.toProfinite ProfiniteGrp.limit Opposite FiniteGaloisIntermediateField CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder FiniteGaloisIntermediateField.instPartialOrder asProfiniteGaloisGroupFunctor instTopologicalSpaceSubtype Subgroup Pi.group CategoryTheory.Functor.obj ProfiniteGrp instCategoryProfiniteGrp ProfiniteGrp.group SetLike.instMembership Subgroup.instSetLike ProfiniteGrp.limitConePtAux Pi.topologicalSpace Set.image AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike mulEquivToLimit SetLike.coe IntermediateField.fixingSubgroup FiniteGaloisIntermediateField.toIntermediateField	—	Set.ext MulEquiv.surjective Set.image_congr EquivLike.toEmbeddingLike IsScalarTower.left IntermediateField.isScalarTower_mid' IsGalois.to_normal FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateField FiniteGaloisIntermediateField.mem_fixingSubgroup_iff isOpen_induced Continuous.isOpen_preimage continuous_apply
krullTopology_mem_nhds_one_iff_of_isGalois 📖	mathematical	—	Set AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Filter Filter.instMembership nhds krullTopology InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid AlgEquiv.aut Set.instHasSubset SetLike.coe Subgroup Subgroup.instSetLike IntermediateField.fixingSubgroup FiniteGaloisIntermediateField.toIntermediateField	—	IsScalarTower.left krullTopology_mem_nhds_one_iff_of_normal IsGalois.to_normal IntermediateField.isSeparable_tower_bot IsGalois.to_isSeparable FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateField FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateField
limitToAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.instFunLike limitToAlgEquiv	—	—
limitToAlgEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.instFunLike AlgEquiv.symm limitToAlgEquiv TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str ProfiniteGrp.toProfinite ProfiniteGrp.limit Opposite FiniteGaloisIntermediateField CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder FiniteGaloisIntermediateField.instPartialOrder asProfiniteGaloisGroupFunctor Subgroup.inv Pi.group CategoryTheory.Functor.obj ProfiniteGrp instCategoryProfiniteGrp ProfiniteGrp.group ProfiniteGrp.limitConePtAux	—	—
mk_toAlgEquivAux 📖	mathematical	IntermediateField SetLike.instMembership IntermediateField.instSetLike FiniteGaloisIntermediateField.toIntermediateField	DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Module.toDistribMulAction Algebra.toModule AlgEquiv.instFunLike MonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str ProfiniteGrp.toProfinite ProfiniteGrp.limit Opposite FiniteGaloisIntermediateField CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder FiniteGaloisIntermediateField.instPartialOrder asProfiniteGaloisGroupFunctor MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Pi.group CategoryTheory.Functor.obj ProfiniteGrp instCategoryProfiniteGrp ProfiniteGrp.group ProfiniteGrp.limitConePtAux AlgEquiv.aut MonoidHom.instFunLike proj	—	IsScalarTower.left toAlgEquivAux_eq_proj_of_mem
mulEquivToLimit_symm_continuous 📖	mathematical	—	Continuous TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str ProfiniteGrp.toProfinite ProfiniteGrp.limit Opposite FiniteGaloisIntermediateField CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder FiniteGaloisIntermediateField.instPartialOrder asProfiniteGaloisGroupFunctor AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring instTopologicalSpaceSubtype Subgroup Pi.group CategoryTheory.Functor.obj ProfiniteGrp instCategoryProfiniteGrp ProfiniteGrp.group SetLike.instMembership Subgroup.instSetLike ProfiniteGrp.limitConePtAux Pi.topologicalSpace krullTopology DFunLike.coe MulEquiv Subgroup.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm mulEquivToLimit	—	continuous_of_continuousAt_one Subgroup.instIsTopologicalGroupSubtypeMem Pi.topologicalGroup ProfiniteGrp.topologicalGroup IsTopologicalGroup.toContinuousMul instIsTopologicalGroupAlgEquiv MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass continuousAt_def map_one MonoidHomClass.toOneHomClass Equiv.image_eq_preimage_symm Set.image_congr mem_nhds_iff isOpen_mulEquivToLimit_image_fixingSubgroup EquivLike.toEmbeddingLike Set.image_subset_iff Set.image_mono
proj_adjoin_singleton_val 📖	mathematical	IntermediateField SetLike.instMembership IntermediateField.instSetLike FiniteGaloisIntermediateField.toIntermediateField	FiniteGaloisIntermediateField.adjoin Set Set.instSingletonSet Finite.of_fintype Set.Elem Set.fintypeSingleton DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Module.toDistribMulAction Algebra.toModule AlgEquiv.instFunLike MonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str ProfiniteGrp.toProfinite ProfiniteGrp.limit Opposite FiniteGaloisIntermediateField CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder FiniteGaloisIntermediateField.instPartialOrder asProfiniteGaloisGroupFunctor MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Pi.group CategoryTheory.Functor.obj ProfiniteGrp instCategoryProfiniteGrp ProfiniteGrp.group ProfiniteGrp.limitConePtAux AlgEquiv.aut MonoidHom.instFunLike proj Preorder.toLE FiniteGaloisIntermediateField.adjoin_simple_le_iff	—	Finite.of_fintype proj_of_le FiniteGaloisIntermediateField.adjoin_simple_le_iff
proj_of_le 📖	mathematical	FiniteGaloisIntermediateField Preorder.toLE PartialOrder.toPreorder FiniteGaloisIntermediateField.instPartialOrder	IntermediateField SetLike.instMembership IntermediateField.instSetLike FiniteGaloisIntermediateField.toIntermediateField DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Module.toDistribMulAction Algebra.toModule AlgEquiv.instFunLike MonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str ProfiniteGrp.toProfinite ProfiniteGrp.limit Opposite CategoryTheory.Category.opposite Preorder.smallCategory asProfiniteGaloisGroupFunctor MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Pi.group CategoryTheory.Functor.obj ProfiniteGrp instCategoryProfiniteGrp ProfiniteGrp.group ProfiniteGrp.limitConePtAux AlgEquiv.aut MonoidHom.instFunLike proj	—	IsScalarTower.left finGaloisGroupFunctor_map_proj_eq_proj SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IsScalarTower.of_algebraMap_eq IsGalois.to_normal AlgEquiv.restrictNormal_commutes
restrictNormalHom_continuous 📖	mathematical	—	Continuous AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.toField IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Module.toDistribMulAction Algebra.toModule krullTopology DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut MonoidHom.instFunLike AlgEquiv.restrictNormalHom IntermediateField.instAlgebraSubtypeMem IntermediateField.isScalarTower_mid'	—	IsScalarTower.left continuous_of_continuousAt_one instIsTopologicalGroupAlgEquiv IsTopologicalGroup.toContinuousMul MonoidHom.instMonoidHomClass IntermediateField.isScalarTower_mid' continuousAt_def krullTopology_mem_nhds_one_iff map_one MonoidHomClass.toOneHomClass Module.Finite.equiv IntermediateField.isScalarTower mem_nhds_iff AlgEquiv.restrictNormal_commutes SetLike.coe_eq_coe IntermediateField.mem_lift IntermediateField.fixingSubgroup_isOpen
toAlgEquivAux_eq_liftNormal 📖	mathematical	IntermediateField SetLike.instMembership IntermediateField.instSetLike FiniteGaloisIntermediateField.toIntermediateField	DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.instFunLike AlgEquiv.liftNormal IntermediateField.toField IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Module.toDistribMulAction Algebra.toModule MonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str ProfiniteGrp.toProfinite ProfiniteGrp.limit Opposite FiniteGaloisIntermediateField CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder FiniteGaloisIntermediateField.instPartialOrder asProfiniteGaloisGroupFunctor MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Pi.group CategoryTheory.Functor.obj ProfiniteGrp instCategoryProfiniteGrp ProfiniteGrp.group ProfiniteGrp.limitConePtAux AlgEquiv.aut MonoidHom.instFunLike proj IntermediateField.instAlgebraSubtypeMem IntermediateField.isScalarTower_mid' IsGalois.to_normal	—	IsScalarTower.left IntermediateField.isScalarTower_mid' IsGalois.to_normal toAlgEquivAux_eq_proj_of_mem AlgEquiv.liftNormal_commutes
toAlgEquivAux_eq_proj_of_mem 📖	mathematical	IntermediateField SetLike.instMembership IntermediateField.instSetLike FiniteGaloisIntermediateField.toIntermediateField	DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Module.toDistribMulAction Algebra.toModule AlgEquiv.instFunLike MonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str ProfiniteGrp.toProfinite ProfiniteGrp.limit Opposite FiniteGaloisIntermediateField CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder FiniteGaloisIntermediateField.instPartialOrder asProfiniteGaloisGroupFunctor MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Pi.group CategoryTheory.Functor.obj ProfiniteGrp instCategoryProfiniteGrp ProfiniteGrp.group ProfiniteGrp.limitConePtAux AlgEquiv.aut MonoidHom.instFunLike proj	—	proj_adjoin_singleton_val

(root)

Definitions

Name	Category	Theorems
finGaloisGroupFunctor 📖	CompOp	1 math math: InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj
finGaloisGroupMap 📖	CompOp	2 math math: finGaloisGroupMap.map_id, finGaloisGroupMap.map_comp

finGaloisGroupMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_comp 📖	mathematical	—	finGaloisGroupMap CategoryTheory.CategoryStruct.comp Opposite FiniteGaloisIntermediateField CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Preorder.smallCategory PartialOrder.toPreorder FiniteGaloisIntermediateField.instPartialOrder FiniteGrp FiniteGrp.instCategory FiniteGaloisIntermediateField.finGaloisGroup Opposite.unop	—	IsScalarTower.left LE.le.trans IsScalarTower.of_algebraMap_eq' SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass CategoryTheory.ConcreteCategory.ext IsScalarTower.AlgEquiv.restrictNormalHom_comp IsGalois.to_normal
map_id 📖	mathematical	—	finGaloisGroupMap CategoryTheory.CategoryStruct.id Opposite FiniteGaloisIntermediateField CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Preorder.smallCategory PartialOrder.toPreorder FiniteGaloisIntermediateField.instPartialOrder FiniteGrp FiniteGrp.instCategory FiniteGaloisIntermediateField.finGaloisGroup Opposite.unop	—	CategoryTheory.ConcreteCategory.ext AlgEquiv.restrictNormalHom_id

---

← Back to Index