Integral elements of quadratic algebras

Let R be a commutative ring and K a commutative R-algebra in which R is integrally closed (for instance an integrally closed domain and its fraction field). We characterize the elements of QuadraticAlgebra K a b that are integral over R.

Main results

• QuadraticAlgebra.isIntegral_omega: when a and b lie in R, the generator ω is integral over R.
• QuadraticAlgebra.re_mem_range_of_im_mem_range: if a and b lie in R, z is integral over R and z.im lies in R, then z.re also lies in R.
• QuadraticAlgebra.isIntegral_iff: an element of QuadraticAlgebra K a b is integral over R iff its trace and its norm lie in R.

@[simp]

theorem QuadraticAlgebra.isIntegral_star_iff {R : Type u_1} {K : Type u_2} [CommRing R] [CommRing K] [Algebra R K] {a b : K} {z : QuadraticAlgebra K a b} : IsIntegral R (star z) ↔ IsIntegral R z

theorem QuadraticAlgebra.isIntegral_of_trace_mem_range_of_norm_mem_range {R : Type u_1} {K : Type u_2} [CommRing R] [CommRing K] [Algebra R K] {a b : K} {z : QuadraticAlgebra K a b} (ht : trace z ∈ Set.range ⇑(algebraMap R K)) (hn : norm z ∈ Set.range ⇑(algebraMap R K)) : IsIntegral R z

An element whose trace and norm lie in R is integral over R.

theorem QuadraticAlgebra.isIntegral_omega {R : Type u_1} {K : Type u_2} [CommRing R] [CommRing K] [Algebra R K] {a b : K} (ha : a ∈ Set.range ⇑(algebraMap R K)) (hb : b ∈ Set.range ⇑(algebraMap R K)) : IsIntegral R omega

When a and b lie in R, the generator ω is integral over R.

theorem QuadraticAlgebra.trace_mem_range_of_isIntegral {R : Type u_1} {K : Type u_2} [CommRing R] [CommRing K] [Algebra R K] {a b : K} {z : QuadraticAlgebra K a b} [IsIntegrallyClosedIn R K] (hz : IsIntegral R z) : trace z ∈ Set.range ⇑(algebraMap R K)

The trace of an element integral over R lies in R.

theorem QuadraticAlgebra.norm_mem_range_of_isIntegral {R : Type u_1} {K : Type u_2} [CommRing R] [CommRing K] [Algebra R K] {a b : K} {z : QuadraticAlgebra K a b} [IsIntegrallyClosedIn R K] (hz : IsIntegral R z) : norm z ∈ Set.range ⇑(algebraMap R K)

The norm of an element integral over R lies in R.

theorem QuadraticAlgebra.re_mem_range_of_im_mem_range {R : Type u_1} {K : Type u_2} [CommRing R] [CommRing K] [Algebra R K] {a b : K} {z : QuadraticAlgebra K a b} [IsIntegrallyClosedIn R K] (ha : a ∈ Set.range ⇑(algebraMap R K)) (hb : b ∈ Set.range ⇑(algebraMap R K)) (h : IsIntegral R z) (him : z.im ∈ Set.range ⇑(algebraMap R K)) : z.re ∈ Set.range ⇑(algebraMap R K)

If a and b lie in R, z is integral over R and z.im lies in R, then z.re also lies in R.

theorem QuadraticAlgebra.isIntegral_iff {R : Type u_1} {K : Type u_2} [CommRing R] [CommRing K] [Algebra R K] {a b : K} {z : QuadraticAlgebra K a b} [IsIntegrallyClosedIn R K] : IsIntegral R z ↔ trace z ∈ Set.range ⇑(algebraMap R K) ∧ norm z ∈ Set.range ⇑(algebraMap R K)

An element of QuadraticAlgebra K a b is integral over R iff its trace and its norm lie in R.