From ad588611ac446ff7954044c9e1fc0ab0dcd9a9cf Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 21 Apr 2021 00:48:46 +0000 Subject: [PATCH] refactor(group_theory/submonoid): adjust definitional unfolding of add_monoid_hom.mrange to match set.range (#7227) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This changes the following to unfold to `set.range`: * `monoid_hom.mrange` * `add_monoid_hom.mrange` * `linear_map.range` * `lie_hom.range` * `ring_hom.range` * `ring_hom.srange` * `ring_hom.field_range` * `alg_hom.range` For example: ```lean import ring_theory.subring variables (R : Type*) [ring R] (f : R →+* R) -- before this PR, these required `f '' univ` on the RHS example : (f.range : set R) = set.range f := rfl example : (f.srange : set R) = set.range f := rfl example : (f.to_monoid_hom.mrange : set R) = set.range f := rfl -- this one is unchanged by this PR example : (f.to_add_monoid_hom.range : set R) = set.range f := rfl ``` The motivations behind this change are that * It eliminates a lot of `∈ set.univ` hypotheses and goals that are just annoying * it means that an equivalence like `A ≃ set.range f` is defeq to `A ≃ f.range`, with no need to insert awkward `equiv.cast`-like terms to translate between different approaches * `monoid_hom.range` (as opposed to `mrange`) already used this pattern. The number of lines has gone up a bit, but most of those are comments explaining the design choice. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60set.2Erange.20f.60.20vs.20.60f.20''.20univ.60/near/234893679) --- src/algebra/algebra/subalgebra.lean | 6 +-- src/algebra/algebra/tower.lean | 3 +- src/algebra/lie/nilpotent.lean | 4 +- src/algebra/lie/solvable.lean | 5 +- src/algebra/lie/subalgebra.lean | 3 ++ src/algebra/lie/submodule.lean | 20 ++++++-- src/field_theory/adjoin.lean | 9 ++-- src/field_theory/minpoly.lean | 2 +- src/field_theory/normal.lean | 6 +-- src/field_theory/splitting_field.lean | 2 +- src/field_theory/subfield.lean | 20 +++++--- src/group_theory/congruence.lean | 7 +-- src/group_theory/submonoid/membership.lean | 12 ++--- src/group_theory/submonoid/operations.lean | 34 ++++++++----- src/linear_algebra/basic.lean | 55 +++++++++++++--------- src/linear_algebra/basis.lean | 2 +- src/linear_algebra/bilinear_form.lean | 5 +- src/linear_algebra/dimension.lean | 6 +-- src/linear_algebra/dual.lean | 6 +-- src/linear_algebra/eigenspace.lean | 2 +- src/linear_algebra/finsupp.lean | 17 ++++--- src/linear_algebra/linear_independent.lean | 4 +- src/linear_algebra/prod.lean | 6 +-- src/ring_theory/adjoin/basic.lean | 8 ++-- src/ring_theory/adjoin_root.lean | 2 +- src/ring_theory/noetherian.lean | 2 +- src/ring_theory/subring.lean | 19 +++++--- src/ring_theory/subsemiring.lean | 15 ++++-- 28 files changed, 166 insertions(+), 116 deletions(-) diff --git a/src/algebra/algebra/subalgebra.lean b/src/algebra/algebra/subalgebra.lean index 5da44024642e7..2b15b7c1ee972 100644 --- a/src/algebra/algebra/subalgebra.lean +++ b/src/algebra/algebra/subalgebra.lean @@ -56,7 +56,7 @@ theorem algebra_map_mem (r : R) : algebra_map R A r ∈ S := S.algebra_map_mem' r theorem srange_le : (algebra_map R A).srange ≤ S.to_subsemiring := -λ x ⟨r, _, hr⟩, hr ▸ S.algebra_map_mem r +λ x ⟨r, hr⟩, hr ▸ S.algebra_map_mem r theorem range_subset : set.range (algebra_map R A) ⊆ S := λ x ⟨r, hr⟩, hr ▸ S.algebra_map_mem r @@ -349,7 +349,7 @@ variables (φ : A →ₐ[R] B) /-- Range of an `alg_hom` as a subalgebra. -/ protected def range (φ : A →ₐ[R] B) : subalgebra R B := -{ algebra_map_mem' := λ r, ⟨algebra_map R A r, set.mem_univ _, φ.commutes r⟩, +{ algebra_map_mem' := λ r, ⟨algebra_map R A r, φ.commutes r⟩, .. φ.to_ring_hom.srange } @[simp] lemma mem_range (φ : A →ₐ[R] B) {y : B} : @@ -497,7 +497,7 @@ theorem eq_top_iff {S : subalgebra R A} : @[simp] theorem map_top (f : A →ₐ[R] B) : subalgebra.map (⊤ : subalgebra R A) f = f.range := subalgebra.ext $ λ x, - ⟨λ ⟨y, _, hy⟩, ⟨y, set.mem_univ _, hy⟩, λ ⟨y, mem, hy⟩, ⟨y, algebra.mem_top, hy⟩⟩ + ⟨λ ⟨y, _, hy⟩, ⟨y, hy⟩, λ ⟨y, hy⟩, ⟨y, algebra.mem_top, hy⟩⟩ @[simp] theorem map_bot (f : A →ₐ[R] B) : subalgebra.map (⊥ : subalgebra R A) f = ⊥ := eq_bot_iff.2 $ λ x ⟨y, hy, hfy⟩, let ⟨r, hr⟩ := mem_bot.1 hy in subalgebra.range_le _ diff --git a/src/algebra/algebra/tower.lean b/src/algebra/algebra/tower.lean index e57cbb3a5fed9..55a4059e6593b 100644 --- a/src/algebra/algebra/tower.lean +++ b/src/algebra/algebra/tower.lean @@ -262,8 +262,7 @@ show z ∈ subsemiring.closure (set.range (algebra_map (to_alg_hom R S A).range z ∈ subsemiring.closure (set.range (algebra_map S A) ∪ t : set A), from suffices set.range (algebra_map (to_alg_hom R S A).range A) = set.range (algebra_map S A), by rw this, -by { ext z, exact ⟨λ ⟨⟨x, y, _, h1⟩, h2⟩, ⟨y, h2 ▸ h1⟩, λ ⟨y, hy⟩, - ⟨⟨z, y, set.mem_univ _, hy⟩, rfl⟩⟩ } +by { ext z, exact ⟨λ ⟨⟨x, y, h1⟩, h2⟩, ⟨y, h2 ▸ h1⟩, λ ⟨y, hy⟩, ⟨⟨z, y, hy⟩, rfl⟩⟩ } end is_scalar_tower diff --git a/src/algebra/lie/nilpotent.lean b/src/algebra/lie/nilpotent.lean index 8bc4d4727a4e9..477f5d0c7d2e0 100644 --- a/src/algebra/lie/nilpotent.lean +++ b/src/algebra/lie/nilpotent.lean @@ -110,7 +110,9 @@ lemma lie_ideal.lower_central_series_map_eq (k : ℕ) {f : L →ₗ⁅R⁆ L'} (h : function.surjective f) : lie_ideal.map f (lower_central_series R L L k) = lower_central_series R L' L' k := begin - have h' : (⊤ : lie_ideal R L).map f = ⊤, { exact f.ideal_range_eq_top_of_surjective h, }, + have h' : (⊤ : lie_ideal R L).map f = ⊤, + { rw ←f.ideal_range_eq_map, + exact f.ideal_range_eq_top_of_surjective h, }, induction k with k ih, { simp only [lie_module.lower_central_series_zero], exact h', }, { simp only [lie_module.lower_central_series_succ, lie_ideal.map_bracket_eq f h, ih, h'], }, diff --git a/src/algebra/lie/solvable.lean b/src/algebra/lie/solvable.lean index 72d7983cc0834..c86d78d44197e 100644 --- a/src/algebra/lie/solvable.lean +++ b/src/algebra/lie/solvable.lean @@ -171,9 +171,10 @@ end lemma derived_series_map_eq (k : ℕ) (h : function.surjective f) : (derived_series R L' k).map f = derived_series R L k := begin - have h' : (⊤ : lie_ideal R L').map f = ⊤, { exact f.ideal_range_eq_top_of_surjective h, }, induction k with k ih, - { exact h', }, + { change (⊤ : lie_ideal R L').map f = ⊤, + rw ←f.ideal_range_eq_map, + exact f.ideal_range_eq_top_of_surjective h, }, { simp only [derived_series_def, map_bracket_eq f h, ih, derived_series_of_ideal_succ], }, end diff --git a/src/algebra/lie/subalgebra.lean b/src/algebra/lie/subalgebra.lean index 736379c01d60b..4f31bdb83b3fa 100644 --- a/src/algebra/lie/subalgebra.lean +++ b/src/algebra/lie/subalgebra.lean @@ -259,6 +259,9 @@ instance : has_top (lie_subalgebra R L) := @[simp] lemma mem_top (x : L) : x ∈ (⊤ : lie_subalgebra R L) := mem_univ x +lemma _root_.lie_hom.range_eq_map : f.range = map f ⊤ := +by { ext, simp } + instance : has_inf (lie_subalgebra R L) := ⟨λ K K', { lie_mem' := λ x y hx hy, mem_inter (K.lie_mem hx.1 hy.1) (K'.lie_mem hx.2 hy.2), ..(K ⊓ K' : submodule R L) }⟩ diff --git a/src/algebra/lie/submodule.lean b/src/algebra/lie/submodule.lean index 3a99d0b13dad9..b8c0926d16777 100644 --- a/src/algebra/lie/submodule.lean +++ b/src/algebra/lie/submodule.lean @@ -506,11 +506,15 @@ variables (f : L →ₗ⁅R⁆ L') (I : lie_ideal R L) (J : lie_ideal R L') def ker : lie_ideal R L := lie_ideal.comap f ⊥ /-- The range of a morphism of Lie algebras as an ideal in the codomain. -/ -def ideal_range : lie_ideal R L' := lie_ideal.map f ⊤ +def ideal_range : lie_ideal R L' := lie_submodule.lie_span R L' f.range lemma ideal_range_eq_lie_span_range : f.ideal_range = lie_submodule.lie_span R L' f.range := rfl +lemma ideal_range_eq_map : + f.ideal_range = lie_ideal.map f ⊤ := +by { ext, simp only [ideal_range, range_eq_map], refl } + /-- The condition that the image of a morphism of Lie algebras is an ideal. -/ def is_ideal_morphism : Prop := (f.ideal_range : lie_subalgebra R L') = f.range @@ -532,7 +536,11 @@ end lemma range_subset_ideal_range : (f.range : set L') ⊆ f.ideal_range := lie_submodule.subset_lie_span -lemma map_le_ideal_range : I.map f ≤ f.ideal_range := lie_ideal.map_mono le_top +lemma map_le_ideal_range : I.map f ≤ f.ideal_range := +begin + rw f.ideal_range_eq_map, + exact lie_ideal.map_mono le_top, +end lemma ker_le_comap : f.ker ≤ J.comap f := lie_ideal.comap_mono bot_le @@ -542,7 +550,11 @@ lemma ker_le_comap : f.ker ≤ J.comap f := lie_ideal.comap_mono bot_le show x ∈ (f.ker : submodule R L) ↔ _, by simp only [ker_coe_submodule, linear_map.mem_ker, coe_to_linear_map] -lemma mem_ideal_range {x : L} : f x ∈ ideal_range f := lie_ideal.mem_map (lie_submodule.mem_top x) +lemma mem_ideal_range {x : L} : f x ∈ ideal_range f := +begin + rw ideal_range_eq_map, + exact lie_ideal.mem_map (lie_submodule.mem_top x) +end @[simp] lemma mem_ideal_range_iff (h : is_ideal_morphism f) {y : L'} : y ∈ ideal_range f ↔ ∃ (x : L), f x = y := @@ -663,7 +675,7 @@ begin { rw le_inf_iff, exact ⟨f.map_le_ideal_range _, map_comap_le⟩, }, { rw f.is_ideal_morphism_def at h, rw [lie_submodule.le_def, lie_submodule.inf_coe, ← coe_to_subalgebra, h], - rintros y ⟨⟨x, h₁, h₂⟩, h₃⟩, rw ← h₂ at h₃ ⊢, exact mem_map h₃, }, + rintros y ⟨⟨x, h₁⟩, h₂⟩, rw ← h₁ at h₂ ⊢, exact mem_map h₂, }, end @[simp] lemma comap_map_eq (h : ↑(map f I) = f '' I) : comap f (map f I) = I ⊔ f.ker := diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 44c361c398d03..1f2d008f38a2f 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -434,12 +434,11 @@ alg_equiv.of_bijective (alg_hom.mk (adjoin_root.lift (algebra_map F F⟮α⟯) split, { exact ring_hom.injective f }, { suffices : F⟮α⟯.to_subfield ≤ ring_hom.field_range ((F⟮α⟯.to_subfield.subtype).comp f), - { exact λ x, Exists.cases_on (this (subtype.mem x)) (λ y hy, ⟨y, subtype.ext hy.2⟩) }, - exact subfield.closure_le.mpr (set.union_subset (λ x hx, Exists.cases_on hx (λ y hy, ⟨y, - ⟨subfield.mem_top y, by { rw [ring_hom.comp_apply, adjoin_root.lift_of], exact hy }⟩⟩)) + { exact λ x, Exists.cases_on (this (subtype.mem x)) (λ y hy, ⟨y, subtype.ext hy⟩) }, + exact subfield.closure_le.mpr (set.union_subset (λ x hx, Exists.cases_on hx (λ y hy, + ⟨y, by { rw [ring_hom.comp_apply, adjoin_root.lift_of], exact hy }⟩)) (set.singleton_subset_iff.mpr ⟨adjoin_root.root (minpoly F α), - ⟨subfield.mem_top (adjoin_root.root (minpoly F α)), - by { rw [ring_hom.comp_apply, adjoin_root.lift_root], refl }⟩⟩)) } end) + by { rw [ring_hom.comp_apply, adjoin_root.lift_root], refl }⟩)) } end) lemma adjoin_root_equiv_adjoin_apply_root (h : is_integral F α) : adjoin_root_equiv_adjoin F h (adjoin_root.root (minpoly F α)) = diff --git a/src/field_theory/minpoly.lean b/src/field_theory/minpoly.lean index 1b51730405825..ffb872930817a 100644 --- a/src/field_theory/minpoly.lean +++ b/src/field_theory/minpoly.lean @@ -74,7 +74,7 @@ begin have key := minpoly.aeval A x, rw [eq_X_add_C_of_degree_eq_one hx, (minpoly.monic h).leading_coeff, C_1, one_mul, aeval_add, aeval_C, aeval_X, ←eq_neg_iff_add_eq_zero, ←ring_hom.map_neg] at key, - exact ⟨-(minpoly A x).coeff 0, subring.mem_top (-(minpoly A x).coeff 0), key.symm⟩, + exact ⟨-(minpoly A x).coeff 0, key.symm⟩, end /--The defining property of the minimal polynomial of an element x: diff --git a/src/field_theory/normal.lean b/src/field_theory/normal.lean index 23ffeba7e77bd..26fdaed222c2e 100644 --- a/src/field_theory/normal.lean +++ b/src/field_theory/normal.lean @@ -99,7 +99,7 @@ lemma alg_hom.normal_bijective [h : normal F E] (ϕ : E →ₐ[F] K) : function. { rw [ring_hom.map_zero, aeval_map, ←is_scalar_tower.to_alg_hom_apply F K E, ←alg_hom.comp_apply, ←aeval_alg_hom], exact minpoly.aeval F (algebra_map K E x) })))) with y hy, - exact ⟨y, hy.2⟩ }⟩ + exact ⟨y, hy⟩ }⟩ variables {F} {E} {E' : Type*} [field E'] [algebra F E'] @@ -200,7 +200,7 @@ def alg_hom.restrict_normal_aux [h : normal F E] : { to_fun := λ x, ⟨ϕ x, by { suffices : (to_alg_hom F E K).range.map ϕ ≤ _, { exact this ⟨x, subtype.mem x, rfl⟩ }, - rintros x ⟨y, ⟨z, -, hy⟩, hx⟩, + rintros x ⟨y, ⟨z, hy⟩, hx⟩, rw [←hx, ←hy], apply minpoly.mem_range_of_degree_eq_one E, exact or.resolve_left (h.splits z) (minpoly.ne_zero (h.is_integral z)) @@ -224,7 +224,7 @@ def alg_hom.restrict_normal [normal F E] : E →ₐ[F] E := algebra_map E K (ϕ.restrict_normal E x) = ϕ (algebra_map E K x) := subtype.ext_iff.mp (alg_equiv.apply_symm_apply (alg_equiv.of_injective_field (is_scalar_tower.to_alg_hom F E K)) (ϕ.restrict_normal_aux E - ⟨is_scalar_tower.to_alg_hom F E K x, ⟨x, ⟨subsemiring.mem_top x, rfl⟩⟩⟩)) + ⟨is_scalar_tower.to_alg_hom F E K x, x, rfl⟩)) lemma alg_hom.restrict_normal_comp [normal F E] : (ϕ.restrict_normal E).comp (ψ.restrict_normal E) = (ϕ.comp ψ).restrict_normal E := diff --git a/src/field_theory/splitting_field.lean b/src/field_theory/splitting_field.lean index a744680255b0c..f65694a9a7fb7 100644 --- a/src/field_theory/splitting_field.lean +++ b/src/field_theory/splitting_field.lean @@ -447,7 +447,7 @@ alg_equiv.symm $ alg_equiv.of_bijective adjoin_root.induction_on _ p $ λ p hp, ideal.quotient.eq_zero_iff_mem.2 $ ideal.mem_span_singleton.2 $ minpoly.dvd F x hp, λ y, - let ⟨p, _, hp⟩ := (set_like.ext_iff.1 (algebra.adjoin_singleton_eq_range F x) (y : R)).1 y.2 in + let ⟨p, hp⟩ := (set_like.ext_iff.1 (algebra.adjoin_singleton_eq_range F x) (y : R)).1 y.2 in ⟨adjoin_root.mk _ p, subtype.eq hp⟩⟩ open finset diff --git a/src/field_theory/subfield.lean b/src/field_theory/subfield.lean index aa4103c8c4e00..661414d61d2be 100644 --- a/src/field_theory/subfield.lean +++ b/src/field_theory/subfield.lean @@ -287,15 +287,21 @@ variables (g : L →+* M) (f : K →+* L) /-! # range -/ /-- The range of a ring homomorphism, as a subfield of the target. -/ -def field_range : subfield L := (⊤ : subfield K).map f +def field_range : subfield L := +((⊤ : subfield K).map f).copy (set.range f) set.image_univ.symm -@[simp] lemma coe_field_range : (f.field_range : set L) = set.range f := set.image_univ +/-- Note that `ring_hom.field_range` is deliberately defined in a way that makes this true by `rfl`, +as this means the types `↥(set.range f)` and `↥f.field_range` are interchangeable without proof +obligations. -/ +@[simp] lemma coe_field_range : (f.field_range : set L) = set.range f := rfl -@[simp] lemma mem_field_range {f : K →+* L} {y : L} : y ∈ f.range ↔ ∃ x, f x = y := -by simp [range] +@[simp] lemma mem_field_range {f : K →+* L} {y : L} : y ∈ f.field_range ↔ ∃ x, f x = y := iff.rfl + +lemma field_range_eq_map : f.field_range = subfield.map f ⊤ := +by { ext, simp } lemma map_field_range : f.field_range.map g = (g.comp f).field_range := -(⊤ : subfield K).map_map g f +by simpa only [field_range_eq_map] using (⊤ : subfield K).map_map g f end ring_hom @@ -549,8 +555,8 @@ def restrict_field (f : K →+* L) (s : subfield K) : s →+* L := f.comp s.subt @[simp] lemma restrict_field_apply (f : K →+* L) (x : s) : f.restrict_field s x = f x := rfl /-- Restriction of a ring homomorphism to its range interpreted as a subfield. -/ -def range_restrict_field (f : K →+* L) : K →+* f.range := -f.cod_restrict' f.range $ λ x, ⟨x, subfield.mem_top x, rfl⟩ +def range_restrict_field (f : K →+* L) : K →+* f.field_range := +f.srange_restrict @[simp] lemma coe_range_restrict_field (f : K →+* L) (x : K) : (f.range_restrict_field x : L) = f x := rfl diff --git a/src/group_theory/congruence.lean b/src/group_theory/congruence.lean index 57519d86fbe36..e3e9751a7a476 100644 --- a/src/group_theory/congruence.lean +++ b/src/group_theory/congruence.lean @@ -727,10 +727,7 @@ lift_funext g (c.lift f H) $ λ x, by rw [lift_coe H, ←comp_mk'_apply, Hg] constant on `c`'s equivalence classes, `f` has the same image as the homomorphism that `f` induces on the quotient."] theorem lift_range (H : c ≤ ker f) : (c.lift f H).mrange = f.mrange := -submonoid.ext $ λ x, - ⟨λ ⟨y, hy⟩, by revert hy; rcases y; exact - λ hy, ⟨y, hy.1, by rw [hy.2.symm, ←lift_coe H]; refl⟩, - λ ⟨y, hy⟩, ⟨↑y, hy.1, by rw ←hy.2; refl⟩⟩ +submonoid.ext $ λ x, ⟨by rintros ⟨⟨y⟩, hy⟩; exact ⟨y, hy⟩, λ ⟨y, hy⟩, ⟨↑y, hy⟩⟩ /-- Surjective monoid homomorphisms constant on a congruence relation `c`'s equivalence classes induce a surjective homomorphism on `c`'s quotient. -/ @@ -810,7 +807,7 @@ noncomputable def quotient_ker_equiv_range (f : M →* P) : (ker f).quotient ≃ $ mul_equiv.submonoid_congr ker_lift_range_eq).comp (ker_lift f).mrange_restrict) $ (equiv.bijective _).comp ⟨λ x y h, ker_lift_injective f $ by rcases x; rcases y; injections, - λ ⟨w, z, hzm, hz⟩, ⟨z, by rcases hz; rcases _x; refl⟩⟩ } + λ ⟨w, z, hz⟩, ⟨z, by rcases hz; rcases _x; refl⟩⟩ } /-- The first isomorphism theorem for monoids in the case of a surjective homomorphism. -/ @[to_additive "The first isomorphism theorem for `add_monoid`s in the case of a surjective diff --git a/src/group_theory/submonoid/membership.lean b/src/group_theory/submonoid/membership.lean index 3f96f81189f73..218d85f1d1186 100644 --- a/src/group_theory/submonoid/membership.lean +++ b/src/group_theory/submonoid/membership.lean @@ -170,8 +170,8 @@ variables [monoid M] open monoid_hom lemma closure_singleton_eq (x : M) : closure ({x} : set M) = (powers_hom M x).mrange := -closure_eq_of_le (set.singleton_subset_iff.2 ⟨multiplicative.of_add 1, trivial, pow_one x⟩) $ - λ x ⟨n, _, hn⟩, hn ▸ pow_mem _ (subset_closure $ set.mem_singleton _) _ +closure_eq_of_le (set.singleton_subset_iff.2 ⟨multiplicative.of_add 1, pow_one x⟩) $ + λ x ⟨n, hn⟩, hn ▸ pow_mem _ (subset_closure $ set.mem_singleton _) _ /-- The submonoid generated by an element of a monoid equals the set of natural number powers of the element. -/ @@ -186,7 +186,7 @@ by simp [eq_bot_iff_forall, mem_closure_singleton] @[to_additive] lemma closure_eq_mrange (s : set M) : closure s = (free_monoid.lift (coe : s → M)).mrange := -by rw [mrange, ← free_monoid.closure_range_of, map_mclosure, ← set.range_comp, +by rw [mrange_eq_map, ← free_monoid.closure_range_of, map_mclosure, ← set.range_comp, free_monoid.lift_comp_of, subtype.range_coe] @[to_additive] @@ -221,7 +221,7 @@ open monoid_hom @[to_additive] lemma sup_eq_range (s t : submonoid N) : s ⊔ t = (s.subtype.coprod t.subtype).mrange := -by rw [mrange, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, +by rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange, coprod_comp_inr, range_subtype, range_subtype] @[to_additive] @@ -244,8 +244,8 @@ lemma nsmul_mem (S : add_submonoid A) {x : A} (hx : x ∈ S) : | (n+1) := by { rw [add_nsmul, one_nsmul], exact S.add_mem (nsmul_mem n) hx } lemma closure_singleton_eq (x : A) : closure ({x} : set A) = (multiples_hom A x).mrange := -closure_eq_of_le (set.singleton_subset_iff.2 ⟨1, trivial, one_nsmul x⟩) $ - λ x ⟨n, _, hn⟩, hn ▸ nsmul_mem _ (subset_closure $ set.mem_singleton _) _ +closure_eq_of_le (set.singleton_subset_iff.2 ⟨1, one_nsmul x⟩) $ + λ x ⟨n, hn⟩, hn ▸ nsmul_mem _ (subset_closure $ set.mem_singleton _) _ /-- The `add_submonoid` generated by an element of an `add_monoid` equals the set of natural number multiples of the element. -/ diff --git a/src/group_theory/submonoid/operations.lean b/src/group_theory/submonoid/operations.lean index bc05556d11c56..f235a08f981aa 100644 --- a/src/group_theory/submonoid/operations.lean +++ b/src/group_theory/submonoid/operations.lean @@ -546,19 +546,32 @@ open submonoid /-- The range of a monoid homomorphism is a submonoid. -/ @[to_additive "The range of an `add_monoid_hom` is an `add_submonoid`."] -def mrange (f : M →* N) : submonoid N := (⊤ : submonoid M).map f +def mrange (f : M →* N) : submonoid N := +((⊤ : submonoid M).map f).copy (set.range f) set.image_univ.symm -@[simp, to_additive] lemma coe_mrange (f : M →* N) : +/-- Note that `monoid_hom.mrange` is deliberately defined in a way that makes this true by `rfl`, +as this means the types `↥(set.range f)` and `↥f.mrange` are interchangeable without proof +obligations. -/ +@[simp, to_additive] +lemma coe_mrange (f : M →* N) : (f.mrange : set N) = set.range f := -set.image_univ +rfl + +/-- Note that `add_monoid_hom.mrange` is deliberately defined in a way that makes this true by +`rfl`, as this means the types `↥(set.range f)` and `↥f.mrange` are interchangeable without proof +obligations. -/ +add_decl_doc add_monoid_hom.coe_mrange @[simp, to_additive] lemma mem_mrange {f : M →* N} {y : N} : y ∈ f.mrange ↔ ∃ x, f x = y := -by simp [mrange] +iff.rfl + +@[to_additive] lemma mrange_eq_map (f : M →* N) : f.mrange = (⊤ : submonoid M).map f := +by ext; simp @[to_additive] lemma map_mrange (g : N →* P) (f : M →* N) : f.mrange.map g = (g.comp f).mrange := -(⊤ : submonoid M).map_map g f +by simpa only [mrange_eq_map] using (⊤ : submonoid M).map_map g f @[to_additive] lemma mrange_top_iff_surjective {N} [mul_one_class N] {f : M →* N} : @@ -571,9 +584,6 @@ lemma mrange_top_of_surjective {N} [mul_one_class N] (f : M →* N) (hf : functi f.mrange = (⊤ : submonoid N) := mrange_top_iff_surjective.2 hf -@[to_additive] -lemma mrange_eq_map (f : M →* N) : f.mrange = map f ⊤ := rfl - @[to_additive] lemma mclosure_preimage_le (f : M →* N) (s : set N) : closure (f ⁻¹' s) ≤ (closure s).comap f := @@ -609,7 +619,7 @@ def cod_mrestrict (f : M →* N) (S : submonoid N) (h : ∀ x, f x ∈ S) : M /-- Restriction of a monoid hom to its range interpreted as a submonoid. -/ @[to_additive "Restriction of an `add_monoid` hom to its range interpreted as a submonoid."] def mrange_restrict {N} [mul_one_class N] (f : M →* N) : M →* f.mrange := -f.cod_mrestrict f.mrange $ λ x, ⟨x, submonoid.mem_top x, rfl⟩ +f.cod_mrestrict f.mrange $ λ x, ⟨x, rfl⟩ @[simp, to_additive] lemma coe_mrange_restrict {N} [mul_one_class N] (f : M →* N) (x : M) : @@ -622,10 +632,12 @@ namespace submonoid open monoid_hom @[to_additive] -lemma mrange_inl : (inl M N).mrange = prod ⊤ ⊥ := map_inl ⊤ +lemma mrange_inl : (inl M N).mrange = prod ⊤ ⊥ := +by simpa only [mrange_eq_map] using map_inl ⊤ @[to_additive] -lemma mrange_inr : (inr M N).mrange = prod ⊥ ⊤ := map_inr ⊤ +lemma mrange_inr : (inr M N).mrange = prod ⊥ ⊤ := +by simpa only [mrange_eq_map] using map_inr ⊤ @[to_additive] lemma mrange_inl' : (inl M N).mrange = comap (snd M N) ⊥ := mrange_inl.trans (top_prod _) diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean index 95fe0af0e5b89..cb5d939697f2b 100644 --- a/src/linear_algebra/basic.lean +++ b/src/linear_algebra/basic.lean @@ -1341,31 +1341,39 @@ theorem comap_cod_restrict (p : submodule R M) (f : M₂ →ₗ[R] M) (hf p') : submodule.ext $ λ x, ⟨λ h, ⟨⟨_, hf x⟩, h, rfl⟩, by rintro ⟨⟨_, _⟩, h, ⟨⟩⟩; exact h⟩ /-- The range of a linear map `f : M → M₂` is a submodule of `M₂`. -/ -def range (f : M →ₗ[R] M₂) : submodule R M₂ := map f ⊤ +def range (f : M →ₗ[R] M₂) : submodule R M₂ := +(map f ⊤).copy (set.range f) set.image_univ.symm -theorem range_coe (f : M →ₗ[R] M₂) : (range f : set M₂) = set.range f := set.image_univ +/-- Note that `linear_map.range` is deliberately defined in a way that makes this true by `rfl`, +as this means the types `↥(set.range f)` and `↥f.mrange` are interchangeable without proof +obligations. -/ +theorem range_coe (f : M →ₗ[R] M₂) : (range f : set M₂) = set.range f := rfl -@[simp] theorem mem_range {f : M →ₗ[R] M₂} : ∀ {x}, x ∈ range f ↔ ∃ y, f y = x := -set.ext_iff.1 (range_coe f) +@[simp] theorem mem_range {f : M →ₗ[R] M₂} {x} : x ∈ range f ↔ ∃ y, f y = x := +iff.rfl -theorem mem_range_self (f : M →ₗ[R] M₂) (x : M) : f x ∈ f.range := mem_range.2 ⟨x, rfl⟩ +lemma range_eq_map (f : M →ₗ[R] M₂) : f.range = map f ⊤ := +by { ext, simp } + +theorem mem_range_self (f : M →ₗ[R] M₂) (x : M) : f x ∈ f.range := ⟨x, rfl⟩ -@[simp] theorem range_id : range (linear_map.id : M →ₗ[R] M) = ⊤ := map_id _ +@[simp] theorem range_id : range (linear_map.id : M →ₗ[R] M) = ⊤ := +set_like.coe_injective set.range_id theorem range_comp (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) : range (g.comp f) = map g (range f) := -map_comp _ _ _ +set_like.coe_injective (set.range_comp g f) theorem range_comp_le_range (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) : range (g.comp f) ≤ range g := -by rw range_comp; exact map_mono le_top +set_like.coe_mono (set.range_comp_subset_range f g) theorem range_eq_top {f : M →ₗ[R] M₂} : range f = ⊤ ↔ surjective f := by rw [set_like.ext'_iff, range_coe, top_coe, set.range_iff_surjective] lemma range_le_iff_comap {f : M →ₗ[R] M₂} {p : submodule R M₂} : range f ≤ p ↔ comap f p = ⊤ := -by rw [range, map_le_iff_le_comap, eq_top_iff] +by rw [range_eq_map, map_le_iff_le_comap, eq_top_iff] lemma map_le_range {f : M →ₗ[R] M₂} {p : submodule R M} : map f p ≤ range f := -map_mono le_top +set_like.coe_mono (set.image_subset_range f p) /-- Restrict the codomain of a linear map `f` to `f.range`. @@ -1428,7 +1436,7 @@ by rw [ker, comap_cod_restrict, map_bot]; refl lemma range_cod_restrict (p : submodule R M) (f : M₂ →ₗ[R] M) (hf) : range (cod_restrict p f hf) = comap p.subtype f.range := -map_cod_restrict _ _ _ _ +by simpa only [range_eq_map] using map_cod_restrict _ _ _ _ lemma ker_restrict {p : submodule R M} {f : M →ₗ[R] M} (hf : ∀ x : M, x ∈ p → f x ∈ p) : ker (f.restrict hf) = (f.dom_restrict p).ker := @@ -1436,7 +1444,7 @@ by rw [restrict_eq_cod_restrict_dom_restrict, ker_cod_restrict] lemma map_comap_eq (f : M →ₗ[R] M₂) (q : submodule R M₂) : map f (comap f q) = range f ⊓ q := -le_antisymm (le_inf (map_mono le_top) (map_comap_le _ _)) $ +le_antisymm (le_inf map_le_range (map_comap_le _ _)) $ by rintro _ ⟨⟨x, _, rfl⟩, hx⟩; exact ⟨x, hx, rfl⟩ lemma map_comap_eq_self {f : M →ₗ[R] M₂} {q : submodule R M₂} (h : q ≤ range f) : @@ -1447,7 +1455,7 @@ by rwa [map_comap_eq, inf_eq_right] eq_top_iff'.2 $ λ x, by simp @[simp] theorem range_zero : range (0 : M →ₗ[R] M₂) = ⊥ := -submodule.map_zero _ +by simpa only [range_eq_map] using submodule.map_zero _ theorem ker_eq_top {f : M →ₗ[R] M₂} : ker f = ⊤ ↔ f = 0 := ⟨λ h, ext $ λ x, mem_ker.1 $ h.symm ▸ trivial, λ h, h.symm ▸ ker_zero⟩ @@ -1459,8 +1467,8 @@ theorem range_eq_bot {f : M →ₗ[R] M₂} : range f = ⊥ ↔ f = 0 := by rw [← range_le_bot_iff, le_bot_iff] lemma range_le_ker_iff {f : M →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} : range f ≤ ker g ↔ g.comp f = 0 := -⟨λ h, ker_eq_top.1 $ eq_top_iff'.2 $ λ x, h $ mem_map_of_mem trivial, - λ h x hx, mem_ker.2 $ exists.elim hx $ λ y ⟨_, hy⟩, by rw [←hy, ←comp_apply, h, zero_apply]⟩ +⟨λ h, ker_eq_top.1 $ eq_top_iff'.2 $ λ x, h $ ⟨_, rfl⟩, + λ h x hx, mem_ker.2 $ exists.elim hx $ λ y hy, by rw [←hy, ←comp_apply, h, zero_apply]⟩ theorem comap_le_comap_iff {f : M →ₗ[R] M₂} (hf : range f = ⊤) {p p'} : comap f p ≤ comap f p' ↔ p ≤ p' := @@ -1508,7 +1516,7 @@ theorem map_injective {f : M →ₗ[R] M₂} (hf : ker f = ⊥) : injective (map theorem map_eq_top_iff {f : M →ₗ[R] M₂} (hf : range f = ⊤) {p : submodule R M} : p.map f = ⊤ ↔ p ⊔ f.ker = ⊤ := -by simp_rw [← top_le_iff, ← hf, range, map_le_map_iff] +by simp_rw [← top_le_iff, ← hf, range_eq_map, map_le_map_iff] end add_comm_group @@ -1565,10 +1573,10 @@ lemma ker_smul' (f : V →ₗ[K] V₂) (a : K) : ker (a • f) = ⨅(h : a ≠ 0 submodule.comap_smul' f _ a lemma range_smul (f : V →ₗ[K] V₂) (a : K) (h : a ≠ 0) : range (a • f) = range f := -submodule.map_smul f _ a h +by simpa only [range_eq_map] using submodule.map_smul f _ a h lemma range_smul' (f : V →ₗ[K] V₂) (a : K) : range (a • f) = ⨆(h : a ≠ 0), range f := -submodule.map_smul' f _ a +by simpa only [range_eq_map] using submodule.map_smul' f _ a lemma span_singleton_sup_ker_eq_top (f : V →ₗ[K] K) {x : V} (hx : f x ≠ 0) : (K ∙ x) ⊔ f.ker = ⊤ := @@ -1618,7 +1626,7 @@ variables (p p' : submodule R M) (q : submodule R M₂) include T open linear_map -@[simp] theorem map_top (f : M →ₗ[R] M₂) : map f ⊤ = range f := rfl +@[simp] theorem map_top (f : M →ₗ[R] M₂) : map f ⊤ = range f := f.range_eq_map.symm @[simp] theorem comap_bot (f : M →ₗ[R] M₂) : comap f ⊥ = ker f := rfl @@ -1629,7 +1637,7 @@ ker_eq_bot_of_injective $ λ x y, subtype.ext_val by simpa using map_comap_subtype p ⊤ lemma map_subtype_le (p' : submodule R p) : map p.subtype p' ≤ p := -by simpa using (map_mono le_top : map p.subtype p' ≤ p.subtype.range) +by simpa using (map_le_range : map p.subtype p' ≤ p.subtype.range) /-- Under the canonical linear map from a submodule `p` to the ambient space `M`, the image of the maximal submodule of `p` is just `p `. -/ @@ -1701,7 +1709,7 @@ def liftq (f : M →ₗ[R] M₂) (h : p ≤ f.ker) : p.quotient →ₗ[R] M₂ : by ext; refl @[simp] theorem range_mkq : p.mkq.range = ⊤ := -eq_top_iff'.2 $ by rintro ⟨x⟩; exact ⟨x, trivial, rfl⟩ +eq_top_iff'.2 $ by rintro ⟨x⟩; exact ⟨x, rfl⟩ @[simp] theorem ker_mkq : p.mkq.ker = p := by ext; simp @@ -1745,7 +1753,8 @@ theorem ker_liftq (f : M →ₗ[R] M₂) (h) : ker (p.liftq f h) = (ker f).map (mkq p) := comap_liftq _ _ _ _ theorem range_liftq (f : M →ₗ[R] M₂) (h) : - range (p.liftq f h) = range f := map_liftq _ _ _ _ + range (p.liftq f h) = range f := +by simpa only [range_eq_map] using map_liftq _ _ _ _ theorem ker_liftq_eq_bot (f : M →ₗ[R] M₂) (h) (h' : ker f ≤ p) : ker (p.liftq f h) = ⊥ := by rw [ker_liftq, le_antisymm h h', mkq_map_self] @@ -2426,7 +2435,7 @@ linear_equiv.of_bijective (quotient_inf_to_sup_quotient p p') begin rw [quotient_inf_to_sup_quotient, range_liftq, eq_top_iff'], rintros ⟨x, hx⟩, rcases mem_sup.1 hx with ⟨y, hy, z, hz, rfl⟩, - use [⟨y, hy⟩, trivial], apply (submodule.quotient.eq _).2, + use [⟨y, hy⟩], apply (submodule.quotient.eq _).2, change y - (y + z) ∈ p', rwa [sub_add_eq_sub_sub, sub_self, zero_sub, neg_mem_iff] end diff --git a/src/linear_algebra/basis.lean b/src/linear_algebra/basis.lean index 3675f5d1417d5..31fa206827341 100644 --- a/src/linear_algebra/basis.lean +++ b/src/linear_algebra/basis.lean @@ -112,7 +112,7 @@ lemma is_basis.repr_ker : hv.repr.ker = ⊥ := linear_map.ker_eq_bot.2 $ left_inverse.injective hv.total_repr lemma is_basis.repr_range : hv.repr.range = finsupp.supported R R univ := -by rw [is_basis.repr, linear_map.range, submodule.map_comp, +by rw [is_basis.repr, linear_map.range_eq_map, submodule.map_comp, linear_map.map_cod_restrict, submodule.map_id, comap_top, map_top, hv.1.repr_range, finsupp.supported_univ] diff --git a/src/linear_algebra/bilinear_form.lean b/src/linear_algebra/bilinear_form.lean index 277d1da5f6cce..2a5e804e1d819 100644 --- a/src/linear_algebra/bilinear_form.lean +++ b/src/linear_algebra/bilinear_form.lean @@ -1362,10 +1362,9 @@ begin ext x, split; rw [mem_orthogonal_iff]; intro hx, { intros y hy, rw submodule.mem_dual_annihilator_comap_iff at hx, - refine hx (B.to_lin.dom_restrict W ⟨y, hy⟩) ⟨⟨y, hy⟩, _, rfl⟩, - simp only [submodule.top_coe] }, + refine hx (B.to_lin.dom_restrict W ⟨y, hy⟩) ⟨⟨y, hy⟩, rfl⟩ }, { rw submodule.mem_dual_annihilator_comap_iff, - rintro _ ⟨⟨w, hw⟩, _, rfl⟩, + rintro _ ⟨⟨w, hw⟩, rfl⟩, exact hx w hw } end diff --git a/src/linear_algebra/dimension.lean b/src/linear_algebra/dimension.lean index 7358edcb5ac16..cbc09a2a6d834 100644 --- a/src/linear_algebra/dimension.lean +++ b/src/linear_algebra/dimension.lean @@ -352,7 +352,7 @@ lemma dim_add_dim_split have hf : surjective (coprod db eb), begin refine (range_eq_top.1 $ top_unique $ _), - rwa [← map_top, ← prod_top, map_coprod_prod] + rwa [← map_top, ← prod_top, map_coprod_prod, ←range_eq_map, ←range_eq_map] end, begin conv {to_rhs, rw [← dim_prod, dim_eq_of_surjective _ hf] }, @@ -470,7 +470,7 @@ calc rank (f + g) ≤ dim K (f.range ⊔ g.range : submodule K V') : refine dim_le_of_submodule _ _ _, exact (linear_map.range_le_iff_comap.2 $ eq_top_iff'.2 $ assume x, show f x + g x ∈ (f.range ⊔ g.range : submodule K V'), from - mem_sup.2 ⟨_, mem_image_of_mem _ (mem_univ _), _, mem_image_of_mem _ (mem_univ _), rfl⟩) + mem_sup.2 ⟨_, ⟨x, rfl⟩, _, ⟨x, rfl⟩, rfl⟩) end ... ≤ rank f + rank g : dim_add_le_dim_add_dim _ _ @@ -488,7 +488,7 @@ lemma rank_comp_le1 (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') : rank (f.comp g begin refine dim_le_of_submodule _ _ _, rw [linear_map.range_comp], - exact image_subset _ (subset_univ _) + exact linear_map.map_le_range, end variables [add_comm_group V'₁] [vector_space K V'₁] diff --git a/src/linear_algebra/dual.lean b/src/linear_algebra/dual.lean index e800c0bfb027f..c5f5a6b81aeae 100644 --- a/src/linear_algebra/dual.lean +++ b/src/linear_algebra/dual.lean @@ -676,18 +676,18 @@ begin ext φ, split; intro hφ, { rw mem_ker at hφ, rw submodule.mem_dual_annihilator, - rintro y ⟨x, _, rfl⟩, + rintro y ⟨x, rfl⟩, rw [← dual_map_apply, hφ, zero_apply] }, { ext x, rw dual_map_apply, rw submodule.mem_dual_annihilator at hφ, - exact hφ (f x) ⟨x, set_like.mem_coe.mpr submodule.mem_top, rfl⟩ } + exact hφ (f x) ⟨x, rfl⟩ } end lemma range_dual_map_le_dual_annihilator_ker : f.dual_map.range ≤ f.ker.dual_annihilator := begin - rintro _ ⟨ψ, _, rfl⟩, + rintro _ ⟨ψ, rfl⟩, simp_rw [submodule.mem_dual_annihilator, mem_ker], rintro x hx, rw [dual_map_apply, hx, map_zero] diff --git a/src/linear_algebra/eigenspace.lean b/src/linear_algebra/eigenspace.lean index 55055fbdfe96e..ceb24f0089bc7 100644 --- a/src/linear_algebra/eigenspace.lean +++ b/src/linear_algebra/eigenspace.lean @@ -446,7 +446,7 @@ begin by { rw ←pow_add, refl } ... = f.generalized_eigenspace μ (findim K V) : by { rw generalized_eigenspace_eq_generalized_eigenspace_findim_of_le, linarith }, - rw [disjoint, generalized_eigenrange, linear_map.range, submodule.map_inf_eq_map_inf_comap, + rw [disjoint, generalized_eigenrange, linear_map.range_eq_map, submodule.map_inf_eq_map_inf_comap, top_inf_eq, h], apply submodule.map_comap_le end diff --git a/src/linear_algebra/finsupp.lean b/src/linear_algebra/finsupp.lean index b185fced46f05..2e0c78c1d2825 100644 --- a/src/linear_algebra/finsupp.lean +++ b/src/linear_algebra/finsupp.lean @@ -126,7 +126,7 @@ lemma supr_lsingle_range : (⨆a, (lsingle a : M →ₗ[R] (α →₀ M)).range) begin refine (eq_top_iff.2 $ set_like.le_def.2 $ assume f _, _), rw [← sum_single f], - refine sum_mem _ (assume a ha, submodule.mem_supr_of_mem a $ set.mem_image_of_mem _ trivial) + exact sum_mem _ (assume a ha, submodule.mem_supr_of_mem a ⟨_, rfl⟩), end lemma disjoint_lsingle_lsingle (s t : set α) (hs : disjoint s t) : @@ -218,11 +218,8 @@ end theorem range_restrict_dom (s : set α) : (restrict_dom M R s).range = ⊤ := -begin - have := linear_map.range_comp (submodule.subtype _) (restrict_dom M R s), - rw [restrict_dom_comp_subtype, linear_map.range_id] at this, - exact eq_top_mono (submodule.map_mono le_top) this.symm -end +range_eq_top.2 $ function.right_inverse.surjective $ + linear_map.congr_fun (restrict_dom_comp_subtype s) theorem supported_mono {s t : set α} (st : s ⊆ t) : supported M R s ≤ supported M R t := @@ -516,9 +513,11 @@ linear_map.cod_restrict _ ((finsupp.total _ _ _ v).comp (submodule.subtype (supp variables {α} {M} {v} theorem total_on_range (s : set α) : (finsupp.total_on α M R v s).range = ⊤ := -by rw [finsupp.total_on, linear_map.range, linear_map.map_cod_restrict, - ← linear_map.range_le_iff_comap, range_subtype, map_top, linear_map.range_comp, range_subtype]; - exact le_of_eq (span_eq_map_total _ _) +begin + rw [finsupp.total_on, linear_map.range_eq_map, linear_map.map_cod_restrict, + ← linear_map.range_le_iff_comap, range_subtype, map_top, linear_map.range_comp, range_subtype], + exact (span_eq_map_total _ _).le +end theorem total_comp (f : α' → α) : (finsupp.total α' M R (v ∘ f)) = (finsupp.total α M R v).comp (lmap_domain R R f) := diff --git a/src/linear_algebra/linear_independent.lean b/src/linear_algebra/linear_independent.lean index 3609a3814b1a9..82e3d4cde260c 100644 --- a/src/linear_algebra/linear_independent.lean +++ b/src/linear_algebra/linear_independent.lean @@ -565,8 +565,8 @@ apply linear_equiv.of_bijective (linear_map.cod_restrict (span R (range v)) (finsupp.total ι M R v) _), { rw linear_map.ker_cod_restrict, apply hv }, -{ rw [linear_map.range, linear_map.map_cod_restrict, ← linear_map.range_le_iff_comap, - range_subtype, map_top], +{ rw [linear_map.range_eq_map, linear_map.map_cod_restrict, ← linear_map.range_le_iff_comap, + range_subtype, map_top], rw finsupp.range_total, apply le_refl (span R (range v)) }, { intro l, diff --git a/src/linear_algebra/prod.lean b/src/linear_algebra/prod.lean index 64768559ec92f..3b25e8498cdce 100644 --- a/src/linear_algebra/prod.lean +++ b/src/linear_algebra/prod.lean @@ -197,7 +197,7 @@ submodule.ext $ λ x, by simp [mem_sup] lemma is_compl_range_inl_inr : is_compl (inl R M M₂).range (inr R M M₂).range := begin split, - { rintros ⟨_, _⟩ ⟨⟨x, -, hx⟩, ⟨y, -, hy⟩⟩, + { rintros ⟨_, _⟩ ⟨⟨x, hx⟩, ⟨y, hy⟩⟩, simp only [prod.ext_iff, inl_apply, inr_apply, mem_bot] at hx hy ⊢, exact ⟨hy.1.symm, hx.2.symm⟩ }, { rintros ⟨x, y⟩ -, @@ -319,10 +319,10 @@ by rw [ker, ← prod_bot, prod_comap_inl] by rw [ker, ← prod_bot, prod_comap_inr] @[simp] theorem range_fst : (fst R M M₂).range = ⊤ := -by rw [range, ← prod_top, prod_map_fst] +by rw [range_eq_map, ← prod_top, prod_map_fst] @[simp] theorem range_snd : (snd R M M₂).range = ⊤ := -by rw [range, ← prod_top, prod_map_snd] +by rw [range_eq_map, ← prod_top, prod_map_snd] end submodule diff --git a/src/ring_theory/adjoin/basic.lean b/src/ring_theory/adjoin/basic.lean index 939576bb0d4be..346bf455f9c5e 100644 --- a/src/ring_theory/adjoin/basic.lean +++ b/src/ring_theory/adjoin/basic.lean @@ -112,8 +112,8 @@ le_antisymm theorem adjoin_eq_range : adjoin R s = (mv_polynomial.aeval (coe : s → A)).range := le_antisymm - (adjoin_le $ λ x hx, ⟨mv_polynomial.X ⟨x, hx⟩, set.mem_univ _, mv_polynomial.eval₂_X _ _ _⟩) - (λ x ⟨p, _, (hp : mv_polynomial.aeval coe p = x)⟩, hp ▸ mv_polynomial.induction_on p + (adjoin_le $ λ x hx, ⟨mv_polynomial.X ⟨x, hx⟩, mv_polynomial.eval₂_X _ _ _⟩) + (λ x ⟨p, (hp : mv_polynomial.aeval coe p = x)⟩, hp ▸ mv_polynomial.induction_on p (λ r, by { rw [mv_polynomial.aeval_def, mv_polynomial.eval₂_C], exact (adjoin R s).algebra_map_mem r }) (λ p q hp hq, by rw alg_hom.map_add; exact subalgebra.add_mem _ hp hq) @@ -122,8 +122,8 @@ le_antisymm theorem adjoin_singleton_eq_range (x : A) : adjoin R {x} = (polynomial.aeval x).range := le_antisymm - (adjoin_le $ set.singleton_subset_iff.2 ⟨polynomial.X, set.mem_univ _, polynomial.eval₂_X _ _⟩) - (λ y ⟨p, _, (hp : polynomial.aeval x p = y)⟩, hp ▸ polynomial.induction_on p + (adjoin_le $ set.singleton_subset_iff.2 ⟨polynomial.X, polynomial.eval₂_X _ _⟩) + (λ y ⟨p, (hp : polynomial.aeval x p = y)⟩, hp ▸ polynomial.induction_on p (λ r, by { rw [polynomial.aeval_def, polynomial.eval₂_C], exact (adjoin R _).algebra_map_mem r }) (λ p q hp hq, by rw alg_hom.map_add; exact subalgebra.add_mem _ hp hq) diff --git a/src/ring_theory/adjoin_root.lean b/src/ring_theory/adjoin_root.lean index 8c7305cacffc9..2948c8c5be728 100644 --- a/src/ring_theory/adjoin_root.lean +++ b/src/ring_theory/adjoin_root.lean @@ -101,7 +101,7 @@ polynomial.induction_on p (λ x, by { rw aeval_C, refl }) theorem adjoin_root_eq_top : algebra.adjoin R ({root f} : set (adjoin_root f)) = ⊤ := algebra.eq_top_iff.2 $ λ x, induction_on f x $ λ p, -(algebra.adjoin_singleton_eq_range R (root f)).symm ▸ ⟨p, set.mem_univ _, aeval_eq p⟩ +(algebra.adjoin_singleton_eq_range R (root f)).symm ▸ ⟨p, aeval_eq p⟩ @[simp] lemma eval₂_root (f : polynomial R) : f.eval₂ (of f) (root f) = 0 := by rw [← algebra_map_eq, ← aeval_def, aeval_eq, mk_self] diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean index 11e999998f2e9..9dc13fed002a6 100644 --- a/src/ring_theory/noetherian.lean +++ b/src/ring_theory/noetherian.lean @@ -353,7 +353,7 @@ instance is_noetherian_prod [is_noetherian R M] [is_noetherian R P] : is_noetherian R (M × P) := ⟨λ s, submodule.fg_of_fg_map_of_fg_inf_ker (linear_map.snd R M P) (noetherian _) $ have s ⊓ linear_map.ker (linear_map.snd R M P) ≤ linear_map.range (linear_map.inl R M P), -from λ x ⟨hx1, hx2⟩, ⟨x.1, trivial, prod.ext rfl $ eq.symm $ linear_map.mem_ker.1 hx2⟩, +from λ x ⟨hx1, hx2⟩, ⟨x.1, prod.ext rfl $ eq.symm $ linear_map.mem_ker.1 hx2⟩, linear_map.map_comap_eq_self this ▸ submodule.fg_map (noetherian _)⟩ instance is_noetherian_pi {R ι : Type*} {M : ι → Type*} [ring R] diff --git a/src/ring_theory/subring.lean b/src/ring_theory/subring.lean index 5388017e229af..94c3ab05b39a5 100644 --- a/src/ring_theory/subring.lean +++ b/src/ring_theory/subring.lean @@ -382,19 +382,24 @@ variables (g : S →+* T) (f : R →+* S) /-! # range -/ /-- The range of a ring homomorphism, as a subring of the target. -/ -def range {R : Type u} {S : Type v} [ring R] [ring S] - (f : R →+* S) : subring S := (⊤ : subring R).map f +def range {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) : subring S := +((⊤ : subring R).map f).copy (set.range f) set.image_univ.symm -@[simp] lemma coe_range : (f.range : set S) = set.range f := set.image_univ +/-- Note that `ring_hom.range` is deliberately defined in a way that makes this true by `rfl`, +as this means the types `↥(set.range f)` and `↥f.range` are interchangeable without proof +obligations. -/ +@[simp] lemma coe_range : (f.range : set S) = set.range f := rfl -@[simp] lemma mem_range {f : R →+* S} {y : S} : y ∈ f.range ↔ ∃ x, f x = y := -by simp [range] +@[simp] lemma mem_range {f : R →+* S} {y : S} : y ∈ f.range ↔ ∃ x, f x = y := iff.rfl + +lemma range_eq_map (f : R →+* S) : f.range = subring.map f ⊤ := +by { ext, simp } lemma mem_range_self (f : R →+* S) (x : R) : f x ∈ f.range := mem_range.mpr ⟨x, rfl⟩ lemma map_range : f.range.map g = (g.comp f).range := -(⊤ : subring R).map_map g f +by simpa only [range_eq_map] using (⊤ : subring R).map_map g f -- TODO -- rename to `cod_restrict` when is_ring_hom is deprecated /-- Restrict the codomain of a ring homomorphism to a subring that includes the range. -/ @@ -677,7 +682,7 @@ def restrict (f : R →+* S) (s : subring R) : s →+* S := f.comp s.subtype This is the bundled version of `set.range_factorization`. -/ def range_restrict (f : R →+* S) : R →+* f.range := -f.cod_restrict' f.range $ λ x, ⟨x, subring.mem_top x, rfl⟩ +f.cod_restrict' f.range $ λ x, ⟨x, rfl⟩ @[simp] lemma coe_range_restrict (f : R →+* S) (x : R) : (f.range_restrict x : S) = f x := rfl diff --git a/src/ring_theory/subsemiring.lean b/src/ring_theory/subsemiring.lean index f88d091a3ea49..65b0cd500cd4c 100644 --- a/src/ring_theory/subsemiring.lean +++ b/src/ring_theory/subsemiring.lean @@ -273,18 +273,25 @@ namespace ring_hom variables (g : S →+* T) (f : R →+* S) /-- The range of a ring homomorphism is a subsemiring. -/ -def srange : subsemiring S := (⊤ : subsemiring R).map f +def srange : subsemiring S := +((⊤ : subsemiring R).map f).copy (set.range f) set.image_univ.symm -@[simp] lemma coe_srange : (f.srange : set S) = set.range f := set.image_univ +/-- Note that `ring_hom.srange` is deliberately defined in a way that makes this true by `rfl`, +as this means the types `↥(set.range f)` and `↥f.srange` are interchangeable without proof +obligations. -/ +@[simp] lemma coe_srange : (f.srange : set S) = set.range f := rfl @[simp] lemma mem_srange {f : R →+* S} {y : S} : y ∈ f.srange ↔ ∃ x, f x = y := -by simp [srange] +iff.rfl + +lemma srange_eq_map (f : R →+* S) : f.srange = (⊤ : subsemiring R).map f := +by { ext, simp } lemma mem_srange_self (f : R →+* S) (x : R) : f x ∈ f.srange := mem_srange.mpr ⟨x, rfl⟩ lemma map_srange : f.srange.map g = (g.comp f).srange := -(⊤ : subsemiring R).map_map g f +by simpa only [srange_eq_map] using (⊤ : subsemiring R).map_map g f end ring_hom