From fe332cf8858a2d8beb7aefa07d8d548835b41084 Mon Sep 17 00:00:00 2001 From: Vierkantor Date: Thu, 23 Nov 2023 16:05:38 +0000 Subject: [PATCH] More --- Mathlib/Algebra/Module/PID.lean | 2 +- Mathlib/Combinatorics/Additive/SalemSpencer.lean | 2 +- .../FieldTheory/IsAlgClosed/AlgebraicClosure.lean | 6 ++++++ Mathlib/LinearAlgebra/QuadraticForm/Basic.lean | 4 ++-- Mathlib/NumberTheory/NumberField/Basic.lean | 3 ++- Mathlib/NumberTheory/RamificationInertia.lean | 2 +- Mathlib/RingTheory/ClassGroup.lean | 2 +- Mathlib/RingTheory/IntegralClosure.lean | 6 ++++-- Mathlib/RingTheory/RootsOfUnity/Basic.lean | 6 ++++-- Mathlib/Topology/Algebra/Equicontinuity.lean | 5 +++-- Mathlib/Topology/ContinuousFunction/Bounded.lean | 13 +++++-------- Mathlib/Topology/VectorBundle/Constructions.lean | 4 ++-- 12 files changed, 32 insertions(+), 23 deletions(-) diff --git a/Mathlib/Algebra/Module/PID.lean b/Mathlib/Algebra/Module/PID.lean index 86fd2d17ad6370..09f806ee7d89f3 100644 --- a/Mathlib/Algebra/Module/PID.lean +++ b/Mathlib/Algebra/Module/PID.lean @@ -219,7 +219,7 @@ theorem torsion_by_prime_power_decomposition (hN : Module.IsTorsion' N (Submonoi simp only [LinearMap.coe_comp, Function.comp_apply, mkQ_apply] rw [LinearEquiv.coe_toLinearMap, LinearMap.id_apply, DirectSum.toModule_lof, liftQSpanSingleton_apply, LinearMap.toSpanSingleton_one, Ideal.Quotient.mk_eq_mk, - map_one, (this i).choose_spec.right] + map_one (Ideal.Quotient.mk _), (this i).choose_spec.right] · exact (mk_surjective _).forall.mpr fun x => ⟨(@hN x).choose, by rw [← Quotient.mk_smul, (@hN x).choose_spec, Quotient.mk_zero]⟩ · have hs' := congr_arg (Submodule.map <| mkQ <| R ∙ s j) hs diff --git a/Mathlib/Combinatorics/Additive/SalemSpencer.lean b/Mathlib/Combinatorics/Additive/SalemSpencer.lean index e6c3b105fb423a..85acf6ab7e2c0a 100644 --- a/Mathlib/Combinatorics/Additive/SalemSpencer.lean +++ b/Mathlib/Combinatorics/Additive/SalemSpencer.lean @@ -128,7 +128,7 @@ theorem MulSalemSpencer.of_image [FunLike F α fun _ => β] [FreimanHomClass F s -- TODO: Generalize to Freiman homs @[to_additive] -theorem MulSalemSpencer.image [MulHomClass F α β] (f : F) (hf : (s * s).InjOn f) +theorem MulSalemSpencer.image [NDFunLike F α β] [MulHomClass F α β] (f : F) (hf : (s * s).InjOn f) (h : MulSalemSpencer s) : MulSalemSpencer (f '' s) := by rintro _ _ _ ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩ ⟨c, hc, rfl⟩ habc rw [h ha hb hc (hf (mul_mem_mul ha hb) (mul_mem_mul hc hc) <| by rwa [map_mul, map_mul])] diff --git a/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean b/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean index 64298ee19fbac3..7bcb52cbd58626 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean @@ -367,6 +367,9 @@ local instance instAlgebra : Algebra k (AlgebraicClosureAux k) := #noalign algebraic_closure.algebra_map_def +-- TODO: is there a better solution? +attribute [instance 50] MulRingSeminormClass.toMonoidHomClass + /-- Canonical algebra embedding from the `n`th step to the algebraic closure. -/ def ofStepHom (n) : Step k n →ₐ[k] AlgebraicClosureAux k := { ofStep k n with @@ -425,6 +428,9 @@ def algEquivAlgebraicClosureAux : exact Ideal.quotientKerAlgEquivOfSurjective (fun x => ⟨MvPolynomial.X x, by simp⟩) +-- TODO: is there a more principled fix? +attribute [instance 50] MulRingSeminormClass.toMonoidWithZeroHomClass + -- This instance is basically copied from the `Field` instance on `SplittingField` instance : Field (AlgebraicClosure k) := letI e := algEquivAlgebraicClosureAux k diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index 3941e29248f676..f09e6eb7b133b2 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -238,8 +238,8 @@ theorem map_zero : Q 0 = 0 := by rw [← @zero_smul R _ _ _ _ (0 : M), map_smul, zero_mul, zero_mul] #align quadratic_form.map_zero QuadraticForm.map_zero -instance zeroHomClass : ZeroHomClass (QuadraticForm R M) M R := - { QuadraticForm.funLike with map_zero := map_zero } +instance zeroHomClass : ZeroHomClass (QuadraticForm R M) M R where + map_zero := map_zero #align quadratic_form.zero_hom_class QuadraticForm.zeroHomClass theorem map_smul_of_tower [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] (a : S) diff --git a/Mathlib/NumberTheory/NumberField/Basic.lean b/Mathlib/NumberTheory/NumberField/Basic.lean index 0c9c5896b60fc5..7a3c0cbf21b5a5 100644 --- a/Mathlib/NumberTheory/NumberField/Basic.lean +++ b/Mathlib/NumberTheory/NumberField/Basic.lean @@ -112,7 +112,8 @@ theorem isIntegral_coe (x : 𝓞 K) : IsIntegral ℤ (x : K) := x.2 #align number_field.ring_of_integers.is_integral_coe NumberField.RingOfIntegers.isIntegral_coe -theorem map_mem {F L : Type*} [Field L] [CharZero K] [CharZero L] [AlgHomClass F ℚ K L] (f : F) +theorem map_mem {F L : Type*} [Field L] [CharZero K] [CharZero L] + [NDFunLike F K L] [AlgHomClass F ℚ K L] (f : F) (x : 𝓞 K) : f x ∈ 𝓞 L := (mem_ringOfIntegers _ _).2 <| map_isIntegral_int f <| RingOfIntegers.isIntegral_coe x #align number_field.ring_of_integers.map_mem NumberField.RingOfIntegers.map_mem diff --git a/Mathlib/NumberTheory/RamificationInertia.lean b/Mathlib/NumberTheory/RamificationInertia.lean index cbfeca458e88a8..5c78b7e3ab1fda 100644 --- a/Mathlib/NumberTheory/RamificationInertia.lean +++ b/Mathlib/NumberTheory/RamificationInertia.lean @@ -367,7 +367,7 @@ theorem FinrankQuotientMap.span_eq_top [IsDomain R] [IsDomain S] [Algebra K L] [ -- Because `det A ≠ 0`, we have `span L {det A} = ⊤`. · rw [eq_comm, Submodule.restrictScalars_eq_top_iff, Ideal.span_singleton_eq_top] refine IsUnit.mk0 _ ((map_ne_zero_iff (algebraMap R L) hRL).mpr ?_) - refine @ne_zero_of_map _ _ _ _ _ _ (Ideal.Quotient.mk p) _ ?_ + refine ne_zero_of_map (f := Ideal.Quotient.mk p) ?_ haveI := Ideal.Quotient.nontrivial hp calc Ideal.Quotient.mk p A.det = Matrix.det ((Ideal.Quotient.mk p).mapMatrix A) := by diff --git a/Mathlib/RingTheory/ClassGroup.lean b/Mathlib/RingTheory/ClassGroup.lean index 767581952d7c87..28f5bc0b1ba373 100644 --- a/Mathlib/RingTheory/ClassGroup.lean +++ b/Mathlib/RingTheory/ClassGroup.lean @@ -152,7 +152,7 @@ theorem ClassGroup.mk_eq_mk_of_coe_ideal {I J : (FractionalIdeal R⁰ <| Fractio theorem ClassGroup.mk_eq_one_of_coe_ideal {I : (FractionalIdeal R⁰ <| FractionRing R)ˣ} {I' : Ideal R} (hI : (I : FractionalIdeal R⁰ <| FractionRing R) = I') : ClassGroup.mk I = 1 ↔ ∃ x : R, x ≠ 0 ∧ I' = Ideal.span {x} := by - rw [← map_one (ClassGroup.mk (R := R) (K := FractionRing R)), + rw [← _root_.map_one (ClassGroup.mk (R := R) (K := FractionRing R)), ClassGroup.mk_eq_mk_of_coe_ideal hI (?_ : _ = ↑(⊤ : Ideal R))] any_goals rfl constructor diff --git a/Mathlib/RingTheory/IntegralClosure.lean b/Mathlib/RingTheory/IntegralClosure.lean index 6dc107f15a0ec1..b5ac213127601f 100644 --- a/Mathlib/RingTheory/IntegralClosure.lean +++ b/Mathlib/RingTheory/IntegralClosure.lean @@ -90,7 +90,8 @@ variable [CommRing R] [CommRing A] [Ring B] [CommRing S] variable [Algebra R A] [Algebra R B] (f : R →+* S) theorem IsIntegral.map {B C F : Type*} [Ring B] [Ring C] [Algebra R B] [Algebra A B] [Algebra R C] - [IsScalarTower R A B] [Algebra A C] [IsScalarTower R A C] {b : B} [AlgHomClass F A B C] (f : F) + [IsScalarTower R A B] [Algebra A C] [IsScalarTower R A C] {b : B} + [NDFunLike F B C] [AlgHomClass F A B C] (f : F) (hb : IsIntegral R b) : IsIntegral R (f b) := by obtain ⟨P, hP⟩ := hb refine' ⟨P, hP.1, _⟩ @@ -138,7 +139,8 @@ theorem IsIntegral.tower_top [Algebra A B] [IsScalarTower R A B] {x : B} #align is_integral_of_is_scalar_tower IsIntegral.tower_top #align is_integral_tower_top_of_is_integral IsIntegral.tower_top -theorem map_isIntegral_int {B C F : Type*} [Ring B] [Ring C] {b : B} [RingHomClass F B C] (f : F) +theorem map_isIntegral_int {B C F : Type*} [Ring B] [Ring C] {b : B} + [NDFunLike F B C] [RingHomClass F B C] (f : F) (hb : IsIntegral ℤ b) : IsIntegral ℤ (f b) := hb.map (f : B →+* C).toIntAlgHom #align map_is_integral_int map_isIntegral_int diff --git a/Mathlib/RingTheory/RootsOfUnity/Basic.lean b/Mathlib/RingTheory/RootsOfUnity/Basic.lean index 0af6a97455c712..8290afec9a1f4f 100644 --- a/Mathlib/RingTheory/RootsOfUnity/Basic.lean +++ b/Mathlib/RingTheory/RootsOfUnity/Basic.lean @@ -135,7 +135,7 @@ theorem rootsOfUnity.coe_pow [CommMonoid R] (ζ : rootsOfUnity k R) (m : ℕ) : section CommSemiring -variable [CommSemiring R] [CommSemiring S] +variable [CommSemiring R] [CommSemiring S] [NDFunLike F R S] /-- Restrict a ring homomorphism to the nth roots of unity. -/ def restrictRootsOfUnity [RingHomClass F R S] (σ : F) (n : ℕ+) : @@ -250,7 +250,7 @@ theorem card_rootsOfUnity : Fintype.card (rootsOfUnity k R) ≤ k := variable {k R} -theorem map_rootsOfUnity_eq_pow_self [RingHomClass F R R] (σ : F) (ζ : rootsOfUnity k R) : +theorem map_rootsOfUnity_eq_pow_self [NDFunLike F R R] [RingHomClass F R R] (σ : F) (ζ : rootsOfUnity k R) : ∃ m : ℕ, σ (ζ : Rˣ) = ((ζ : Rˣ) : R) ^ m := by obtain ⟨m, hm⟩ := MonoidHom.map_cyclic (restrictRootsOfUnity σ k) rw [← restrictRootsOfUnity_coe_apply, hm, ←zpow_mod_orderOf, ← Int.toNat_of_nonneg @@ -498,6 +498,8 @@ section Maps open Function +variable [NDFunLike F M N] + theorem map_of_injective [MonoidHomClass F M N] (h : IsPrimitiveRoot ζ k) (hf : Injective f) : IsPrimitiveRoot (f ζ) k where pow_eq_one := by rw [← map_pow, h.pow_eq_one, _root_.map_one] diff --git a/Mathlib/Topology/Algebra/Equicontinuity.lean b/Mathlib/Topology/Algebra/Equicontinuity.lean index 6a328a9ab1757f..d4b74298e2c00c 100644 --- a/Mathlib/Topology/Algebra/Equicontinuity.lean +++ b/Mathlib/Topology/Algebra/Equicontinuity.lean @@ -19,7 +19,7 @@ open UniformConvergence @[to_additive] theorem equicontinuous_of_equicontinuousAt_one {ι G M hom : Type*} [TopologicalSpace G] [UniformSpace M] [Group G] [Group M] [TopologicalGroup G] [UniformGroup M] - [MonoidHomClass hom G M] (F : ι → hom) + [NDFunLike hom G M] [MonoidHomClass hom G M] (F : ι → hom) (hf : EquicontinuousAt ((↑) ∘ F) (1 : G)) : Equicontinuous ((↑) ∘ F) := by rw [equicontinuous_iff_continuous] @@ -34,7 +34,8 @@ theorem equicontinuous_of_equicontinuousAt_one {ι G M hom : Type*} [Topological @[to_additive] theorem uniformEquicontinuous_of_equicontinuousAt_one {ι G M hom : Type*} [UniformSpace G] - [UniformSpace M] [Group G] [Group M] [UniformGroup G] [UniformGroup M] [MonoidHomClass hom G M] + [UniformSpace M] [Group G] [Group M] [UniformGroup G] [UniformGroup M] + [NDFunLike hom G M] [MonoidHomClass hom G M] (F : ι → hom) (hf : EquicontinuousAt ((↑) ∘ F) (1 : G)) : UniformEquicontinuous ((↑) ∘ F) := by rw [uniformEquicontinuous_iff_uniformContinuous] diff --git a/Mathlib/Topology/ContinuousFunction/Bounded.lean b/Mathlib/Topology/ContinuousFunction/Bounded.lean index bc4394142c5d41..6b5bd4ab0150c0 100644 --- a/Mathlib/Topology/ContinuousFunction/Bounded.lean +++ b/Mathlib/Topology/ContinuousFunction/Bounded.lean @@ -53,7 +53,7 @@ section You should also extend this typeclass when you extend `BoundedContinuousFunction`. -/ class BoundedContinuousMapClass (F : Type*) (α β : outParam <| Type*) [TopologicalSpace α] - [PseudoMetricSpace β] extends ContinuousMapClass F α β where + [PseudoMetricSpace β] [NDFunLike F α β] extends ContinuousMapClass F α β : Prop where map_bounded (f : F) : ∃ C, ∀ x y, dist (f x) (f y) ≤ C #align bounded_continuous_map_class BoundedContinuousMapClass @@ -69,21 +69,18 @@ variable [TopologicalSpace α] [PseudoMetricSpace β] [PseudoMetricSpace γ] variable {f g : α →ᵇ β} {x : α} {C : ℝ} -instance : BoundedContinuousMapClass (α →ᵇ β) α β where +instance : NDFunLike (α →ᵇ β) α β where coe f := f.toFun coe_injective' f g h := by obtain ⟨⟨_, _⟩, _⟩ := f obtain ⟨⟨_, _⟩, _⟩ := g congr + +instance : BoundedContinuousMapClass (α →ᵇ β) α β where map_continuous f := f.continuous_toFun map_bounded f := f.map_bounded' -/-- Helper instance for when there's too many metavariables to apply `FunLike.hasCoeToFun` -directly. -/ -instance : CoeFun (α →ᵇ β) fun _ => α → β := - FunLike.hasCoeToFun - -instance [BoundedContinuousMapClass F α β] : CoeTC F (α →ᵇ β) := +instance [NDFunLike F α β] [BoundedContinuousMapClass F α β] : CoeTC F (α →ᵇ β) := ⟨fun f => { toFun := f continuous_toFun := map_continuous f diff --git a/Mathlib/Topology/VectorBundle/Constructions.lean b/Mathlib/Topology/VectorBundle/Constructions.lean index 729ab7c89240f8..144116a3538f96 100644 --- a/Mathlib/Topology/VectorBundle/Constructions.lean +++ b/Mathlib/Topology/VectorBundle/Constructions.lean @@ -174,10 +174,10 @@ instance [Semiring R] [∀ x : B, AddCommMonoid (E x)] [i : ∀ x, Module R (E x variable {E F} [TopologicalSpace B'] [TopologicalSpace (TotalSpace F E)] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] [∀ x, AddCommMonoid (E x)] - [∀ x, Module 𝕜 (E x)] {K : Type*} [ContinuousMapClass K B' B] + [∀ x, Module 𝕜 (E x)] {K : Type*} [NDFunLike K B' B] [ContinuousMapClass K B' B] instance Trivialization.pullback_linear (e : Trivialization F (π F E)) [e.IsLinear 𝕜] (f : K) : - (@Trivialization.pullback _ _ _ B' _ _ _ _ _ _ _ e f).IsLinear 𝕜 where + (Trivialization.pullback (B' := B') e f).IsLinear 𝕜 where linear _ h := e.linear 𝕜 h #align trivialization.pullback_linear Trivialization.pullback_linear