English
If S is a localization of R and S is unramified over R, then S is unramified over any localization of R.
Русский
Если S локализуется от R и S неразветвлено над R, то S неразветвлено над локализацией R.
LaTeX
$$$[\text{Localization map}] \Rightarrow [\text{Unramified } R_m S_m]$$$
Lean4
theorem bijective_of_isAlgClosed_of_isLocalRing [IsAlgClosed K] [IsLocalRing A] : Function.Bijective (algebraMap K A) :=
by
have := finite_of_free (R := K) (S := A)
have : IsArtinianRing A := isArtinian_of_tower K inferInstance
have hA : IsNilpotent (IsLocalRing.maximalIdeal A) :=
by
rw [← IsLocalRing.jacobson_eq_maximalIdeal ⊥]
· exact IsArtinianRing.isNilpotent_jacobson_bot
· exact bot_ne_top
let e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A :=
{ __ := Algebra.ofId K (A ⧸ IsLocalRing.maximalIdeal A)
__ := Equiv.ofBijective _ IsAlgClosed.algebraMap_bijective_of_isIntegral }
let e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
(Algebra.TensorProduct.congr AlgEquiv.refl e.symm).trans (Algebra.TensorProduct.rid K A A)
let f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap.comp (sec K A _)
have hf : (Algebra.ofId _ _).toLinearMap ∘ₗ f = LinearMap.id :=
by
dsimp [f]
rw [← LinearMap.comp_assoc, ← comp_sec K A]
congr 1
apply LinearMap.restrictScalars_injective K
apply _root_.TensorProduct.ext'
intro r s
obtain ⟨s, rfl⟩ := e.surjective s
suffices s • (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) r = r • e s by simpa [ofId, e']
simp [Algebra.smul_def, e, ofId, mul_comm]
have hf₁ : f 1 • (1 : A ⧸ IsLocalRing.maximalIdeal A) = 1 :=
by
rw [← algebraMap_eq_smul_one]
exact LinearMap.congr_fun hf 1
have hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A := by
rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one, ← Ideal.Quotient.algebraMap_eq, algebraMap_eq_smul_one, hf₁,
sub_self]
have hf₃ : IsIdempotentElem (1 - f 1) := by
apply IsIdempotentElem.one_sub
rw [IsIdempotentElem, ← smul_eq_mul, ← map_smul, hf₁]
have hf₄ : f 1 = 1 := by
obtain ⟨n, hn⟩ := hA
have : (1 - f 1) ^ n = 0 := by
rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hn]
exact Ideal.pow_mem_pow hf₂ n
rw [eq_comm, ← sub_eq_zero, ← hf₃.pow_succ_eq n, pow_succ, this, zero_mul]
refine Equiv.bijective ⟨algebraMap K A, ⇑e.symm ∘ ⇑(algebraMap A _), fun x ↦ by simp, fun x ↦ ?_⟩
have : ⇑(algebraMap K A) = ⇑f ∘ ⇑e := by
ext k
conv_rhs =>
rw [← mul_one k, ← smul_eq_mul, Function.comp_apply, map_smul, LinearMap.map_smul_of_tower, map_one, hf₄, ←
algebraMap_eq_smul_one]
rw [this]
simp only [Function.comp_apply, AlgEquiv.apply_symm_apply, algebraMap_eq_smul_one, map_smul, hf₄, smul_eq_mul,
mul_one]
