KrullTopology

📁 Source: Mathlib/FieldTheory/KrullTopology.lean

Statistics

Metric	Count
Definitions finiteExts, fixedByFinite, galBasis, galGroupBasis, krullTopology	5
Theorems finrank_eq_fixingSubgroup_index, fixingSubgroup_isClosed, fixingSubgroup_isOpen, map_fixingSubgroup, map_fixingSubgroup_index, instIsTopologicalGroupAlgEquiv, instTotallySeparatedSpaceAlgEquivOfIsIntegral, krullTopology_discreteTopology_of_finiteDimensional, krullTopology_isTotallySeparated, krullTopology_mem_nhds_one_iff, krullTopology_mem_nhds_one_iff_of_normal, krullTopology_t2, mem_galBasis_iff, stabilizer_isOpen_of_isIntegral, top_fixedByFinite	15
Total	20

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_eq_fixingSubgroup_index 📖	mathematical	—	Module.finrank IntermediateField SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toField module' Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Algebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Subgroup.index AlgEquiv AlgEquiv.aut fixingSubgroup	—	IsScalarTower.left fieldRange_val AlgHom.fieldRange_le_normalClosure isScalarTower Module.finrank_mul_finrank isScalarTower_mid' commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass Module.Free.of_divisionRing LinearEquiv.finrank_eq LT.lt.ne' Finite.card_pos Subgroup.instFiniteSubtypeMem Finite.algEquiv Finite.algHom normalClosure.is_finiteDimensional instIsDomain One.instNonempty Subgroup.index_mul_card IsGalois.card_aut_eq_finrank IsGalois.normalClosure IsGalois.card_fixingSubgroup_eq_finrank map_fixingSubgroup_index normalClosure.normal IsGalois.to_normal lift_restrict Module.finrank_of_infinite_dimensional exists_lt_finrank_of_infinite_dimensional isAlgebraic_tower_bot Algebra.IsSeparable.isAlgebraic IsGalois.to_isSeparable RingHomInvPair.ids LinearEquiv.finiteDimensional LE.le.not_gt Subgroup.index_antitone fixingSubgroup_le lift_le
fixingSubgroup_isClosed 📖	mathematical	—	IsClosed AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring krullTopology SetLike.coe Subgroup AlgEquiv.aut Subgroup.instSetLike fixingSubgroup	—	IsScalarTower.left OpenSubgroup.isClosed IsTopologicalGroup.toContinuousMul instIsTopologicalGroupAlgEquiv fixingSubgroup_isOpen
fixingSubgroup_isOpen 📖	mathematical	—	IsOpen AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring krullTopology SetLike.coe Subgroup AlgEquiv.aut Subgroup.instSetLike fixingSubgroup	—	IsScalarTower.left GroupFilterBasis.mem_nhds_one Subgroup.isOpen_of_mem_nhds IsTopologicalGroup.toContinuousMul instIsTopologicalGroupAlgEquiv
map_fixingSubgroup 📖	mathematical	—	fixingSubgroup map IsScalarTower.toAlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subgroup.comap AlgEquiv AlgEquiv.aut AlgEquiv.restrictNormalHom	—	Subgroup.ext RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing AlgEquiv.restrictNormal_commutes
map_fixingSubgroup_index 📖	mathematical	—	Subgroup.index AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.aut fixingSubgroup map IsScalarTower.toAlgHom	—	map_fixingSubgroup Subgroup.index_comap_of_surjective AlgEquiv.restrictNormalHom_surjective

(root)

Definitions

