EtaleFundamentalGroups.isIntegral_of_isIntegral_localizationAway_pair_of_prime
Integrality over A is detected by the two principal localizations at a prime x and at an element y not divisible by x.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open nonZeroDivisors
universe u v wLean source · full declaration
theorem isIntegral_of_isIntegral_localizationAway_pair_of_prime
{A : Type u} {K : Type v} {L : Type w}
[CommRing A] [IsDomain A] [IsIntegrallyClosed A]
[Field K] [Algebra A K] [IsFractionRing A K]
[Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L]
[Algebra.IsAlgebraic K L]
{x y : A} (hx : Prime x) (hy : y ≠ 0) (hxy : ¬ x ∣ y)
(z : L)
(hzx :
let Aₓ := Localization.subalgebra.ofField K (Submonoid.powers x)
(Submonoid.powers_le.mpr
(mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero))
IsIntegral Aₓ z)
(hzy :
let Aᵧ := Localization.subalgebra.ofField K (Submonoid.powers y)
(Submonoid.powers_le.mpr
(mem_nonZeroDivisors_iff_ne_zero.mpr hy))
IsIntegral Aᵧ z) :
IsIntegral A z := by
have hcoeff : ∀ i : ℕ, (minpoly K z).coeff i ∈ (algebraMap A K).range := by
intro i
apply Algebra.mem_bot.mp
apply mem_bot_of_mem_localizationAway_pair_of_prime
hx hy hxy (z := (minpoly K z).coeff i)
· let Aₓ := Localization.subalgebra.ofField K (Submonoid.powers x)
(Submonoid.powers_le.mpr
(mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero))
let : IsIntegrallyClosed Aₓ :=
isIntegrallyClosed_of_isLocalization Aₓ (Submonoid.powers x)
(Submonoid.powers_le.mpr
(mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero))
have hmin := minpoly.isIntegrallyClosed_eq_field_fractions' K hzx
rw [hmin, Polynomial.coeff_map]
exact Subtype.prop _
· let Aᵧ := Localization.subalgebra.ofField K (Submonoid.powers y)
(Submonoid.powers_le.mpr
(mem_nonZeroDivisors_iff_ne_zero.mpr hy))
let : IsIntegrallyClosed Aᵧ :=
isIntegrallyClosed_of_isLocalization Aᵧ (Submonoid.powers y)
(Submonoid.powers_le.mpr
(mem_nonZeroDivisors_iff_ne_zero.mpr hy))
have hmin := minpoly.isIntegrallyClosed_eq_field_fractions' K hzy
rw [hmin, Polynomial.coeff_map]
exact Subtype.prop _
obtain ⟨q, hq⟩ :=
(Polynomial.mem_map_range (algebraMap A K)).mpr hcoeff
change q.map (algebraMap A K) = minpoly K z at hq
have hqmonic : q.Monic := by
apply ((IsFractionRing.injective A K).monic_map_iff).mpr
rw [hq]
exact minpoly.monic (Algebra.IsIntegral.isIntegral z)
refine ⟨q, hqmonic, ?_⟩
have hzmin := minpoly.aeval K z
rw [← hq] at hzmin
change Polynomial.aeval z q = 0
simpa only [Polynomial.aeval_map_algebraMap] using hzmin