From c4bdcd50743c6c1a07cd3ad4480ab75cbbf2101b Mon Sep 17 00:00:00 2001 From: Xavier Roblot Date: Thu, 9 May 2024 12:28:41 +0200 Subject: [PATCH] 1st commit --- Mathlib/RingTheory/Ideal/Basic.lean | 19 ----- Mathlib/RingTheory/Ideal/Maps.lean | 66 +++++++++++++++ Mathlib/RingTheory/Ideal/Operations.lean | 102 ----------------------- 3 files changed, 66 insertions(+), 121 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Basic.lean b/Mathlib/RingTheory/Ideal/Basic.lean index c0b2d95f290c9..dc362ad99dd44 100644 --- a/Mathlib/RingTheory/Ideal/Basic.lean +++ b/Mathlib/RingTheory/Ideal/Basic.lean @@ -518,25 +518,6 @@ theorem span_singleton_eq_span_singleton {α : Type u} [CommRing α] [IsDomain apply and_congr <;> rw [span_singleton_le_span_singleton] #align ideal.span_singleton_eq_span_singleton Ideal.span_singleton_eq_span_singleton -/-- The equivalence between `Associates R` and the principal ideals of `R` defined by sending the -class of `x` to the principal ideal generated by `x`. -/ -noncomputable def associatesEquivIsPrincipal (R : Type*) [CommRing R] [IsDomain R] : - Associates R ≃ {I : Ideal R // Submodule.IsPrincipal I} := by - refine Equiv.ofBijective (fun x ↦ ⟨Ideal.span {Quot.out x}, ⟨Quot.out x, rfl⟩⟩) - ⟨fun _ _ h ↦ ?_, fun ⟨I, hI⟩ ↦ ?_⟩ - · rw [Subtype.mk_eq_mk, span_singleton_eq_span_singleton] at h - exact Quotient.out_equiv_out.mp h - · obtain ⟨x, hx⟩ := hI - refine ⟨⟦x⟧, ?_⟩ - rw [Subtype.mk_eq_mk, hx, submodule_span_eq, span_singleton_eq_span_singleton] - exact Associates.mk_quot_out x - -@[simp] -theorem associatesEquivIsPrincipal_apply (R : Type*) [CommRing R] [IsDomain R] (x : R) : - associatesEquivIsPrincipal R ⟦x⟧ = Ideal.span {x} := by - rw [associatesEquivIsPrincipal, Equiv.ofBijective_apply, span_singleton_eq_span_singleton] - exact Associates.mk_quot_out x - theorem span_singleton_mul_right_unit {a : α} (h2 : IsUnit a) (x : α) : span ({x * a} : Set α) = span {x} := by rw [mul_comm, span_singleton_mul_left_unit h2] #align ideal.span_singleton_mul_right_unit Ideal.span_singleton_mul_right_unit diff --git a/Mathlib/RingTheory/Ideal/Maps.lean b/Mathlib/RingTheory/Ideal/Maps.lean index 3f8ef20d79397..bd6c8aebf349e 100644 --- a/Mathlib/RingTheory/Ideal/Maps.lean +++ b/Mathlib/RingTheory/Ideal/Maps.lean @@ -911,3 +911,69 @@ lemma coe_ideal_map (I : Ideal A) : Ideal.map f I = Ideal.map (f : A →+* B) I := rfl end AlgHom + +noncomputable section IsPrincipal + +namespace Ideal + +open nonZeroDivisors Submodule + +variable (R : Type*) [CommRing R] [IsDomain R] + +/-- The equivalence between `Associates R` and the principal ideals of `R` defined by sending the +class of `x` to the principal ideal generated by `x`. -/ +noncomputable def associatesEquivIsPrincipal : + Associates R ≃ {I : Ideal R // IsPrincipal I} := by + refine Equiv.ofBijective (fun x ↦ ⟨Ideal.span {Quot.out x}, ⟨Quot.out x, rfl⟩⟩) + ⟨fun _ _ h ↦ ?_, fun ⟨I, hI⟩ ↦ ?_⟩ + · rw [Subtype.mk_eq_mk, span_singleton_eq_span_singleton] at h + exact Quotient.out_equiv_out.mp h + · obtain ⟨x, hx⟩ := hI + refine ⟨⟦x⟧, ?_⟩ + rw [Subtype.mk_eq_mk, hx, submodule_span_eq, span_singleton_eq_span_singleton] + exact Associates.mk_quot_out x + +@[simp] +theorem associatesEquivIsPrincipal_apply (x : R) : + associatesEquivIsPrincipal R ⟦x⟧ = Ideal.span {x} := by + rw [associatesEquivIsPrincipal, Equiv.ofBijective_apply, span_singleton_eq_span_singleton] + exact Associates.mk_quot_out x + +theorem associatesEquivIsPrincipal_mem_nonZeroDivisors {x : R} : + ↑(Ideal.associatesEquivIsPrincipal R ⟦x⟧) ∈ (Ideal R)⁰ ↔ x ∈ R⁰ := by + rw [Ideal.associatesEquivIsPrincipal_apply, mem_nonZeroDivisors_iff, mem_nonZeroDivisors_iff, + ← not_iff_not] + push_neg + refine ⟨fun ⟨I, hI₁, hI₂⟩ ↦ ?_, fun ⟨y, hy₁, hy₂⟩ ↦ ?_⟩ + · rw [Ideal.zero_eq_bot, Submodule.ne_bot_iff] at hI₂ + refine ⟨hI₂.choose, ?_, hI₂.choose_spec.2⟩ + · suffices hI₂.choose * x ∈ I * Ideal.span {x} by + rwa [hI₁] at this + rw [Ideal.mem_mul_span_singleton] + exact ⟨hI₂.choose, hI₂.choose_spec.1, rfl⟩ + · refine ⟨Ideal.span {y}, ?_, ?_⟩ + · rw [Ideal.span_singleton_mul_span_singleton, hy₁, Set.singleton_zero, Ideal.span_zero, + Ideal.zero_eq_bot] + · rw [Ideal.zero_eq_bot, Submodule.ne_bot_iff] + exact ⟨y, Ideal.mem_span_singleton_self y, hy₂⟩ + +/-- A version of `Ideal.associatesEquivIsPrincipal` for non-zero-divisor generators. -/ +def associatesNonZeroDivisorsEquivIsPrincipal : + Associates R⁰ ≃ {I : (Ideal R)⁰ // IsPrincipal (I : Ideal R)} := + calc Associates R⁰ ≃ (Associates R)⁰ := (AssociatesNonZeroDivisorsMulEquiv R).toEquiv + _ ≃ {I : {I : Ideal R // IsPrincipal I} // I.1 ∈ (Ideal R)⁰} := + Equiv.subtypeEquiv (Ideal.associatesEquivIsPrincipal R) + (fun x ↦ by rw [← Associates.quot_out x, Associates_mk_mem_nonZeroDivisors_iff, + Ideal.associatesEquivIsPrincipal_mem_nonZeroDivisors]) + _ ≃ {I : Ideal R // IsPrincipal I ∧ I ∈ (Ideal R)⁰} := + Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ IsPrincipal I) (fun I ↦ I ∈ (Ideal R)⁰) + _ ≃ {I : Ideal R // I ∈ (Ideal R)⁰ ∧ IsPrincipal I} := Equiv.setCongr (by simp_rw [and_comm]) + _ ≃ {I : (Ideal R)⁰ // IsPrincipal I.1} := (Equiv.subtypeSubtypeEquivSubtypeInter _ _).symm + +@[simp] +theorem associatesNonZeroDivisorsEquivIsPrincipal_apply (x : R⁰) : + Ideal.associatesNonZeroDivisorsEquivIsPrincipal R ⟦x⟧ = Ideal.span {(x : R)} := by + rw [← Ideal.associatesEquivIsPrincipal_apply] + rfl + +end Ideal diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean index 3aa9aa3f8690a..dba1683177de7 100644 --- a/Mathlib/RingTheory/Ideal/Operations.lean +++ b/Mathlib/RingTheory/Ideal/Operations.lean @@ -1388,105 +1388,3 @@ lemma span_smul_eq rw [← coe_set_smul, coe_span_smul] end Submodule - -namespace RingHom - -variable {A B C : Type*} [Ring A] [Ring B] [Ring C] -variable (f : A →+* B) (f_inv : B → A) - -/-- Auxiliary definition used to define `liftOfRightInverse` -/ -def liftOfRightInverseAux (hf : Function.RightInverse f_inv f) (g : A →+* C) - (hg : RingHom.ker f ≤ RingHom.ker g) : - B →+* C := - { AddMonoidHom.liftOfRightInverse f.toAddMonoidHom f_inv hf ⟨g.toAddMonoidHom, hg⟩ with - toFun := fun b => g (f_inv b) - map_one' := by - rw [← map_one g, ← sub_eq_zero, ← map_sub g, ← mem_ker g] - apply hg - rw [mem_ker f, map_sub f, sub_eq_zero, map_one f] - exact hf 1 - map_mul' := by - intro x y - rw [← map_mul g, ← sub_eq_zero, ← map_sub g, ← mem_ker g] - apply hg - rw [mem_ker f, map_sub f, sub_eq_zero, map_mul f] - simp only [hf _] } -#align ring_hom.lift_of_right_inverse_aux RingHom.liftOfRightInverseAux - -@[simp] -theorem liftOfRightInverseAux_comp_apply (hf : Function.RightInverse f_inv f) (g : A →+* C) - (hg : RingHom.ker f ≤ RingHom.ker g) (a : A) : - (f.liftOfRightInverseAux f_inv hf g hg) (f a) = g a := - f.toAddMonoidHom.liftOfRightInverse_comp_apply f_inv hf ⟨g.toAddMonoidHom, hg⟩ a -#align ring_hom.lift_of_right_inverse_aux_comp_apply RingHom.liftOfRightInverseAux_comp_apply - -/-- `liftOfRightInverse f hf g hg` is the unique ring homomorphism `φ` - -* such that `φ.comp f = g` (`RingHom.liftOfRightInverse_comp`), -* where `f : A →+* B` has a right_inverse `f_inv` (`hf`), -* and `g : B →+* C` satisfies `hg : f.ker ≤ g.ker`. - -See `RingHom.eq_liftOfRightInverse` for the uniqueness lemma. - -``` - A . - | \ - f | \ g - | \ - v \⌟ - B ----> C - ∃!φ -``` --/ -def liftOfRightInverse (hf : Function.RightInverse f_inv f) : - { g : A →+* C // RingHom.ker f ≤ RingHom.ker g } ≃ (B →+* C) where - toFun g := f.liftOfRightInverseAux f_inv hf g.1 g.2 - invFun φ := ⟨φ.comp f, fun x hx => (mem_ker _).mpr <| by simp [(mem_ker _).mp hx]⟩ - left_inv g := by - ext - simp only [comp_apply, liftOfRightInverseAux_comp_apply, Subtype.coe_mk] - right_inv φ := by - ext b - simp [liftOfRightInverseAux, hf b] -#align ring_hom.lift_of_right_inverse RingHom.liftOfRightInverse - -/-- A non-computable version of `RingHom.liftOfRightInverse` for when no computable right -inverse is available, that uses `Function.surjInv`. -/ -@[simp] -noncomputable abbrev liftOfSurjective (hf : Function.Surjective f) : - { g : A →+* C // RingHom.ker f ≤ RingHom.ker g } ≃ (B →+* C) := - f.liftOfRightInverse (Function.surjInv hf) (Function.rightInverse_surjInv hf) -#align ring_hom.lift_of_surjective RingHom.liftOfSurjective - -theorem liftOfRightInverse_comp_apply (hf : Function.RightInverse f_inv f) - (g : { g : A →+* C // RingHom.ker f ≤ RingHom.ker g }) (x : A) : - (f.liftOfRightInverse f_inv hf g) (f x) = g.1 x := - f.liftOfRightInverseAux_comp_apply f_inv hf g.1 g.2 x -#align ring_hom.lift_of_right_inverse_comp_apply RingHom.liftOfRightInverse_comp_apply - -theorem liftOfRightInverse_comp (hf : Function.RightInverse f_inv f) - (g : { g : A →+* C // RingHom.ker f ≤ RingHom.ker g }) : - (f.liftOfRightInverse f_inv hf g).comp f = g := - RingHom.ext <| f.liftOfRightInverse_comp_apply f_inv hf g -#align ring_hom.lift_of_right_inverse_comp RingHom.liftOfRightInverse_comp - -theorem eq_liftOfRightInverse (hf : Function.RightInverse f_inv f) (g : A →+* C) - (hg : RingHom.ker f ≤ RingHom.ker g) (h : B →+* C) (hh : h.comp f = g) : - h = f.liftOfRightInverse f_inv hf ⟨g, hg⟩ := by - simp_rw [← hh] - exact ((f.liftOfRightInverse f_inv hf).apply_symm_apply _).symm -#align ring_hom.eq_lift_of_right_inverse RingHom.eq_liftOfRightInverse - -end RingHom - -namespace AlgHom - -variable {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B] - [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) - -lemma coe_ker : RingHom.ker f = RingHom.ker (f : A →+* B) := rfl - -lemma coe_ideal_map (I : Ideal A) : - Ideal.map f I = Ideal.map (f : A →+* B) I := rfl - -end AlgHom