isFractionRing_of_isDomain_of_isLocalization

English

If M is a submonoid of a domain R and S is a localization of R at M, then under mild hypotheses there is an induced IsFractionRing S T for some T, i.e., S localizes to a fraction ring of T.

Русский

Если M задаёт локализацию S = M^{-1}R, то S выступает как фракционная оболочка над T.

LaTeX

$$IsFractionRing S T$$

Lean4

theorem isFractionRing_of_isDomain_of_isLocalization [IsDomain R] (S T : Type*) [CommRing S] [CommRing T] [Algebra R S]
    [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsFractionRing R T] : IsFractionRing S T :=
  by
  haveI := IsFractionRing.nontrivial R T
  haveI := (algebraMap S T).domain_nontrivial
  apply isFractionRing_of_isLocalization M S T
  intro x hx
  rw [mem_nonZeroDivisors_iff_ne_zero]
  intro hx'
  apply @zero_ne_one S
  rw [← (algebraMap R S).map_one, ← @mk'_one R _ M, @comm _ Eq, mk'_eq_zero_iff]
  exact ⟨⟨x, hx⟩, by simp [hx']⟩

Похожие утверждения