AtPrime 📖 | CompOp | 145 mathmath: Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective, MaximalSpectrum.mapPiLocalization_bijective, PrimeSpectrum.preimageEquivFiber_symm_apply_coe, PrimeSpectrum.residueField_specComap, Ideal.exists_mem_span_singleton_map_residueField_eq, Ideal.ker_algebraMap_residueField, Polynomial.fiberEquivQuotient_tmul, AtPrime.mapPiEvalRingHom_bijective, Module.rankAtStalk_eq, instLiesOverFiberOfIsPrime, MaximalSpectrum.toPiLocalization_apply_apply, localRingHom_mk', instIsAlgebraicResidueFieldOfIsIntegral, Ideal.algebraMap_quotient_residueField_mk, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, instIsScalarTowerAtPrimeFractionRing_1, instIsFractionRingAtPrimeFractionRing, Algebra.QuasiFinite.instResidueField, localRingHom_to_map, Module.associatedPrimes.mem_associatePrimes_localizedModule_atPrime_of_mem_associated_primes, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Algebra.instFiniteResidueFieldOfQuasiFiniteAt, localRingHom_injective_of_primesOver_eq_singleton, Algebra.WeaklyQuasiFiniteAt.finite_residueField, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, instIsLocalHomAtPrimeRingHomAlgebraMap, PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal, MaximalSpectrum.mapPiLocalization_naturality, AlgebraicGeometry.stalkwise_SpecMap_iff, AtPrime.eq_maximalIdeal_iff_comap_eq, PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, instEssFiniteTypeResidueField_1, AtPrime.isDedekindDomain, AlgebraicGeometry.StructureSheaf.comap_apply, Ideal.Fiber.lift_residueField_surjective, Ideal.algebraMap_residueField_surjective, IsLocalization.instIsScalarTowerLocalizationAtPrime, IsFractionRing.instAtPrimeFractionRing, Ideal.ResidueField.ringHom_ext_iff, instIsSeparableResidueFieldOfQuotientIdeal, Ideal.surjectiveOnStalks_residueField, PrimeSpectrum.preimageEquivFiber_apply_asIdeal, Algebra.WeaklyQuasiFiniteAt.finite_locoalization, PrimeSpectrum.mem_image_comap_basicOpen, AlgHom.IsArithFrobAt.localize_algebraMap, Ideal.ResidueField.liftₐ_comp_toAlgHom, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, localRingHom_id, instIsScalarTowerAtPrimeFractionRing, instIsAlgebraicQuotientIdealResidueField, AtPrime.mapPiEvalRingHom_comp_algebraMap, Algebra.QuasiFinite.finite_fiber, Algebra.QuasiFinite.instFiniteResidueField, MaximalSpectrum.mapPiLocalization_id, Module.rankAtStalk_eq_finrank_tensorProduct, Ideal.ResidueField.map_algebraMap, algebraMap_mk, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom_assoc, Ideal.ResidueField.exists_smul_eq_tmul_one, AtPrime.comap_maximalIdeal, Algebra.isUnramifiedAt_iff_map_eq, finite_of_primesOver_eq_singleton, localAlgHom_apply, PrimeSpectrum.residueField_comap, Algebra.instFiniteResidueFieldOfIsUnramifiedAt, RingHom.SurjectiveOnStalks.residueFieldMap_bijective, RingHom.surjective_localRingHom_of_surjective, PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization, Algebra.IsUnramifiedAt.not_minpoly_sq_dvd, Algebra.instIsSeparableResidueFieldOfIsUnramifiedAt, instLiesOverResidueFieldBotIdeal, IsDedekindDomainDvr.is_dvr_at_nonzero_prime, PrimeSpectrum.piLocalizationToMaximal_surjective, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, RingHom.HoldsForLocalization.localRingHom, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, instFlatAtPrime, instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, AlgebraicGeometry.stalkwise_Spec_map_iff, instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, instEssFiniteTypeResidueField, Ideal.ResidueField.algHom_ext_iff, Ideal.ResidueField.lift_algebraMap, MaximalSpectrum.mapPiLocalization_comp, IsLocalization.instIsScalarTowerAtPrimeFractionRing, isNilpotent_tensor_residueField_iff, AtPrime.instIsScalarTower_1, Algebra.weaklyQuasiFiniteAt_iff, AtPrime.instIsScalarTower, PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal, Module.mem_support_iff_nontrivial_residueField_tensorProduct, instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, AlgHom.IsArithFrobAt.isArithFrobAt_localize, Module.associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes, instFiniteResidueField, Ideal.injective_algebraMap_quotient_residueField, RingHom.Flat.localRingHom, instFaithfulSMulAtPrimeOfNoZeroDivisors, instIsScalarTowerQuotientIdealResidueField, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, MaximalSpectrum.toPiLocalization_injective, Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top, RingHom.SurjectiveOnStalks.localRingHom_surjective, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, localRingHom_bijective_of_saturated_inf_eq_top, Algebra.instFormallyUnramifiedAtPrimeOfIsUnramifiedAt, MaximalSpectrum.toPiLocalization_not_surjective_of_infinite, PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, IsLocalization.isLocalization_atPrime_localization_atPrime, localRingHom_comp, PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, isLocalHom_localRingHom, PrimeSpectrum.piLocalizationToMaximal_bijective, localRingHom_bijective_of_not_conductor_le, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, Polynomial.residueFieldMapCAlgEquiv_symm_X, Module.mem_freeLocus, Algebra.isSeparable_residueField_iff, Ideal.algebraMap_residueField_eq_zero, Ideal.bijective_algebraMap_quotient_residueField, AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom, Ideal.ResidueField.liftₐ_algebraMap, Algebra.QuasiFinite.instIsArtinianRingFiber, PrimeSpectrum.maximalSpectrumToPiLocalization_surjective_of_discreteTopology, RingHom.surjectiveOnStalks_iff_forall_maximal, AlgebraicGeometry.localRingHom_comp_stalkIso, AtPrime.map_eq_maximalIdeal, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso, Polynomial.residueFieldMapCAlgEquiv_algebraMap, instIsIntegralAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Ideal.Fiber.exists_smul_eq_one_tmul, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom, Ideal.ResidueField.mapₐ_apply, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply, PrimeSpectrum.nontrivial_iff_mem_rangeComap, IsLocalization.isDomain_of_local_atPrime, AtPrime.mapPiEvalRingHom_algebraMap_apply, Polynomial.residueFieldMapCAlgEquiv_symm_C, RingHom.surjective_localRingHom_iff, instIsFractionRingQuotientIdealResidueField
|