Fiber

📁 Source: Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean

Statistics

Metric	Count
Definitions preimageEquivFiber, preimageHomeomorphFiber, preimageOrderIsoFiber, preimageOrderIsoTensorResidueField, primesOverOrderIsoFiber	5
Theorems exists_smul_eq_one_tmul, exists_smul_eq_tmul_one, coe_preimageHomeomorphFiber_apply_asIdeal, coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, coe_preimageOrderIsoFiber_apply_asIdeal, coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, coe_primesOverOrderIsoFiber_apply_asIdeal, coe_primesOverOrderIsoFiber_symm_apply_coe, preimageEquivFiber_apply_asIdeal, preimageEquivFiber_symm_apply_coe, instIsLocalRingTensorProductResidueFieldOfIsLocalHomRingHomAlgebraMap, instLiesOverFiberOfIsPrime	12
Total	17

Ideal.Fiber

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_smul_eq_one_tmul 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.Fiber TensorProduct.instSMul Ideal.ResidueField NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsLocalRing.instCommRingResidueField Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	Ideal.ResidueField.exists_smul_eq_tmul_one map_smul SemilinearMapClass.toMulActionSemiHomClass Algebra.to_smulCommClass IsScalarTower.right NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquiv.symm_apply_apply

Ideal.ResidueField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_smul_eq_tmul_one 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule TensorProduct Ideal.ResidueField NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsLocalRing.instCommRingResidueField Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id TensorProduct.instSMul TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	Algebra.to_smulCommClass IsScalarTower.right RingHom.SurjectiveOnStalks.exists_mul_eq_tmul Ideal.surjectiveOnStalks_residueField Ideal.isPrime_bot IsLocalRing.toNontrivial Field.instIsLocalRing IsDomain.to_noZeroDivisors instIsDomain IsLocalRing.residue_surjective Localization.isLocalization IsLocalization.mk'_surjective Submonoid.mul_mem Algebra.smul_def AlgHom.commutes TensorProduct.smul_tmul TensorProduct.CompatibleSMul.isScalarTower IsScalarTower.left IsLocalRing.instIsScalarTowerResidueField OreLocalization.instIsScalarTower Algebra.algebraMap_eq_smul_one Algebra.TensorProduct.includeRight_apply map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Submonoid.isScalarTower Submonoid.smulCommClass_right smulCommClass_self SMulCommClass.smul_comm Submonoid.smulCommClass_left OreLocalization.instSMulCommClass IsLocalization.smul_mk'_self

PrimeSpectrum

Definitions

