[Merged by Bors] - perf(NumberTheory.NumberField.Basic): make RingOfIntegers a Type.

Mathlib/NumberTheory/Cyclotomic/Rat.lean

@@ -242,9 +242,7 @@ theorem power_basis_int'_dim [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : Is
 extension of `ℚ`. -/
 noncomputable def subOneIntegralPowerBasis [IsCyclotomicExtension {p ^ k} ℚ K]
     (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : PowerBasis ℤ (𝓞 K) :=
-  PowerBasis.ofGenMemAdjoin' hζ.integralPowerBasis
-    (isIntegral_of_mem_ringOfIntegers <|
-      Subalgebra.sub_mem _ (hζ.isIntegral (p ^ k).pos) (Subalgebra.one_mem _))
+  PowerBasis.ofGenMemAdjoin' hζ.integralPowerBasis (RingOfIntegers.isIntegral _)
     (by
       simp only [integralPowerBasis_gen, toInteger]
       convert Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ (⟨ζ - 1, _⟩ : 𝓞 K))
@@ -285,13 +283,13 @@ theorem zeta_sub_one_prime_of_ne_two [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
   letI := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
   refine Ideal.prime_of_irreducible_absNorm_span (fun h ↦ ?_) ?_
   · apply hζ.pow_ne_one_of_pos_of_lt zero_lt_one (one_lt_pow hp.out.one_lt (by simp))
-    rw [← Subalgebra.coe_eq_zero] at h
-    simpa [sub_eq_zero] using h
+    rw [sub_eq_zero] at h
+    simpa using congrArg (algebraMap _ K) h
   rw [Nat.irreducible_iff_prime, Ideal.absNorm_span_singleton, ← Nat.prime_iff,
     ← Int.prime_iff_natAbs_prime]
   convert Nat.prime_iff_prime_int.1 hp.out
   apply RingHom.injective_int (algebraMap ℤ ℚ)
-  rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ), Subalgebra.algebraMap_eq]
+  rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ)]
   simp only [PNat.pow_coe, id.map_eq_id, RingHomCompTriple.comp_eq, RingHom.coe_coe,
     Subalgebra.coe_val, algebraMap_int_eq, map_natCast]
   exact hζ.sub_one_norm_prime_ne_two (Polynomial.cyclotomic.irreducible_rat (PNat.pos _)) hodd
@@ -304,20 +302,20 @@ theorem zeta_sub_one_prime_of_two_pow [IsCyclotomicExtension {(2 : ℕ+) ^ (k +
   letI := IsCyclotomicExtension.numberField {(2 : ℕ+) ^ (k + 1)} ℚ K
   refine Ideal.prime_of_irreducible_absNorm_span (fun h ↦ ?_) ?_
   · apply hζ.pow_ne_one_of_pos_of_lt zero_lt_one (one_lt_pow (by decide) (by simp))
-    rw [← Subalgebra.coe_eq_zero] at h
-    simpa [sub_eq_zero] using h
+    rw [sub_eq_zero] at h
+    simpa using congrArg (algebraMap _ K) h
   rw [Nat.irreducible_iff_prime, Ideal.absNorm_span_singleton, ← Nat.prime_iff,
     ← Int.prime_iff_natAbs_prime]
   cases k
   · convert Prime.neg Int.prime_two
     apply RingHom.injective_int (algebraMap ℤ ℚ)
-    rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ), Subalgebra.algebraMap_eq]
+    rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ)]
     simp only [Nat.zero_eq, PNat.pow_coe, id.map_eq_id, RingHomCompTriple.comp_eq, RingHom.coe_coe,
       Subalgebra.coe_val, algebraMap_int_eq, map_neg, map_ofNat]
     simpa using hζ.pow_sub_one_norm_two (cyclotomic.irreducible_rat (by simp))
   convert Int.prime_two
   apply RingHom.injective_int (algebraMap ℤ ℚ)
-  rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ), Subalgebra.algebraMap_eq]
+  rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ)]
   simp only [PNat.pow_coe, id.map_eq_id, RingHomCompTriple.comp_eq, RingHom.coe_coe,
     Subalgebra.coe_val, algebraMap_int_eq, map_natCast]
   exact hζ.sub_one_norm_two Nat.AtLeastTwo.prop (cyclotomic.irreducible_rat (by simp))

Mathlib/NumberTheory/NumberField/Basic.lean

