English
If a commutative ring R has an I-adic topology with I contained in the Jacobson radical, then R× is open in R.
Русский
Если кольцо R коммутативно снабжено I-адической топологией и I включено в радикал Якобсона, то R× открыто в R.
LaTeX
$$$R^{\\times} \\text{ открыто в } R$ under IsAdic I$$
Lean4
/-- If `R` has the `I`-adic topology where `I` is contained in the Jacobson radical
(e.g. when `R` is complete or local), then `Rˣ` is an open subspace of `R`. -/
theorem of_isAdic {R : Type*} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] {I : Ideal R} (hR : IsAdic I)
(hI : I ≤ Ideal.jacobson ⊥) : IsOpenUnits R :=
by
refine ⟨.of_continuous_injective_isOpenMap Units.continuous_val Units.val_injective ?_⟩
refine (IsTopologicalGroup.isOpenMap_iff_nhds_one (f := Units.coeHom R)).mpr ?_
rw [nhds_induced, nhds_prod_eq]
simp only [Units.embedProduct_apply, Units.val_one, inv_one, MulOpposite.op_one]
intro s hs
have H := hR ▸ Ideal.hasBasis_nhds_adic I 1
have := (H.prod (H.comap MulOpposite.opHomeomorph.symm))
simp only [Homeomorph.comap_nhds_eq, Homeomorph.symm_symm, MulOpposite.opHomeomorph_apply, MulOpposite.op_one,
and_self, Set.image_add_left] at this
have : ∃ n₁ n₂, ∀ (u : Rˣ), (-1 + u : R) ∈ I ^ n₁ → (-1 + u⁻¹ : R) ∈ I ^ n₂ → ↑u ∈ s := by
simpa [Set.subset_def, forall_comm (β := Rˣ), forall_comm (β := _ = _)] using
(((this.comap (Units.embedProduct R)).map (Units.coeHom R)).1 _).mp hs
obtain ⟨n, hn, hn'⟩ : ∃ n ≠ 0, ∀ (u : Rˣ), (-1 + u : R) ∈ I ^ n → (-1 + u⁻¹ : R) ∈ I ^ n → ↑u ∈ s :=
by
obtain ⟨n₁, n₂, H⟩ := this
exact
⟨n₁ ⊔ n₂ ⊔ 1, by simp, fun u h₁ h₂ ↦
H u (Ideal.pow_le_pow_right (by simp) h₁) (Ideal.pow_le_pow_right (by simp) h₂)⟩
rw [H.1]
refine ⟨n, trivial, ?_⟩
rintro _ ⟨x, hx, rfl⟩
have := Ideal.mem_jacobson_bot.mp (hI (Ideal.pow_le_self hn hx)) 1
rw [mul_one, add_comm] at this
refine hn' this.unit (by simpa using hx) ?_
have : -1 + ↑this.unit⁻¹ = -this.unit⁻¹ * x :=
by
trans this.unit⁻¹ * (-(1 + x) + 1)
· rw [mul_add, mul_neg, IsUnit.val_inv_mul, mul_one]
· simp
rw [this]
exact Ideal.mul_mem_left _ _ hx
