From 0c13422e74d8bce916ee5bcea2a2ab5d032b280f Mon Sep 17 00:00:00 2001 From: artie2000 Date: Fri, 27 Dec 2024 10:44:58 +0000 Subject: [PATCH 1/3] add missing lemmas; clean up dot notation --- .../Algebra/Subalgebra/Unitization.lean | 30 +++++++++++++++++-- 1 file changed, 28 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean b/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean index 2cacd22757a8c..facb4429853a5 100644 --- a/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean +++ b/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean @@ -208,10 +208,36 @@ variable {R : Type*} [NonAssocSemiring R] def Subsemiring.toNonUnitalSubsemiring (S : Subsemiring R) : NonUnitalSubsemiring R := { S with } +theorem Subsemiring.toNonUnitalSubsemiring_injective : + Function.Injective (toNonUnitalSubsemiring : Subsemiring R → _) := + fun S₁ S₂ h => SetLike.ext'_iff.2 ( + show (S₁.toNonUnitalSubsemiring : Set R) = S₂ from SetLike.ext'_iff.1 h) + +@[simp] +theorem Subsemiring.toNonUnitalSubsemiring_eq {S₁ S₂ : Subsemiring R} : + S₁.toNonUnitalSubsemiring = S₂.toNonUnitalSubsemiring ↔ S₁ = S₂ := + toNonUnitalSubsemiring_injective.eq_iff + +@[simp] +theorem Subsemiring.mem_toNonUnitalSubsemiring {S : Subsemiring R} + {x : R} : x ∈ S.toNonUnitalSubsemiring ↔ x ∈ S := Iff.rfl + +@[simp] +theorem Subsemiring.coe_toNonUnitalSubsemiring (S : Subsemiring R) : + (S.toNonUnitalSubsemiring : Set R) = S := rfl + theorem Subsemiring.one_mem_toNonUnitalSubsemiring (S : Subsemiring R) : (1 : R) ∈ S.toNonUnitalSubsemiring := S.one_mem +@[simp] +theorem Submonoid.subsemiringClosure_toNonUnitalSubsemiring {M : Submonoid R} : + M.subsemiringClosure.toNonUnitalSubsemiring = .closure M := by + refine Eq.symm (NonUnitalSubsemiring.closure_eq_of_le ?_ (fun _ hx => ?_)) + · simp [Submonoid.subsemiringClosure_coe] + · simp [Submonoid.subsemiringClosure_mem] at hx + induction hx using AddSubmonoid.closure_induction <;> aesop + /-- Turn a non-unital subsemiring containing `1` into a subsemiring. -/ def NonUnitalSubsemiring.toSubsemiring (S : NonUnitalSubsemiring R) (h1 : (1 : R) ∈ S) : Subsemiring R := @@ -241,7 +267,7 @@ theorem unitization_apply (x : Unitization ℕ s) : unitization s x = x.fst + x. rfl theorem unitization_range : - (unitization s).range = subalgebraOfSubsemiring (Subsemiring.closure s) := by + (unitization s).range = subalgebraOfSubsemiring (.closure s) := by have := AddSubmonoidClass.nsmulMemClass (S := S) rw [unitization, NonUnitalSubalgebra.unitization_range (hSRA := this), Algebra.adjoin_nat] @@ -288,7 +314,7 @@ theorem unitization_apply (x : Unitization ℤ s) : unitization s x = x.fst + x. rfl theorem unitization_range : - (unitization s).range = subalgebraOfSubring (Subring.closure s) := by + (unitization s).range = subalgebraOfSubring (.closure s) := by have := AddSubgroupClass.zsmulMemClass (S := S) rw [unitization, NonUnitalSubalgebra.unitization_range (hSRA := this), Algebra.adjoin_int] From 8193df311606667bd30df327aea87b0ba849ac7c Mon Sep 17 00:00:00 2001 From: artie2000 Date: Fri, 27 Dec 2024 10:54:55 +0000 Subject: [PATCH 2/3] oops forgot a lemma --- Mathlib/Algebra/Ring/Subsemiring/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Algebra/Ring/Subsemiring/Basic.lean b/Mathlib/Algebra/Ring/Subsemiring/Basic.lean index 88035633f260c..db80142d9f7af 100644 --- a/Mathlib/Algebra/Ring/Subsemiring/Basic.lean +++ b/Mathlib/Algebra/Ring/Subsemiring/Basic.lean @@ -391,6 +391,10 @@ theorem subsemiringClosure_coe : (M.subsemiringClosure : Set R) = AddSubmonoid.closure (M : Set R) := rfl +theorem subsemiringClosure_mem {x : R} : + x ∈ M.subsemiringClosure ↔ x ∈ AddSubmonoid.closure (M : Set R) := + Iff.rfl + theorem subsemiringClosure_toAddSubmonoid : M.subsemiringClosure.toAddSubmonoid = AddSubmonoid.closure (M : Set R) := rfl From 0559d53153f0592ed68d3085fbedcce0914c14c1 Mon Sep 17 00:00:00 2001 From: Artie Khovanov Date: Sun, 29 Dec 2024 15:33:55 +0000 Subject: [PATCH 3/3] Update Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean b/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean index facb4429853a5..e1bf0603035cd 100644 --- a/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean +++ b/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean @@ -214,7 +214,7 @@ theorem Subsemiring.toNonUnitalSubsemiring_injective : show (S₁.toNonUnitalSubsemiring : Set R) = S₂ from SetLike.ext'_iff.1 h) @[simp] -theorem Subsemiring.toNonUnitalSubsemiring_eq {S₁ S₂ : Subsemiring R} : +theorem Subsemiring.toNonUnitalSubsemiring_inj {S₁ S₂ : Subsemiring R} : S₁.toNonUnitalSubsemiring = S₂.toNonUnitalSubsemiring ↔ S₁ = S₂ := toNonUnitalSubsemiring_injective.eq_iff