@@ -15,7 +15,7 @@ This file defines a number field and the ring of integers corresponding to it.
 ## Main definitions
  - `NumberField` defines a number field as a field which has characteristic zero and is finite
     dimensional over ℚ.
- - `ringOfIntegers` defines the ring of integers (or number ring) corresponding to a number field
+ - `RingOfIntegers` defines the ring of integers (or number ring) corresponding to a number field
     as the integral closure of ℤ in the number field.
 
 ## Implementation notes
@@ -64,35 +64,88 @@ instance [NumberField L] [Algebra K L] : FiniteDimensional K L :=
   Module.Finite.of_restrictScalars_finite ℚ K L
 
 /-- The ring of integers (or number ring) corresponding to a number field
-is the integral closure of ℤ in the number field. -/
-def ringOfIntegers :=
+is the integral closure of ℤ in the number field.
+
+This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
+looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
+much more effective use of the discrimination tree than instances of the form
+`SMul (Subtype _) (Subtype _)`.
+The drawback is we have to copy over instances manually.
+-/
+def RingOfIntegers : Type _ :=
   integralClosure ℤ K
-#align number_field.ring_of_integers NumberField.ringOfIntegers
+#align number_field.ring_of_integers NumberField.RingOfIntegers
 
-@[inherit_doc] scoped notation "𝓞" => NumberField.ringOfIntegers
+@[inherit_doc] scoped notation "𝓞" => NumberField.RingOfIntegers
 
-theorem mem_ringOfIntegers (x : K) : x ∈ 𝓞 K ↔ IsIntegral ℤ x :=
-  Iff.rfl
-#align number_field.mem_ring_of_integers NumberField.mem_ringOfIntegers
+#noalign number_field.mem_ring_of_integers
 
-theorem isIntegral_of_mem_ringOfIntegers {K : Type*} [Field K] {x : K} (hx : x ∈ 𝓞 K) :
-    IsIntegral ℤ (⟨x, hx⟩ : 𝓞 K) := by
-  obtain ⟨P, hPm, hP⟩ := hx
-  refine' ⟨P, hPm, _⟩
-  rw [← Polynomial.aeval_def, ← Subalgebra.coe_eq_zero, Polynomial.aeval_subalgebra_coe,
-    Polynomial.aeval_def, Subtype.coe_mk, hP]
-#align number_field.is_integral_of_mem_ring_of_integers NumberField.isIntegral_of_mem_ringOfIntegers
+namespace RingOfIntegers
+
+instance : CommRing (𝓞 K) :=
+  inferInstanceAs (CommRing (integralClosure _ _))
+instance : IsDomain (𝓞 K) :=
+  inferInstanceAs (IsDomain (integralClosure _ _))
+instance : CharZero (𝓞 K) :=
+  inferInstanceAs (CharZero (integralClosure _ _))
+instance : Algebra (𝓞 K) K :=
+  inferInstanceAs (Algebra (integralClosure _ _) _)
+instance : NoZeroSMulDivisors (𝓞 K) K :=
+  inferInstanceAs (NoZeroSMulDivisors (integralClosure _ _) _)
+instance : Nontrivial (𝓞 K) :=
+  inferInstanceAs (Nontrivial (integralClosure _ _))
+
+variable {K}
+
+/-- The canonical coercion from `𝓞 K` to `K`. -/
+@[coe]
+abbrev val (x : 𝓞 K) : K := algebraMap _ _ x
+
+/-- This instance has to be `CoeHead` because we only want to apply it from `𝓞 K` to `K`. -/
+instance : CoeHead (𝓞 K) K := ⟨val⟩
+
+lemma coe_eq_algebraMap (x : 𝓞 K) : (x : K) = algebraMap _ _ x := rfl
+
+@[ext] theorem ext {x y : 𝓞 K} (h : (x : K) = (y : K)) : x = y :=
+  Subtype.ext h
+
+theorem ext_iff {x y : 𝓞 K} : x = y ↔ (x : K) = (y : K) :=
+  Subtype.ext_iff
+
+@[simp] lemma map_mk (x : K) (hx) : algebraMap (𝓞 K) K ⟨x, hx⟩ = x := rfl
+
+lemma coe_mk {x : K} (hx) : ((⟨x, hx⟩ : 𝓞 K) : K) = x := rfl
+
+lemma mk_eq_mk (x y : K) (hx hy) : (⟨x, hx⟩ : 𝓞 K) = ⟨y, hy⟩ ↔ x = y := by simp
+
+@[simp] lemma mk_one : (⟨1, one_mem _⟩ : 𝓞 K) = 1 :=
+  rfl
+
+@[simp] lemma mk_zero : (⟨0, zero_mem _⟩ : 𝓞 K) = 0 :=
+  rfl
+-- TODO: these lemmas don't seem to fire?
+@[simp] lemma mk_add_mk (x y : K) (hx hy) : (⟨x, hx⟩ : 𝓞 K) + ⟨y, hy⟩ = ⟨x + y, add_mem hx hy⟩ :=
+  rfl
+
+@[simp] lemma mk_mul_mk (x y : K) (hx hy) : (⟨x, hx⟩ : 𝓞 K) * ⟨y, hy⟩ = ⟨x * y, mul_mem hx hy⟩ :=
+  rfl
+
+@[simp] lemma mk_sub_mk (x y : K) (hx hy) : (⟨x, hx⟩ : 𝓞 K) - ⟨y, hy⟩ = ⟨x - y, sub_mem hx hy⟩ :=
+  rfl
+
+@[simp] lemma neg_mk (x : K) (hx) : (-⟨x, hx⟩ : 𝓞 K) = ⟨-x, neg_mem hx⟩ :=
+  rfl
+
+end RingOfIntegers
 
 /-- Given an algebra between two fields, create an algebra between their two rings of integers. -/
 instance inst_ringOfIntegersAlgebra [Algebra K L] : Algebra (𝓞 K) (𝓞 L) :=
   RingHom.toAlgebra
