instance Submonoid.instMul {A : Type u_1} [CommMonoid A] : Mul (Submonoid A)

Equations

• Submonoid.instMul = { mul := fun (S T : Submonoid A) => { carrier := ↑S * ↑T, mul_mem' := ⋯, one_mem' := ⋯ } }

instance AddSubmonoid.instAdd {A : Type u_1} [AddCommMonoid A] : Add (AddSubmonoid A)

Equations

• AddSubmonoid.instAdd = { add := fun (S T : AddSubmonoid A) => { carrier := ↑S + ↑T, add_mem' := ⋯, zero_mem' := ⋯ } }

theorem Submonoid.mem_mul_iff {A : Type u_1} [CommMonoid A] {S T : Submonoid A} {x : A} : x ∈ S * T ↔ ∃ y ∈ S, ∃ z ∈ T, y * z = x

theorem AddSubmonoid.mem_add_iff {A : Type u_1} [AddCommMonoid A] {S T : AddSubmonoid A} {x : A} : x ∈ S + T ↔ ∃ y ∈ S, ∃ z ∈ T, y + z = x

theorem Submonoid.left_le_mul {A : Type u_1} [CommMonoid A] {S T : Submonoid A} : S ≤ S * T

theorem Submonoid.right_le_mul {A : Type u_1} [CommMonoid A] {S T : Submonoid A} : T ≤ S * T

theorem Submonoid.mul_le_mul {A : Type u_1} [CommMonoid A] {S S' T T' : Submonoid A} (hS : S ≤ S') (hT : T ≤ T') : S * T ≤ S' * T'

instance Submonoid.instOne {A : Type u_1} [CommMonoid A] : One (Submonoid A)

Equations

• Submonoid.instOne = { one := ⊥ }

theorem Submonoid.one_eq_bot {A : Type u_1} [CommMonoid A] : 1 = ⊥

instance Submonoid.instCommMonoid_project {A : Type u_1} [CommMonoid A] : CommMonoid (Submonoid A)

Equations

• Submonoid.instCommMonoid_project = CommMonoid.mk ⋯

@[simp]

theorem Submonoid.mul_self {A : Type u_1} [CommMonoid A] (S : Submonoid A) : S * S = S

theorem Submonoid.closure_union_eq_mul {A : Type u_1} [CommMonoid A] (s t : Set A) : Submonoid.closure (s ∪ t) = Submonoid.closure s * Submonoid.closure t

theorem Submonoid.FG.mul {A : Type u_1} [CommMonoid A] {S T : Submonoid A} (hS : S.FG) (hT : T.FG) : (S * T).FG

theorem Submonoid.map_mul {A : Type u_2} {B : Type u_3} [CommMonoid A] [CommMonoid B] (f : A →* B) (S T : Submonoid A) : Submonoid.map f (S * T) = Submonoid.map f S * Submonoid.map f T

