mathlib documentation

ring_theory.integrally_closed

Integrally closed rings #

An integrally closed domain R contains all the elements of Frac(R) that are integral over R. A special case of integrally closed domains are the Dedekind domains.

Main definitions #

Main results #

@[class]
structure is_integrally_closed (R : Type u_1) [comm_ring R] [is_domain R] :
Prop

R is integrally closed if all integral elements of Frac(R) are also elements of R.

This definition uses fraction_ring R to denote Frac(R). See is_integrally_closed_iff if you want to choose another field of fractions for R.

Instances
theorem is_integrally_closed_iff {R : Type u_1} [comm_ring R] [is_domain R] (K : Type u_2) [field K] [algebra R K] [is_fraction_ring R K] :
is_integrally_closed R ∀ {x : K}, is_integral R x(∃ (y : R), (algebra_map R K) y = x)

R is integrally closed iff all integral elements of its fraction field K are also elements of R.

R is integrally closed iff it is the integral closure of itself in its field of fractions.

@[instance]
def is_integrally_closed.is_integral_closure {R : Type u_1} [comm_ring R] [is_domain R] [iic : is_integrally_closed R] {K : Type u_2} [field K] [algebra R K] [is_fraction_ring R K] :
theorem is_integrally_closed.is_integral_iff {R : Type u_1} [comm_ring R] [is_domain R] [iic : is_integrally_closed R] {K : Type u_2} [field K] [algebra R K] [is_fraction_ring R K] {x : K} :
is_integral R x ∃ (y : R), (algebra_map R K) y = x
@[simp]
theorem is_integrally_closed.integral_closure_eq_bot (R : Type u_1) [comm_ring R] [is_domain R] [iic : is_integrally_closed R] (K : Type u_2) [field K] [algebra R K] [is_fraction_ring R K] :