Namespace Subalgebra 29 theorems
- Extending k-points from a subalgebra of a module-finite algebra
Subalgebra.exists_algHom_comp_val_eq_of_isAlgClosed0 below · cited by 4 · depth 13 - L[x] is integrally closed for x transcendental
Subalgebra.isIntegrallyClosed_adjoin_singleton_of_transcendental0 below · cited by 7 · depth 13 - Norm over an order in a valuation ring, and its residue
Subalgebra.algebraMap_norm_eq_and_residue_norm_eq_mul0 below · cited by 2 · depth 14 - Krull dimension one for fibres of normal subalgebras over Λ[X]
Subalgebra.ringKrullDim_localization_tensor_eq_one_of_irreducible9 below · cited by 13 · depth 14 - Normality of K ⊗_{R_0} A for finite separable K/k₀
Subalgebra.isDomain_and_isIntegrallyClosed_tensor_of_isField_of_isSeparable1 below · cited by 3 · depth 15 - Integral closedness of R'⊗_R A from reduced special fibre
Subalgebra.isDomain_and_isIntegrallyClosed_tensor_of_isReduced_fibre3 below · cited by 3 · depth 15 - Reducedness of k ⊗_Λ A from separable reduction
Subalgebra.isReduced_tensor_of_separable11 below · cited by 2 · depth 16 - An étale finite R-order spanning A over K is maximal
Subalgebra.eq_integralClosure_of_etale_of_span_eq_top2 below · cited by 2 · depth 17 - Local Dedekind–Kummer criterion at a simple root
Subalgebra.exists_mul_mem_map_ker_of_eval_derivative_map_ne_zero0 below · cited by 1 · depth 17 - Algebra homomorphisms to an algebraically closed field extend along module-finite extensions
Subalgebra.exists_algHom_comp_val_eq_of_isAlgClosed_of_moduleFinite0 below · cited by 5 · depth 18 - Faithful flatness over a directed union of subalgebras
Subalgebra.faithfullyFlat_of_directed_of_forall_faithfullyFlat0 below · cited by 1 · depth 18 - Faithful flatness over a subalgebra descends along a field extension
Subalgebra.faithfullyFlat_of_faithfullyFlat_range_baseChange0 below · cited by 1 · depth 18 - Integral closedness from principal maximal ideals of localisations
Subalgebra.mem_of_isIntegral_of_fg_of_forall_isPrincipal_maximalIdeal_localization_atPrime0 below · cited by 1 · depth 20 - Ascending chains of R-orders in L stabilise
Subalgebra.exists_forall_le_eq_of_monotone_of_le_integralClosure1 below · cited by 1 · depth 26 - Shrinking an affine chart: minimal primes contracting into 𝔪
Subalgebra.exists_notMem_forall_minimalPrimes_map_le_of_fg0 below · cited by 3 · depth 26 - Non-maximal primes over the uniformiser are minimal
Subalgebra.mem_minimalPrimes_map_maximalIdeal_of_not_isMaximal_of_fg_of_isAlgebraic_adjoin1 below · cited by 3 · depth 26 - Module-finite overrings of a local ring with a length-two regular sequence
Subalgebra.eq_bot_of_moduleFinite_of_forall_ne_maximalIdeal_of_isRegular_pair0 below · cited by 1 · depth 27 - Localisation at a horizontal prime is a valuation subring
Subalgebra.exists_valuationSubring_mem_iff_of_isPrime_of_not_map_maximalIdeal_le_of_isAlgebraic_adjoin4 below · cited by 3 · depth 27 - Non-zero primes are maximal in rings between k and F
Subalgebra.isMaximal_of_isPrime_of_ne_bot_of_isAlgebraic_adjoin_singleton1 below · cited by 2 · depth 27 - Krull–Akizuki theorem
Subalgebra.isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite0 below · cited by 5 · depth 27 - Lifting finitely generated ℤ-subalgebras along a directed colimit of rings
Subalgebra.exists_ringHom_comp_eq_val_of_fg_of_directedSystem0 below · cited by 3 · depth 29 - Transitivity of finite generation for subalgebras
Subalgebra.fg_restrictScalars_and_le_of_fg0 below · cited by 2 · depth 30 - Elementary properties of the blow-up chart C[J/t]
Subalgebra.le_and_exists_pow_mul_mem_and_finiteType_of_eq_restrictScalars_adjoin_div0 below · cited by 10 · depth 30 - Finitely generated subalgebras of R_𝔭 spread out to some R[1/r]
Subalgebra.exists_algHom_localizationAway_forall_apply_eq_coe_of_fg0 below · cited by 3 · depth 31 - Subalgebra with associated discriminant is everything
Subalgebra.eq_top_of_associated_discr_of_basis0 below · cited by 1 · depth 32 - Enlarging a finitely generated subring into a given open locus
Subalgebra.exists_fg_le_forall_comap_inclusion_mem_of_isOpen0 below · cited by 1 · depth 32 - Fraction subring of a field is the localisation at P
Subalgebra.exists_ringEquiv_localizationAtPrime_of_forall_mem_iff_exists_mul_eq0 below · cited by 2 · depth 33 - Graded descent for a subalgebra with bijective base change
Subalgebra.exists_gradedAlgebra_isBaseChange_of_bijective_of_decompose_mem0 below · cited by 1 · depth 35 - Blow-up chart C[J/a] under flat adically dense base change
Subalgebra.exists_ringHom_ringEquiv_adicCompletion_adjoin_div_of_flat_of_dense2 below · cited by 2 · depth 35