← all areas

Namespace Ideal 94 theorems

— 92 · IsMaximal 2

directly in Ideal 92

• Primes of finite ℤ-algebras as kernels of ℤ̄-valued characters Ideal.exists_ringHom_integralClosure_ker_eq 0 below · cited by 1 · depth 8
• Wiebe's lemma on colon ideals of (f)=g· x Ideal.colon_span_eq_sup_span_det_of_isWeaklyRegular 0 below · cited by 2 · depth 10
• Maximal ideals of finite torsion-free ℤ-algebras lift to ℤ̄ Ideal.exists_ringHom_integralClosure_comap_eq_of_isMaximal 0 below · cited by 1 · depth 11
• Linear growth of #(R/I^m) for R finite over ℤ Ideal.card_quotient_pow_hilbertSamuel_linear_of_moduleFinite 1 below · cited by 2 · depth 12
• Uniform bound on I^m-torsion in R/q^mR Ideal.exists_natCard_torsionBySet_quotient_span_natCast_pow_le_natCard_quotient_pow_mul_pow_of_moduleFinite 4 below · cited by 2 · depth 12
• Uniform index bound for ideals of a reduced ℤ-order Ideal.exists_forall_natCard_quotient_le_mul_natCard_torsionBySet_of_isReduced 3 below · cited by 1 · depth 14
• Inertia of Qⁱ⁺¹ as image of a lower ramification group Ideal.inertia_pow_succ_eq_map_lowerRamificationGroup_of_dense 0 below · cited by 6 · depth 14
• Decomposition subring: e(P∩ C∣𝔭)=f=1 Ideal.ramificationIdx_and_inertiaDeg_under_eq_one_of_isGaloisGroup_stabilizer 0 below · cited by 2 · depth 14
• Norm of a local equation generates the image maximal ideal Ideal.span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing 4 below · cited by 1 · depth 14
• Frobenius conjugation raises the tame character to the q-th power Ideal.conj_smul_sub_mul_pow_mem_sq_of_frobenius 0 below · cited by 1 · depth 15
• Tame character of inertia at a weak uniformiser Ideal.exists_monoidHom_inertia_residueFieldUnits_ker_iff_of_uniformizer 0 below · cited by 1 · depth 15
• Reducedness of A/(x) from uniformisers at associated primes Ideal.isReduced_quotient_span_singleton_of_forall_mem_associatedPrimes 0 below · cited by 1 · depth 15
• Minimal iff avoiding π below Q forces Q' = Q Ideal.eq_of_le_of_mem_of_mem_minimalPrimes_iff_notMem 0 below · cited by 1 · depth 16
• Finiteness of height-one primes containing a nonzero element Ideal.finite_setOf_height_eq_one_and_mem 0 below · cited by 6 · depth 16
• Height is preserved by contraction along an integral extension Ideal.height_eq_height_under_of_finiteType_of_isIntegral 1 below · cited by 3 · depth 16
• Reducedness and component count of a crossing from a radical witness Ideal.isReduced_quotient_tensorProduct_sup_and_natCard_primeSpectrum_eq_card_of_radical_witness 4 below · cited by 1 · depth 16
• Ideals of a Noetherian local ring are contracted from the completion Ideal.comap_map_adicCompletion_eq_of_isNoetherianRing 0 below · cited by 4 · depth 17
• Height is preserved under contraction along an integral extension Ideal.height_eq_height_under_of_isIntegrallyClosed_of_isIntegral 0 below · cited by 2 · depth 17
• A prime with DVR localisation has height one Ideal.height_eq_one_of_isDiscreteValuationRing_localization_atPrime 0 below · cited by 1 · depth 17
• A maximal ideal of a ring finite over ℤ contains a prime Ideal.exists_prime_natCast_mem_of_isMaximal 0 below · cited by 1 · depth 18
• Flat base change for colon ideals of finitely generated ideals Ideal.map_colon_eq_colon_map_of_flat 0 below · cited by 1 · depth 18
• Minimal primes of the special fibre are not maximal Ideal.not_isMaximal_of_mem_minimalPrimes_of_forall_not_isOpen_singleton 0 below · cited by 1 · depth 18
• Height one equals minimality over a principal ideal Ideal.height_eq_one_iff_mem_minimalPrimes_span_singleton_of_mem 0 below · cited by 3 · depth 19
• Height drops by one modulo an element avoiding minimal primes Ideal.height_map_quotientMk_span_singleton_add_one 1 below · cited by 1 · depth 19
• Faithfully flat descent for ideals, affine case Ideal.map_comap_eq_self_of_map_includeLeft_eq_map_includeRight 0 below · cited by 1 · depth 19
• Principal ideals agreeing at all height-one primes are equal Ideal.span_singleton_eq_span_singleton_of_forall_height_eq_one_map_eq 0 below · cited by 1 · depth 19
• Hensel's lemma along an adically complete ideal Ideal.existsUnique_sub_mem_and_eval_eq_zero_of_isUnit_derivative 0 below · cited by 2 · depth 20
• Galois descent of Γ-stable ideals in S ⊗_W W' Ideal.eq_map_comap_includeLeft_of_forall_map_eq_of_sum_mul_smul_eq 0 below · cited by 1 · depth 26
• G-stable primes are contained in primes over a common base prime Ideal.le_of_liesOver_of_forall_smul_eq_of_isInvariant 0 below · cited by 2 · depth 26
• A closed point on only one minimal prime of I Ideal.exists_isMaximal_forall_mem_minimalPrimes_le_imp_eq_of_finiteType 0 below · cited by 1 · depth 27
• Residue degree at a height-one prime is at most the generic degree Ideal.finrank_residueField_le_finrank_of_height_eq_one 0 below · cited by 2 · depth 27
• Trivial residue extension from trivial action of the stabiliser Ideal.forall_exists_sub_algebraMap_mem_of_forall_smul_eq_imp_smul_sub_mem 0 below · cited by 1 · depth 27
• Dimension formula for affine domains Ideal.height_add_ringKrullDim_quotient_eq_ringKrullDim_of_finiteType 0 below · cited by 10 · depth 27
• Non-maximal non-zero primes have height one in dimension ≤ 2 Ideal.height_eq_one_of_ne_bot_of_not_isMaximal_of_ringKrullDim_le_two 0 below · cited by 8 · depth 27
• Principality at a thickness-one crossing over a DVR Ideal.exists_eq_span_singleton_and_mem_nonZeroDivisors_of_forall_mul_mem_of_surjective_of_isDiscreteValuationRing 1 below · cited by 1 · depth 29
• Two closed points of an affine variety lie on a curve Ideal.exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one 11 below · cited by 2 · depth 29
• Trivial inertia iff e=1 and separable residue extension Ideal.inertia_eq_bot_iff_ramificationIdxIn_eq_one_and_isSeparable 0 below · cited by 1 · depth 29
• Ideals saturated with respect to t are principal Ideal.isPrincipal_of_surjective_of_isDiscreteValuationRing_of_ker_eq_span_singleton_of_forall_mul_mem 0 below · cited by 2 · depth 29
• A fixed element in one of two swapped ideals pins both Ideal.map_eq_self_of_apply_eq_of_mem_of_not_mem 0 below · cited by 1 · depth 29
• Automorphisms fixing π permute the minimal primes of (π) Ideal.map_mem_minimalPrimes_span_singleton_of_apply_eq 0 below · cited by 1 · depth 29
• Ramification index read on the valuation ring S_P Ideal.map_valuationSubring_eq_maximalIdeal_pow_ramificationIdx 0 below · cited by 3 · depth 29
• Inertia at an ideal equals inertia at its centred place Ideal.mem_inertia_iff_smul_valuationSubring_eq_and_forall_smul_sub_mem_nonunits 0 below · cited by 3 · depth 29
• Coprime Kummer radicand forces n ∣ e(P∣𝔪) Ideal.dvd_ramificationIdx_of_pow_eq_unit_mul_zpow_of_isCoprime 0 below · cited by 1 · depth 30
• Generators of K ⊗_P IP and vanishing on J· I Ideal.exists_eq_smul_one_tmul_and_one_tmul_eq_zero_of_isLocalization 0 below · cited by 1 · depth 30
• Principal extended ideal has a generator from I Ideal.exists_mem_and_map_eq_span_singleton_and_mem_nonZeroDivisors_of_map_eq_span_singleton 0 below · cited by 1 · depth 30
• Bertini irreducibility: irreducible hypersurface section through two points Ideal.exists_mem_and_mem_and_radical_span_singleton_isPrime 10 below · cited by 1 · depth 30
• Prime avoidance in pointwise form Ideal.exists_mem_forall_not_mem_of_forall_not_le 0 below · cited by 1 · depth 31
• Geometric irreducibility of the generic fibre spreads out Ideal.exists_ne_zero_and_forall_isMaximal_radical_map_isPrime 8 below · cited by 1 · depth 31
• Refining a basic-open cover along orthogonal idempotents Ideal.exists_span_eq_top_forall_exists_ringHom_localizationAway_idempotent_eq_one 0 below · cited by 1 · depth 31
• Finiteness of residue fields of finite-type algebras Ideal.finite_quotient_of_isMaximal_of_finiteType_of_finite_quotient 0 below · cited by 6 · depth 31
• varpi A is prime when κ ⊗_R A is a domain Ideal.isPrime_span_algebraMap_of_isDomain_tensor 0 below · cited by 2 · depth 31
• Finitely many elements with a prime-local property generate the unit ideal Ideal.exists_finset_span_eq_top_of_forall_prime_exists_not_mem 0 below · cited by 4 · depth 32
• Product of linear forms congruent to x₀x₁^q-x₀^qx₁ modulo 𝔪^{q+2} Ideal.mul_prod_sub_drinfeldForm_mem_pow_of_sub_mem_sq 0 below · cited by 1 · depth 32
• Lower bound d for components of closed fibres Ideal.natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent 1 below · cited by 1 · depth 32
• Splitting trichotomy in Galois extensions of prime degree Ideal.ncard_primesOver_ramificationIdx_inertiaDeg_trichotomy_of_isGalois_of_finrank_prime 0 below · cited by 2 · depth 32
• A predicate avoiding every prime yields a finite unit-ideal family Ideal.exists_finite_span_range_eq_top_of_forall_isPrime_exists_not_mem 0 below · cited by 1 · depth 33
• Artin–Rees estimates along a morphism of J-adic systems Ideal.exists_forall_ker_le_map_proj_sup_pow_smul_top_and_pow_smul_top_inf_le_of_forall_ker_eq_pow_smul_top 3 below · cited by 1 · depth 33
• Uniform Artin–Rees bound for kernels of morphisms of adic systems Ideal.exists_forall_pow_smul_top_inf_ker_le_pow_smul_ker_of_forall_ker_eq_pow_smul_top 2 below · cited by 2 · depth 33
• Automorphic translates of a prime exhaust the primes Ideal.forall_isPrime_exists_eq_comap_of_card_mul_finrank_eq 1 below · cited by 4 · depth 33
• Primes of F⊗_S B versus minimal primes of B Ideal.minimalPrimes_tensorProduct_fractionRing_dictionary 0 below · cited by 4 · depth 33
• Drinfeld-form congruence modulo 𝔪^{q+2} at every prime Ideal.mul_prod_sub_drinfeldForm_mem_pow_of_sub_mem_sq_of_natCast_mem 0 below · cited by 1 · depth 33
• Minimal primes of a flat algebra meet A[x] trivially Ideal.comap_adjoin_singleton_eq_bot_of_mem_minimalPrimes_of_flat_of_isIntegral 0 below · cited by 2 · depth 34
• Finitely many elements with P generating the unit ideal Ideal.exists_finset_span_eq_top_of_forall_isMaximal_exists_not_mem 0 below · cited by 1 · depth 34
• Simultaneous local generators at finitely many maximal ideals Ideal.exists_forall_map_localization_eq_span_of_finite_maximal 0 below · cited by 1 · depth 34
• Local equality of ideals gives an idempotent generator modulo I Ideal.exists_isIdempotentElem_map_mk_eq_span_of_forall_map_localization_eq 0 below · cited by 1 · depth 34
• Lifting N-element local generation of J from the special fibre Ideal.exists_map_localization_eq_span_of_flat_of_residueField_mvPolynomial 0 below · cited by 1 · depth 34
• Completion along a minimal prime when the completion is a domain Ideal.exists_ringEquiv_adicCompletion_quotient_of_mem_minimalPrimes_of_isDomain_adicCompletion 0 below · cited by 4 · depth 34
• Primes exhaust S when residue degrees sum to dim_F R Ideal.forall_isPrime_mem_of_sum_finrank_quotient_eq_finrank 0 below · cited by 1 · depth 34
• Integrally closed quotients by minimal primes from adic completions Ideal.isIntegrallyClosed_quotient_of_mem_minimalPrimes_of_forall_isMaximal_adicCompletion 2 below · cited by 2 · depth 34
• Ideals generated by idempotents lie in all powers Ideal.span_le_pow_of_forall_isIdempotentElem_of_subset 0 below · cited by 2 · depth 34
• Descent of local M-generation along a field extension Ideal.exists_map_localization_eq_span_of_baseChange_mvPolynomial 0 below · cited by 1 · depth 35
• Non-zero primes of affine domains are centres of prime divisors Ideal.exists_valuationSubring_valuation_lt_one_iff_mem_of_finiteType 2 below · cited by 1 · depth 35
• Ring as fibre product of two quotients with zero intersection Ideal.injective_quotient_mk_prod_and_exists_of_factor_eq_of_inf_eq_bot 0 below · cited by 1 · depth 35
• Residue separability from inertia of order prime to the residue characteristic Ideal.isSeparable_quotient_of_forall_prime_not_dvd_card_inertia 0 below · cited by 1 · depth 35
• Minimal primes of a ring with a root of Φ_ℓ Ideal.minimalPrimes_eq_span_sub_pow_of_aeval_cyclotomic_eq_zero 0 below · cited by 1 · depth 35
• Ramification and residue degree are trivial for the decomposition ring Ideal.ramificationIdx_under_eq_one_and_inertiaDeg_under_eq_one_of_isGaloisGroup_stabilizer 0 below · cited by 1 · depth 35
• No tangent directions at an isolated reduced point Ideal.snd_apply_eq_zero_of_mem_minimalPrimes_of_isMaximal 0 below · cited by 2 · depth 35
• Nakayama: finitely generated ideal with flat quotient dies near 𝔭 Ideal.exists_notMem_and_forall_mul_eq_zero_of_flat_quotient_of_rTensor_injective 1 below · cited by 1 · depth 36
• Nonzero prime with d independent residues has height one Ideal.height_eq_one_of_ne_bot_of_forall_aeval_mem_imp_eq_zero_of_ringKrullDim_eq 2 below · cited by 1 · depth 36
• Krull intersection for mathfrak m_S-powers in a module-finite algebra Ideal.iInf_map_maximalIdeal_pow_eq_bot_of_moduleFinite 0 below · cited by 1 · depth 36
• Complementary principal ideals at a root of Φ_ℓ Ideal.isCompl_span_singleton_sub_algebraMap_of_aeval_cyclotomic_eq_zero 0 below · cited by 1 · depth 36
• Reduced ring: a complemented ideal with one minimal prime over it Ideal.isDomain_quotient_of_isReduced_of_isCompl_of_existsUnique_minimalPrimes 0 below · cited by 1 · depth 36
• Cotangent space at a maximal ideal equals that of the localisation Ideal.mapCotangent_bijective_of_isLocalization_atPrime_of_isMaximal 0 below · cited by 1 · depth 36
• Nakayama: local generation of J at a prime Ideal.map_algebraMap_localizationAtPrime_eq_span_of_le_span_sup_mul 0 below · cited by 1 · depth 36
• Tame ramification: P^e does not divide the different Ideal.ramificationIdx_pow_not_dvd_differentIdeal 0 below · cited by 1 · depth 36
• Globalising a locally ideal-cut condition on ring maps Ideal.exists_forall_iff_map_eq_bot_of_forall_away 0 below · cited by 1 · depth 37
• Dropping a minimal generator of an ideal over a local ring Ideal.exists_map_mk_span_singleton_eq_span_of_not_mem_smul 0 below · cited by 1 · depth 37
• Clearing denominators: finitely generated ideals agreeing locally at 𝔭 Ideal.exists_not_mem_forall_map_eq_map_of_isLocalization_of_map_eq_map_of_fg 0 below · cited by 1 · depth 37
• A predicate avoiding every maximal ideal yields a finite unit-ideal cover Ideal.exists_span_range_eq_top_of_forall_isMaximal_exists_notMem 0 below · cited by 1 · depth 37
• Reduced rings: √(a)∩√Ann(a)=0 Ideal.radical_span_inf_radical_annihilator_eq_bot_of_isReduced 0 below · cited by 1 · depth 39
• Idempotent ideal in a Noetherian ring is annihilated off a prime Ideal.exists_not_mem_and_forall_mul_eq_zero_of_le_sq_of_le 0 below · cited by 2 · depth 41
• Faithful flatness detects ideals of R_𝔭 Ideal.map_algebraMap_localization_atPrime_eq_of_map_comp_eq_of_faithfullyFlat 0 below · cited by 1 · depth 44

Ideal.IsMaximal 2

• Nonzero primes of a domain integral over F[x] are maximal Ideal.IsMaximal.of_isPrime_of_ne_bot_of_isIntegral_adjoin_singleton 0 below · cited by 2 · depth 31
• Completion at a maximal ideal agrees with completion of the localisation Ideal.IsMaximal.exists_adicCompletion_localization_ringEquiv 0 below · cited by 2 · depth 34