theorem Localization.prod_mk {A : Type u_1} [CommRing A] (S : Submonoid A) {ι : Type u_4} (s : Finset ι) (t : ι → A) (t' : ι → ↥S) : ∏ i ∈ s, Localization.mk (t i) (t' i) = Localization.mk (∏ i ∈ s, t i) (∏ i ∈ s, t' i)

theorem Localization.split_den {A : Type u_1} [CommRing A] (S : Submonoid A) (x : A) (s t : ↥S) : Localization.mk x s * Localization.mk 1 t = Localization.mk x (s * t)

noncomputable def Localization.mulToTensor {A : Type u_1} [CommRing A] (S T : Submonoid A) : Localization (S * T) →ₐ[A] TensorProduct A (Localization S) (Localization T)

Equations

• Localization.mulToTensor S T = IsLocalization.liftAlgHom ⋯

@[simp]

theorem Localization.mulToTensor_mk {A : Type u_1} [CommRing A] {S T : Submonoid A} (a s t : A) (hs : s ∈ S) (ht : t ∈ T) : (Localization.mulToTensor S T) (Localization.mk a ⟨s * t, ⋯⟩) = Localization.mk a ⟨s, hs⟩ ⊗ₜ[A] Localization.mk 1 ⟨t, ht⟩

@[simp]

theorem Localization.mulToTensor_mk' {A : Type u_1} [CommRing A] {S T : Submonoid A} (a s : A) (hs : s ∈ S) : (Localization.mulToTensor S T) (Localization.mk a ⟨s, ⋯⟩) = Localization.mk a ⟨s, hs⟩ ⊗ₜ[A] 1

@[simp]

theorem Localization.mulToTensor_mk'' {A : Type u_1} [CommRing A] {S T : Submonoid A} (a t : A) (ht : t ∈ T) : (Localization.mulToTensor S T) (Localization.mk a ⟨t, ⋯⟩) = Localization.mk a 1 ⊗ₜ[A] Localization.mk 1 ⟨t, ht⟩

noncomputable def Localization.tensorToLocalization {A : Type u_1} [CommRing A] (S T : Submonoid A) : TensorProduct A (Localization S) (Localization T) →ₐ[A] Localization (S * T)

Equations

• Localization.tensorToLocalization S T = Algebra.TensorProduct.lift (IsLocalization.liftAlgHom ⋯) (IsLocalization.liftAlgHom ⋯) ⋯

@[simp]

theorem Localization.tensorToLocalization_tmul_mk_mk {A : Type u_1} [CommRing A] (S T : Submonoid A) (a b : A) (s : ↥S) (t : ↥T) : (Localization.tensorToLocalization S T) (Localization.mk a s ⊗ₜ[A] Localization.mk b t) = Localization.mk (a * b) ⟨↑s * ↑t, ⋯⟩

@[simp]

theorem Localization.tensorToLocalization_tmul_mk_one {A : Type u_1} [CommRing A] (S T : Submonoid A) (a : A) (s : ↥S) : (Localization.tensorToLocalization S T) (Localization.mk a s ⊗ₜ[A] 1) = Localization.mk a ⟨↑s, ⋯⟩

@[simp]

theorem Localization.tensorToLocalization_tmul_one_mk {A : Type u_1} [CommRing A] (S T : Submonoid A) (b : A) (t : ↥T) : (Localization.tensorToLocalization S T) (1 ⊗ₜ[A] Localization.mk b t) = Localization.mk b ⟨↑t, ⋯⟩

noncomputable def Localization.mulEquivTensor {A : Type u_1} [CommRing A] (S T : Submonoid A) : Localization (S * T) ≃ₐ[A] TensorProduct A (Localization S) (Localization T)

Equations

• Localization.mulEquivTensor S T = AlgEquiv.ofAlgHom (Localization.mulToTensor S T) (Localization.tensorToLocalization S T) ⋯ ⋯

@[simp]

theorem Localization.mulEquivTensor_apply {A : Type u_1} [CommRing A] (S T : Submonoid A) (x : Localization (S * T)) : (Localization.mulEquivTensor S T) x = (Localization.mulToTensor S T) x

@[simp]

theorem Localization.mulEquivTensor_symm_apply {A : Type u_1} [CommRing A] (S T : Submonoid A) (x : TensorProduct A (Localization S) (Localization T)) : (Localization.mulEquivTensor S T).symm x = (Localization.tensorToLocalization S T) x

noncomputable def Localization.mapEq {A : Type u_1} [CommRing A] {S T : Submonoid A} (eq : S = T) : Localization S →ₐ[A] Localization T

Equations

• Localization.mapEq eq = IsLocalization.liftAlgHom ⋯

@[simp]

theorem Localization.mapEq_mk {A : Type u_1} [CommRing A] (S T : Submonoid A) (eq : S = T) (x : A) (y : ↥S) : (Localization.mapEq eq) (Localization.mk x y) = Localization.mk x ⟨↑y, ⋯⟩

noncomputable def Localization.equivEq {A : Type u_1} [CommRing A] {S T : Submonoid A} (eq : S = T) : Localization S ≃ₐ[A] Localization T

Equations

• Localization.equivEq eq = AlgEquiv.ofAlgHom (Localization.mapEq eq) (Localization.mapEq ⋯) ⋯ ⋯

@[simp]

theorem Localization.equivEq_apply {A : Type u_1} [CommRing A] (S T : Submonoid A) (eq : S = T) (x : Localization S) : (Localization.equivEq eq) x = (Localization.mapEq eq) x

@[simp]

theorem Localization.equivEq_symm_apply {A : Type u_1} [CommRing A] (S T : Submonoid A) (eq : S = T) (x : Localization T) : (Localization.equivEq eq).symm x = (Localization.mapEq ⋯) x