-    { toFun := fun k => ⟨algebraMap K L k, IsIntegral.algebraMap k.2⟩
-      map_zero' := Subtype.ext <| by simp only [Subtype.coe_mk, Subalgebra.coe_zero, map_zero]
-      map_one' := Subtype.ext <| by simp only [Subtype.coe_mk, Subalgebra.coe_one, map_one]
-      map_add' := fun x y =>
-        Subtype.ext <| by simp only [map_add, Subalgebra.coe_add, Subtype.coe_mk]
-      map_mul' := fun x y =>
-        Subtype.ext <| by simp only [Subalgebra.coe_mul, map_mul, Subtype.coe_mk] }
+    { toFun := fun k => ⟨algebraMap K L (algebraMap _ K k), IsIntegral.algebraMap k.2⟩
+      map_zero' := by ext; simp only [RingOfIntegers.map_mk, map_zero]
+      map_one' := by ext; simp only [RingOfIntegers.map_mk, map_one]
+      map_add' := fun x y => by ext; simp only [RingOfIntegers.map_mk, map_add]
+      map_mul' := fun x y => by ext; simp only [RingOfIntegers.map_mk, map_mul] }
 #align number_field.ring_of_integers_algebra NumberField.inst_ringOfIntegersAlgebra
 
 -- diamond at `reducible_and_instances` #10906
@@ -102,6 +155,31 @@ namespace RingOfIntegers
 
 variable {K}
 
+/-- The canonical map from `𝓞 K` to `K` is injective.
+
+This is a convenient abbreviation for `NoZeroSMulDivisors.algebraMap_injective`.
+-/
+lemma coe_injective : Function.Injective (algebraMap (𝓞 K) K) :=
+  NoZeroSMulDivisors.algebraMap_injective _ _
+
+/-- The canonical map from `𝓞 K` to `K` is injective.
+
+This is a convenient abbreviation for `map_eq_zero_iff` applied to
+`NoZeroSMulDivisors.algebraMap_injective`.
+-/
+@[simp] lemma coe_eq_zero_iff {x : 𝓞 K} : algebraMap _ K x = 0 ↔ x = 0 :=
+  map_eq_zero_iff _  coe_injective
+
+theorem isIntegral_coe (x : 𝓞 K) : IsIntegral ℤ (algebraMap _ K x) :=
+  x.2
+#align number_field.ring_of_integers.is_integral_coe NumberField.RingOfIntegers.isIntegral_coe
+
+theorem isIntegral (x : 𝓞 K) : IsIntegral ℤ x := by
+  obtain ⟨P, hPm, hP⟩ := x.isIntegral_coe
+  refine' ⟨P, hPm, _⟩
+  rwa [IsScalarTower.algebraMap_eq (S := 𝓞 K), ← Polynomial.hom_eval₂, coe_eq_zero_iff] at hP
+#align number_field.is_integral_of_mem_ring_of_integers NumberField.RingOfIntegers.isIntegral
+
 instance [NumberField K] : IsFractionRing (𝓞 K) K :=
   integralClosure.isFractionRing_of_finite_extension ℚ _
 
@@ -111,15 +189,7 @@ instance : IsIntegralClosure (𝓞 K) ℤ K :=
 instance [NumberField K] : IsIntegrallyClosed (𝓞 K) :=
   integralClosure.isIntegrallyClosedOfFiniteExtension ℚ
 
-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]
-    [FunLike 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
+#noalign number_field.ring_of_integers.map_mem
 
 /-- The ring of integers of `K` are equivalent to any integral closure of `ℤ` in `K` -/
 protected noncomputable def equiv (R : Type*) [CommRing R] [Algebra R K]
@@ -129,7 +199,7 @@ protected noncomputable def equiv (R : Type*) [CommRing R] [Algebra R K]
 
 variable (K)
 
-instance : CharZero (𝓞 K) :=
+instance [CharZero K] : CharZero (𝓞 K) :=
   CharZero.of_module _ K
 
 instance : IsNoetherian ℤ (𝓞 K) :=
@@ -157,6 +227,29 @@ noncomputable def basis : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K
   Free.chooseBasis ℤ (𝓞 K)
 #align number_field.ring_of_integers.basis NumberField.RingOfIntegers.basis
 
+variable {K} {M : Type*}
+
+/-- Given `f : M → K` such that `∀ x, IsIntegral ℤ (f x)`, the corresponding function
+`M → 𝓞 K`. -/
+def restrict (f : M → K) (h : ∀ x, IsIntegral ℤ (f x)) (x : M) : 𝓞 K :=
+  ⟨f x, h x⟩
+
+/-- Given `f : M →+ K` such that `∀ x, IsIntegral ℤ (f x)`, the corresponding function
+`M →+ 𝓞 K`. -/
+def restrict_addMonoidHom [AddZeroClass M] (f : M →+ K) (h : ∀ x, IsIntegral ℤ (f x)) :
+    M →+ 𝓞 K where
+  toFun := restrict f h
+  map_zero' := by simp only [restrict, map_zero, mk_zero]
+  map_add' x y := by simp only [restrict, map_add, mk_add_mk _]
+
+/-- Given `f : M →* K` such that `∀ x, IsIntegral ℤ (f x)`, the corresponding function
+`M →* 𝓞 K`. -/
+@[to_additive existing] -- TODO: why doesn't it figure this out by itself?
+def restrict_monoidHom [MulOneClass M] (f : M →* K) (h : ∀ x, IsIntegral ℤ (f x)) : M →* 𝓞 K where
+  toFun := restrict f h
+  map_one' := by simp only [restrict, map_one, mk_one]
+  map_mul' x y := by simp only [restrict, map_mul, mk_mul_mk _]
+
 end RingOfIntegers
 
 /-- A basis of `K` over `ℚ` that is also a basis of `𝓞 K` over `ℤ`. -/
@@ -171,14 +264,15 @@ theorem integralBasis_apply (i : Free.ChooseBasisIndex ℤ (𝓞 K)) :
 #align number_field.integral_basis_apply NumberField.integralBasis_apply
 
 @[simp]
-theorem integralBasis_repr_apply (x : (𝓞 K)) (i : Free.ChooseBasisIndex ℤ (𝓞 K)):
-    (integralBasis K).repr x i = (algebraMap ℤ ℚ) ((RingOfIntegers.basis K).repr x i) :=
+theorem integralBasis_repr_apply (x : (𝓞 K)) (i : Free.ChooseBasisIndex ℤ (𝓞 K)) :
+    (integralBasis K).repr (algebraMap _ _ x) i =
+      (algebraMap ℤ ℚ) ((RingOfIntegers.basis K).repr x i) :=
   Basis.localizationLocalization_repr_algebraMap ℚ (nonZeroDivisors ℤ) K _ x i
 
 theorem mem_span_integralBasis {x : K} :
-    x ∈ Submodule.span ℤ (Set.range (integralBasis K)) ↔ x ∈ 𝓞 K := by
-  rw [integralBasis, Basis.localizationLocalization_span, Subalgebra.range_isScalarTower_toAlgHom,
-    Subalgebra.mem_toSubmodule]
+    x ∈ Submodule.span ℤ (Set.range (integralBasis K)) ↔ x ∈ (algebraMap (𝓞 K) K).range := by
+  rw [integralBasis, Basis.localizationLocalization_span, LinearMap.mem_range,
+      IsScalarTower.coe_toAlgHom', RingHom.mem_range]
 
 theorem RingOfIntegers.rank : FiniteDimensional.finrank ℤ (𝓞 K) = FiniteDimensional.finrank ℚ K :=
   IsIntegralClosure.rank ℤ ℚ K (𝓞 K)
@@ -201,7 +295,7 @@ instance numberField : NumberField ℚ where
 #align rat.number_field Rat.numberField
 
 /-- The ring of integers of `ℚ` as a number field is just `ℤ`. -/
-noncomputable def ringOfIntegersEquiv : ringOfIntegers ℚ ≃+* ℤ :=
+noncomputable def ringOfIntegersEquiv : 𝓞 ℚ ≃+* ℤ :=
   RingOfIntegers.equiv ℤ
 #align rat.ring_of_integers_equiv Rat.ringOfIntegersEquiv
 

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

@@ -100,7 +100,7 @@ theorem integerLattice.inter_ball_finite [NumberField K] (r : ℝ) :
     convert (Embeddings.finite_of_norm_le K ℂ r).image (canonicalEmbedding K)
     ext; constructor
     · rintro ⟨⟨_, ⟨x, rfl⟩, rfl⟩, hx⟩
-      exact ⟨↑x, ⟨SetLike.coe_mem x, fun φ => (heq x).mp hx φ⟩, rfl⟩
+      exact ⟨x, ⟨SetLike.coe_mem x, fun φ => (heq _).mp hx φ⟩, rfl⟩
     · rintro ⟨x, ⟨hx1, hx2⟩, rfl⟩
       exact ⟨⟨x, ⟨⟨x, hx1⟩, rfl⟩, rfl⟩, (heq x).mpr hx2⟩
 
@@ -142,13 +142,14 @@ theorem latticeBasis_apply [NumberField K] (i : Free.ChooseBasisIndex ℤ (𝓞
     Function.comp_apply, Equiv.apply_symm_apply]
 
 theorem mem_span_latticeBasis [NumberField K] (x : (K →+* ℂ) → ℂ) :
-    x ∈ Submodule.span ℤ (Set.range (latticeBasis K)) ↔ x ∈ canonicalEmbedding K '' (𝓞 K) := by
+    x ∈ Submodule.span ℤ (Set.range (latticeBasis K)) ↔
+      x ∈ ((canonicalEmbedding K).comp (algebraMap (𝓞 K) K)).range := by
   rw [show Set.range (latticeBasis K) =
       (canonicalEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (integralBasis K)) by
     rw [← Set.range_comp]; exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))]
   rw [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe]
-  rw [show (Submodule.span ℤ (Set.range (integralBasis K)) : Set K) = 𝓞 K by
-    ext; exact mem_span_integralBasis K]
+  rw [← RingHom.map_range, Subring.mem_map, Set.mem_image]
+  simp only [SetLike.mem_coe, mem_span_integralBasis K]
   rfl
 
 end NumberField.canonicalEmbedding
@@ -484,13 +485,14 @@ theorem latticeBasis_apply (i : ChooseBasisIndex ℤ (𝓞 K)) :
     canonicalEmbedding.latticeBasis_apply, integralBasis_apply, commMap_canonical_eq_mixed]
 
 theorem mem_span_latticeBasis (x : (E K)) :
-    x ∈ Submodule.span ℤ (Set.range (latticeBasis K)) ↔ x ∈ mixedEmbedding K '' (𝓞 K) := by
+    x ∈ Submodule.span ℤ (Set.range (latticeBasis K)) ↔
+      x ∈ ((mixedEmbedding K).comp (algebraMap (𝓞 K) K)).range := by
   rw [show Set.range (latticeBasis K) =
       (mixedEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (integralBasis K)) by
     rw [← Set.range_comp]; exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))]
   rw [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe]
-  rw [show (Submodule.span ℤ (Set.range (integralBasis K)) : Set K) = 𝓞 K by
-    ext; exact mem_span_integralBasis K]
+  simp only [Set.mem_image, SetLike.mem_coe, mem_span_integralBasis K,
+    RingHom.mem_range, exists_exists_eq_and]
   rfl
 
 theorem mem_rat_span_latticeBasis (x : K) :