English
For a ring equivalence φ: R ≃+* T, an element a ∈ S is integral over R iff it is integral over T under matching algebra maps.
Русский
Для эквивалентности колец φ: R ≃+* T элемент a ∈ S интегрирован над R тогда и только тогда, когда интегрирован над T при совместимых отображениях.
LaTeX
$$$\\text{IsIntegral}_R(a) \\iff \\text{IsIntegral}_T(a)$$$
Lean4
theorem isIntegral_iff {R S T : Type*} [CommRing R] [Ring S] [CommRing T] [Algebra R S] [Algebra T S] (φ : R ≃+* T)
(h : (algebraMap T S).comp φ.toRingHom = algebraMap R S) (a : S) : IsIntegral R a ↔ IsIntegral T a :=
by
constructor <;> intro ha
· letI : Algebra R T := φ.toRingHom.toAlgebra
letI : IsScalarTower R T S := ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, ← h, mul_assoc]; rfl⟩
exact IsIntegral.tower_top ha
· have h' : (algebraMap T S) = (algebraMap R S).comp φ.symm.toRingHom := by
simp only [← h, RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe, RingEquiv.comp_symm, RingHomCompTriple.comp_eq]
letI : Algebra T R := φ.symm.toRingHom.toAlgebra
letI : IsScalarTower T R S := ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, h', mul_assoc]; rfl⟩
exact IsIntegral.tower_top ha
