Changing the base ring of an integrality claim

Mathlib's isIntegral_trans transfers integrality down a scalar tower R → A → B. The variant here drops the tower: the two candidate base rings are only required to map compatibly into the ring where the element lives, which is what happens when both of them sit inside that ring without either being an algebra over the other.

Main results

• TauCeti.isIntegral_trans_common: if every element of P becomes integral over R once mapped into L, then an element of L integral over P is integral over R.
• TauCeti.dvd_of_isIntegral_div: an element of a field extension of A that is a quotient of elements of A and is integral over A has its numerator divisible by its denominator, when A is integrally closed.

theorem TauCeti.isIntegral_trans_common {R : Type u_1} {P : Type u_2} {L : Type u_3} [CommRing R] [CommRing P] [CommRing L] [Algebra R L] [Algebra P L] (hP : ∀ (x : P), IsIntegral R ((algebraMap P L) x)) {x : L} (hx : IsIntegral P x) : IsIntegral R x

Integrality transfers through compatible maps from two rings into a common ring.

theorem TauCeti.dvd_of_isIntegral_div {A : Type u_1} {L : Type u_2} [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [Field L] [Algebra A L] [FaithfulSMul A L] {a d : A} (hd : d ≠ 0) (h : IsIntegral A ((algebraMap A L) a / (algebraMap A L) d)) : d ∣ a

An element of a field extension of A that is a quotient of elements of A and is integral over A has its numerator divisible by its denominator, when A is integrally closed.