Name	Category	Theorems
preimageEquivFiber 📖	CompOp	2 math math: preimageEquivFiber_symm_apply_coe, preimageEquivFiber_apply_asIdeal
preimageHomeomorphFiber 📖	CompOp	2 math math: coe_preimageHomeomorphFiber_apply_asIdeal, coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal
preimageOrderIsoFiber 📖	CompOp	2 math math: coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, coe_preimageOrderIsoFiber_apply_asIdeal
preimageOrderIsoTensorResidueField 📖	CompOp	—
primesOverOrderIsoFiber 📖	CompOp	2 math math: coe_primesOverOrderIsoFiber_apply_asIdeal, coe_primesOverOrderIsoFiber_symm_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_preimageHomeomorphFiber_apply_asIdeal 📖	mathematical	—	SetLike.coe Submodule Ideal.Fiber asIdeal CommRing.toCommSemiring CommSemiring.toSemiring Algebra.TensorProduct.instCommSemiring Ideal.ResidueField Semifield.toCommSemiring Field.toSemifield IsLocalRing.ResidueField.field Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.setLike DFunLike.coe Homeomorph Set.Elem PrimeSpectrum Set.preimage comap algebraMap Set Set.instSingletonSet isPrime instTopologicalSpaceSubtype Set.instMembership zariskiTopology EquivLike.toFunLike Homeomorph.instEquivLike preimageHomeomorphFiber AlgHom TensorProduct DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra AlgHom.funLike Algebra.TensorProduct.lift Ideal.ResidueField.mapₐ Algebra.ofId IsScalarTower.toAlgHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	isPrime
coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal 📖	mathematical	—	SetLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.setLike asIdeal PrimeSpectrum Set Set.instMembership Set.preimage comap algebraMap Set.instSingletonSet DFunLike.coe Homeomorph Ideal.Fiber isPrime Algebra.TensorProduct.instCommSemiring Ideal.ResidueField Semifield.toCommSemiring Field.toSemifield IsLocalRing.ResidueField.field Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id Set.Elem zariskiTopology instTopologicalSpaceSubtype EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm preimageHomeomorphFiber AlgHom TensorProduct DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra AlgHom.funLike Algebra.TensorProduct.includeRight Ideal	—	isPrime
coe_preimageOrderIsoFiber_apply_asIdeal 📖	mathematical	—	SetLike.coe Submodule Ideal.Fiber asIdeal CommRing.toCommSemiring CommSemiring.toSemiring Algebra.TensorProduct.instCommSemiring Ideal.ResidueField Semifield.toCommSemiring Field.toSemifield IsLocalRing.ResidueField.field Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.setLike DFunLike.coe RelIso Set.Elem PrimeSpectrum Set.preimage comap algebraMap Set Set.instSingletonSet isPrime Preorder.toLE PartialOrder.toPreorder instPartialOrder Set.instMembership RelIso.instFunLike preimageOrderIsoFiber AlgHom TensorProduct DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra AlgHom.funLike Algebra.TensorProduct.lift Ideal.ResidueField.mapₐ Algebra.ofId IsScalarTower.toAlgHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	isPrime
coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal 📖	mathematical	—	SetLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.setLike asIdeal PrimeSpectrum Set Set.instMembership Set.preimage comap algebraMap Set.instSingletonSet DFunLike.coe RelIso Ideal.Fiber isPrime Algebra.TensorProduct.instCommSemiring Ideal.ResidueField Semifield.toCommSemiring Field.toSemifield IsLocalRing.ResidueField.field Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id Set.Elem Preorder.toLE PartialOrder.toPreorder instPartialOrder RelIso.instFunLike RelIso.symm preimageOrderIsoFiber AlgHom TensorProduct DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra AlgHom.funLike Algebra.TensorProduct.includeRight Ideal	—	isPrime
coe_primesOverOrderIsoFiber_apply_asIdeal 📖	mathematical	—	SetLike.coe Submodule Ideal.Fiber asIdeal CommRing.toCommSemiring CommSemiring.toSemiring Algebra.TensorProduct.instCommSemiring Ideal.ResidueField Semifield.toCommSemiring Field.toSemifield IsLocalRing.ResidueField.field Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.setLike DFunLike.coe RelIso Set.Elem Ideal Ideal.primesOver PrimeSpectrum Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Set Set.instMembership instPartialOrder RelIso.instFunLike primesOverOrderIsoFiber Set.preimage Equiv comap algebraMap Set.instSingletonSet EquivLike.toFunLike Equiv.instEquivLike RelIso.toEquiv AlgHom TensorProduct DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra AlgHom.funLike Algebra.TensorProduct.lift Ideal.ResidueField.mapₐ Algebra.ofId IsScalarTower.toAlgHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
coe_primesOverOrderIsoFiber_symm_apply_coe 📖	mathematical	—	SetLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.setLike Ideal Set Set.instMembership Ideal.primesOver DFunLike.coe RelIso PrimeSpectrum Ideal.Fiber Algebra.TensorProduct.instCommSemiring Ideal.ResidueField Semifield.toCommSemiring Field.toSemifield IsLocalRing.ResidueField.field Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id Set.Elem Preorder.toLE PartialOrder.toPreorder instPartialOrder Submodule.instPartialOrder RelIso.instFunLike RelIso.symm primesOverOrderIsoFiber Set.preimage AlgHom TensorProduct DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra AlgHom.funLike Algebra.TensorProduct.includeRight asIdeal	—	—
preimageEquivFiber_apply_asIdeal 📖	mathematical	—	asIdeal Ideal.Fiber CommRing.toCommSemiring Algebra.TensorProduct.instCommSemiring Ideal.ResidueField Semifield.toCommSemiring Field.toSemifield IsLocalRing.ResidueField.field Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id DFunLike.coe Equiv Set.Elem PrimeSpectrum Set.preimage comap algebraMap Set Set.instSingletonSet isPrime EquivLike.toFunLike Equiv.instEquivLike preimageEquivFiber RingHom.ker Set.instMembership RingHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.toModule Algebra.TensorProduct.instSemiring RingHom.instFunLike AlgHom.toRingHom Algebra.TensorProduct.leftAlgebra Algebra.TensorProduct.lift Ideal.ResidueField.mapₐ Algebra.ofId IsScalarTower.toAlgHom	—	isPrime
preimageEquivFiber_symm_apply_coe 📖	mathematical	—	PrimeSpectrum CommRing.toCommSemiring Set Set.instMembership Set.preimage comap algebraMap CommSemiring.toSemiring Set.instSingletonSet DFunLike.coe Equiv Ideal.Fiber asIdeal isPrime Algebra.TensorProduct.instCommSemiring Ideal.ResidueField Semifield.toCommSemiring Field.toSemifield IsLocalRing.ResidueField.field Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm preimageEquivFiber AlgHom.toRingHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra Algebra.TensorProduct.includeRight	—	isPrime

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLocalRingTensorProductResidueFieldOfIsLocalHomRingHomAlgebraMap 📖	mathematical	—	IsLocalRing TensorProduct CommRing.toCommSemiring IsLocalRing.ResidueField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsLocalRing.instCommRingResidueField Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field IsLocalRing.ResidueField.algebra Algebra.id CommSemiring.toSemiring Algebra.TensorProduct.instSemiring	—	Algebra.to_smulCommClass TensorProduct.isScalarTower_left IsScalarTower.right Ideal.Quotient.isScalarTower Equiv.nontrivial_congr Ideal.Quotient.nontrivial_iff LT.lt.ne LE.le.trans_lt List.TFAE.out RingHom.instRingHomClass IsLocalRing.local_hom_TFAE Ne.lt_top Ideal.IsMaximal.ne_top IsLocalRing.maximalIdeal.isMaximal IsLocalRing.of_surjective' TensorProduct.mk_surjective IsLocalRing.residue_surjective
instLiesOverFiberOfIsPrime 📖	mathematical	—	Ideal.LiesOver CommRing.toCommSemiring Ideal.Fiber Algebra.TensorProduct.instSemiring Ideal.ResidueField DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id Algebra.TensorProduct.instAlgebra	—	Ideal.LiesOver.trans Algebra.to_smulCommClass TensorProduct.isScalarTower_left IsScalarTower.right Ideal.instLiesOverBotOfIsPrime instLiesOverResidueFieldBotIdeal

---

← Back to Index