Name	Category	Theorems
finiteExts 📖	CompOp	—
fixedByFinite 📖	CompOp	2 math math: top_fixedByFinite, mem_galBasis_iff
galBasis 📖	CompOp	1 math math: mem_galBasis_iff
galGroupBasis 📖	CompOp	1 math math: Field.absoluteGaloisGroup.commutator_closure_isNormal
krullTopology 📖	CompOp	21 math math: InfiniteGalois.isOpen_and_normal_iff_finite_and_isGalois, InfiniteGalois.normalAutEquivQuotient_apply, InfiniteGalois.krullTopology_mem_nhds_one_iff_of_isGalois, InfiniteGalois.fixingSubgroup_fixedField, InfiniteGalois.mulEquivToLimit_symm_continuous, instTotallySeparatedSpaceAlgEquivOfIsIntegral, InfiniteGalois.instCompactSpaceAlgEquivOfIsGalois, IntermediateField.fixingSubgroup_isClosed, krullTopology_isTotallySeparated, instIsTopologicalGroupAlgEquiv, stabilizer_isOpen_of_isIntegral, InfiniteGalois.isOpen_iff_finite, InfiniteGalois.restrictNormalHom_continuous, krullTopology_mem_nhds_one_iff, krullTopology_mem_nhds_one_iff_of_normal, IntermediateField.fixingSubgroup_isOpen, krullTopology_discreteTopology_of_finiteDimensional, InfiniteGalois.algEquivToLimit_continuous, krullTopology_t2, InfiniteGalois.fixingSubgroup_isClosed, cyclotomicCharacter.continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsTopologicalGroupAlgEquiv 📖	mathematical	—	IsTopologicalGroup AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring krullTopology AlgEquiv.aut	—	GroupFilterBasis.isTopologicalGroup
instTotallySeparatedSpaceAlgEquivOfIsIntegral 📖	mathematical	—	TotallySeparatedSpace AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring krullTopology	—	totallySeparatedSpace_iff_exists_isClopen inv_mul_eq_one DFunLike.exists_ne IsClosed.leftCoset IsTopologicalGroup.toContinuousMul instIsTopologicalGroupAlgEquiv IntermediateField.fixingSubgroup_isClosed IntermediateField.adjoin.finiteDimensional Algebra.IsIntegral.isIntegral IsOpen.leftCoset IntermediateField.fixingSubgroup_isOpen Submonoid.one_mem' mul_one IntermediateField.mem_adjoin_simple_self
krullTopology_discreteTopology_of_finiteDimensional 📖	mathematical	—	DiscreteTopology AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring krullTopology	—	discreteTopology_iff_isOpen_singleton_one IsTopologicalGroup.toContinuousMul instIsTopologicalGroupAlgEquiv IntermediateField.fixingSubgroup_top IntermediateField.fixingSubgroup_isOpen IntermediateField.finiteDimensional_left
krullTopology_isTotallySeparated 📖	mathematical	—	IsTotallySeparated AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring krullTopology Set.univ	—	totallySeparatedSpace_iff instTotallySeparatedSpaceAlgEquivOfIsIntegral
krullTopology_mem_nhds_one_iff 📖	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 FiniteDimensional IntermediateField SetLike.instMembership IntermediateField.instSetLike Field.toDivisionRing Ring.toAddCommGroup DivisionRing.toRing IntermediateField.toField IntermediateField.module' DivisionRing.toDivisionSemiring Algebra.toSMul CommSemiring.toSemiring Algebra.id Algebra.toModule 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 Set.instHasSubset SetLike.coe Subgroup Subgroup.instSetLike IntermediateField.fixingSubgroup	—	IsScalarTower.left GroupFilterBasis.nhds_one_eq
krullTopology_mem_nhds_one_iff_of_normal 📖	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 FiniteDimensional IntermediateField SetLike.instMembership IntermediateField.instSetLike Field.toDivisionRing Ring.toAddCommGroup DivisionRing.toRing IntermediateField.toField IntermediateField.module' DivisionRing.toDivisionSemiring Algebra.toSMul CommSemiring.toSemiring Algebra.id Algebra.toModule 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 Normal IntermediateField.algebra' Set.instHasSubset SetLike.coe Subgroup Subgroup.instSetLike IntermediateField.fixingSubgroup	—	IsScalarTower.left krullTopology_mem_nhds_one_iff normalClosure.is_finiteDimensional normalClosure.normal le_trans IntermediateField.fixingSubgroup_antitone IntermediateField.le_normalClosure
krullTopology_t2 📖	mathematical	—	T2Space AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring krullTopology	—	DFunLike.exists_ne AlgEquiv.apply_symm_apply IsScalarTower.left IntermediateField.adjoin.finiteDimensional Algebra.IsIntegral.isIntegral GroupFilterBasis.mem_nhds_one mem_nhds_iff IsOpen.leftCoset IsTopologicalGroup.toContinuousMul instIsTopologicalGroupAlgEquiv mul_one Set.disjoint_left Subgroup.mul_mem Subgroup.inv_mem IntermediateField.subset_adjoin Set.mem_singleton IntermediateField.mem_fixingSubgroup_iff mul_inv_eq_iff_eq_mul mul_assoc eq_inv_mul_iff_mul_eq
mem_galBasis_iff 📖	mathematical	—	Set AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring FilterBasis instMembershipSetFilterBasis galBasis Set.instMembership Set.image Subgroup AlgEquiv.aut Subsemigroup.carrier MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Submonoid.toSubsemigroup Subgroup.toSubmonoid fixedByFinite	—	—
stabilizer_isOpen_of_isIntegral 📖	mathematical	—	IsOpen AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring krullTopology SetLike.coe Subgroup AlgEquiv.aut Subgroup.instSetLike MulAction.stabilizer DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction AlgEquiv.applyMulSemiringAction	—	IsScalarTower.left IntermediateField.adjoin.finiteDimensional Algebra.IsIntegral.isIntegral Subgroup.ext IntermediateField.forall_mem_adjoin_smul_eq_self_iff AlgEquiv.apply_smulCommClass' IntermediateField.fixingSubgroup_isOpen
top_fixedByFinite 📖	mathematical	—	Subgroup AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.aut Set Set.instMembership fixedByFinite Top.top Subgroup.instTop	—	IntermediateField.instFiniteSubtypeMemBot IntermediateField.fixingSubgroup_bot

---

← Back to Index