IsLocalization

Supporting results for Nagata’s factoriality theorem.

theorem NagataFactoriality.IsLocalization.mk'_mul_map {α : Type u_1} {β : Type u_2} [CommRing α] [CommRing β] {S : Submonoid α} [Algebra α β] [IsLocalization S β] (a s : α) (hs : s ∈ S) : IsLocalization.mk' β a ⟨s, hs⟩ * (algebraMap α β) s = (algebraMap α β) a

@[simp]

theorem NagataFactoriality.IsLocalization.map_mul_mk' {α : Type u_1} {β : Type u_2} [CommRing α] [CommRing β] {S : Submonoid α} [Algebra α β] [IsLocalization S β] (a b s : α) (hs : s ∈ S) : (algebraMap α β) a * IsLocalization.mk' β b ⟨s, hs⟩ = IsLocalization.mk' β (a * b) ⟨s, hs⟩

theorem NagataFactoriality.IsLocalization.surj {α : Type u_1} {β : Type u_2} [CommRing α] [CommRing β] {S : Submonoid α} [Algebra α β] [IsLocalization S β] (z : β) : ∃ (a : α) (s : α) (hs : s ∈ S), z = IsLocalization.mk' β a ⟨s, hs⟩

theorem NagataFactoriality.IsLocalization.algebraMap_injective {α : Type u_1} {β : Type u_2} [CommRing α] [CommRing β] [Algebra α β] [IsDomain α] (S : Submonoid α) [Fact (0 ∉ S)] [IsLocalization S β] : Function.Injective ⇑(algebraMap α β)

theorem NagataFactoriality.IsLocalization.mk'_eq_iff {α : Type u_1} {β : Type u_2} [CommRing α] [CommRing β] {S : Submonoid α} [Algebra α β] [IsLocalization S β] [IsDomain α] [Fact (0 ∉ S)] {a b s t : α} (hs : s ∈ S) (ht : t ∈ S) : IsLocalization.mk' β a ⟨s, hs⟩ = IsLocalization.mk' β b ⟨t, ht⟩ ↔ a * t = b * s

theorem NagataFactoriality.IsLocalization.map_eq_iff {α : Type u_1} {β : Type u_2} [CommRing α] [CommRing β] [Algebra α β] [IsDomain α] (S : Submonoid α) [Fact (0 ∉ S)] [IsLocalization S β] (a b : α) : (algebraMap α β) a = (algebraMap α β) b ↔ a = b

theorem NagataFactoriality.IsLocalization.mk'_eq_zero_iff {α : Type u_1} {β : Type u_2} [CommRing α] [CommRing β] {S : Submonoid α} [Algebra α β] [IsLocalization S β] [IsDomain α] [Fact (0 ∉ S)] {a s : α} (hs : s ∈ S) : IsLocalization.mk' β a ⟨s, hs⟩ = 0 ↔ a = 0

theorem NagataFactoriality.IsLocalization.map_eq_zero_iff {α : Type u_1} {β : Type u_2} [CommRing α] [CommRing β] [Algebra α β] [IsDomain α] (S : Submonoid α) [Fact (0 ∉ S)] [IsLocalization S β] (a : α) : (algebraMap α β) a = 0 ↔ a = 0

theorem NagataFactoriality.IsLocalization.dvd_map_iff {α : Type u_1} {β : Type u_2} [CommRing α] [CommRing β] {S : Submonoid α} [Algebra α β] [IsLocalization S β] [IsDomain α] [Fact (0 ∉ S)] {a b : α} : (algebraMap α β) a ∣ (algebraMap α β) b ↔ ∃ s ∈ S, a ∣ s * b

@[simp]

theorem NagataFactoriality.IsLocalization.isUnit_mk'_of_mem {α : Type u_1} {β : Type u_2} [CommRing α] [CommRing β] {S : Submonoid α} [Algebra α β] [IsLocalization S β] {a s : α} (ha : a ∈ S) (hs : s ∈ S) : IsUnit (IsLocalization.mk' β a ⟨s, hs⟩)

theorem NagataFactoriality.IsLocalization.isUnit_map_of_mem {α : Type u_1} {β : Type u_2} [CommRing α] [CommRing β] {S : Submonoid α} [Algebra α β] [IsLocalization S β] {s : α} (hs : s ∈ S) : IsUnit ((algebraMap α β) s)

theorem NagataFactoriality.IsLocalization.isUnit_map_of_isUnit {α : Type u_1} {β : Type u_2} [CommRing α] [CommRing β] [Algebra α β] {a : α} (ha : IsUnit a) : IsUnit ((algebraMap α β) a)

theorem NagataFactoriality.IsLocalization.isUnit_mk'_of_isUnit {α : Type u_1} {β : Type u_2} [CommRing α] [CommRing β] {S : Submonoid α} [Algebra α β] [IsLocalization S β] {a s : α} (ha : IsUnit a) (hs : s ∈ S) : IsUnit (IsLocalization.mk' β a ⟨s, hs⟩)