AlgebraicCurves.Geometry.Sheaves.Proofs.SaturatedProductIdeal.LABody.isLocalizationAway_of_irreducible
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SaturatedProductIdeal
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace LABody
open _root_.AlgebraicGeometry.Scheme
section DVR
variable {O : Type u} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
(T' : Type u) [Field T'] [Algebra O T'] [IsFractionRing O T']Lean source · full declaration
theorem isLocalizationAway_of_irreducible {ϖ : O} (hϖ : Irreducible ϖ) : IsLocalization.Away ϖ T'
where
map_units := fun ⟨y, hy⟩ => by
obtain ⟨n, rfl⟩ := hy
exact IsUnit.mk0 _ (by
rw [map_pow]
exact pow_ne_zero _ (fun h => hϖ.ne_zero ((IsFractionRing.injective O T')
(by rw [h, map_zero]))))
surj := fun z => by
obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective (A := O) z
have hb0 : b ≠ 0 := nonZeroDivisors.ne_zero hb
obtain ⟨n, u, rfl⟩ := IsDiscreteValuationRing.eq_unit_mul_pow_irreducible hb0 hϖ
refine ⟨⟨a * ↑u⁻¹, ⟨ϖ ^ n, n, rfl⟩⟩, ?_⟩
have hb' : algebraMap O T' (↑u * ϖ ^ n) ≠ 0 := fun h =>
hb0 ((IsFractionRing.injective O T') (by rw [h, map_zero]))
change algebraMap O T' a / algebraMap O T' (↑u * ϖ ^ n) * algebraMap O T' (ϖ ^ n) =
algebraMap O T' (a * ↑u⁻¹)
rw [div_mul_eq_mul_div, div_eq_iff hb', ← map_mul, ← map_mul]
congr 1
rw [show a * ↑u⁻¹ * (↑u * ϖ ^ n) = a * (↑u⁻¹ * ↑u) * ϖ ^ n by ring, Units.inv_mul, mul_one]
exists_of_eq := fun {a b} h => ⟨1, by rw [IsFractionRing.injective O T' h]⟩