Merge branch 'aliu/complete_univ' into aliu/krullTopology

Author: plp127

Counterexamples/Pseudoelement.lean

@@ -65,8 +65,6 @@ theorem snd_x_pseudo_eq_snd_y : PseudoEqual _ (app biprod.snd x) (app biprod.snd
     simp_rw [biprod.lift_snd]; rfl
 
 set_option backward.isDefEq.respectTransparency false in
--- Porting note: locally disable instance to avoid inferred/synthesized clash
-attribute [-instance] AddCommGroup.toIntModule in
 /-- `x` is not pseudoequal to `y`. -/
 theorem x_not_pseudo_eq : ¬PseudoEqual _ x y := by
   intro h

Mathlib.lean

@@ -2046,6 +2046,7 @@ public import Mathlib.Analysis.InnerProductSpace.Convex
 public import Mathlib.Analysis.InnerProductSpace.Defs
 public import Mathlib.Analysis.InnerProductSpace.Dual
 public import Mathlib.Analysis.InnerProductSpace.EuclideanDist
+public import Mathlib.Analysis.InnerProductSpace.ExteriorPower
 public import Mathlib.Analysis.InnerProductSpace.GramMatrix
 public import Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
 public import Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
@@ -4904,6 +4905,7 @@ public import Mathlib.InformationTheory.Coding.UniquelyDecodable
 public import Mathlib.InformationTheory.Hamming
 public import Mathlib.InformationTheory.KullbackLeibler.Basic
 public import Mathlib.InformationTheory.KullbackLeibler.ChainRule
+public import Mathlib.InformationTheory.KullbackLeibler.DataProcessing
 public import Mathlib.InformationTheory.KullbackLeibler.KLFun
 public import Mathlib.Init
 public import Mathlib.Lean.ContextInfo
@@ -6134,6 +6136,7 @@ public import Mathlib.Order.Interval.Finset.Box
 public import Mathlib.Order.Interval.Finset.Defs
 public import Mathlib.Order.Interval.Finset.DenselyOrdered
 public import Mathlib.Order.Interval.Finset.Fin
+public import Mathlib.Order.Interval.Finset.Floor
 public import Mathlib.Order.Interval.Finset.Gaps
 public import Mathlib.Order.Interval.Finset.Nat
 public import Mathlib.Order.Interval.Finset.SuccPred

Mathlib/Algebra/Algebra/Equiv.lean

@@ -777,6 +777,68 @@ end Semiring
 
 end AlgEquiv
 
+namespace RingEquiv
+
+variable {R S : Type*}
+
+/-- Reinterpret a `RingEquiv` as an `ℕ`-algebra isomorphism. -/
+@[simps! -isSimp apply]
+def toNatAlgEquiv [Semiring R] [Semiring S] (f : R ≃+* S) : R ≃ₐ[ℕ] S where
+  toEquiv := f
+  __ := f.toRingHom.toNatAlgHom
+
+@[simp]
+lemma coe_toNatAlgEquiv [Semiring R] [Semiring S] (f : R ≃+* S) :
+    ⇑f.toNatAlgEquiv = ⇑f := rfl
+
+lemma toAlgHom_toNatAlgEquiv [Semiring R] [Semiring S] (f : R ≃+* S) :
+    f.toNatAlgEquiv.toAlgHom = (f : R →+* S).toNatAlgHom := rfl
+
+@[simp]
+lemma symm_toNatAlgEquiv [Semiring R] [Semiring S] (f : R ≃+* S) :
+    f.toNatAlgEquiv.symm = f.symm.toNatAlgEquiv := rfl
+
+variable (R) (S) in
+/-- The equivalence between `RingEquiv` and `ℕ`-algebra isomorphisms. -/
+@[simps apply symm_apply]
+def equivNatAlgEquiv [Semiring R] [Semiring S] : (R ≃+* S) ≃ (R ≃ₐ[ℕ] S) where
+  toFun := toNatAlgEquiv
+  invFun := AlgEquiv.toRingEquiv
+
+lemma toNatAlgEquiv_injective [Semiring R] [Semiring S] :
+    Function.Injective (RingEquiv.toNatAlgEquiv : (R ≃+* S) → _) :=
+  (equivNatAlgEquiv R S).injective
+
+/-- Reinterpret a `RingEquiv` as a `ℤ`-algebra isomorphism. -/
+@[simps! -isSimp apply]
+def toIntAlgEquiv [Ring R] [Ring S] (f : R ≃+* S) : R ≃ₐ[ℤ] S where
+  toEquiv := f
+  __ := f.toRingHom.toIntAlgHom
+
+@[simp]
+lemma coe_toIntAlgEquiv [Ring R] [Ring S] (f : R ≃+* S) :
+    ⇑f.toIntAlgEquiv = ⇑f := rfl
+
+lemma toAlgHom_toIntAlgEquiv [Ring R] [Ring S] (f : R ≃+* S) :
+    f.toIntAlgEquiv.toAlgHom = (f : R →+* S).toIntAlgHom := rfl
+
+@[simp]
+lemma symm_toIntAlgEquiv [Ring R] [Ring S] (f : R ≃+* S) :
+    f.toIntAlgEquiv.symm = f.symm.toIntAlgEquiv := rfl
+
+variable (R) (S) in
+/-- The equivalence between `RingEquiv` and `ℤ`-algebra isomorphisms. -/
+@[simps apply symm_apply]
+def equivIntAlgEquiv [Ring R] [Ring S] : (R ≃+* S) ≃ (R ≃ₐ[ℤ] S) where
+  toFun := toIntAlgEquiv
+  invFun := AlgEquiv.toRingEquiv
+
+lemma toIntAlgEquiv_injective [Ring R] [Ring S] :
+    Function.Injective (RingEquiv.toIntAlgEquiv : (R ≃+* S) → _) :=
+  (equivIntAlgEquiv R S).injective
+
+end RingEquiv
+
 namespace MulSemiringAction
 
 variable {M G : Type*} (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A]

Mathlib/Algebra/Algebra/Hom/Rat.lean

@@ -5,6 +5,7 @@ Authors: Kenny Lau, Yury Kudryashov
 -/
 module
 
+public import Mathlib.Algebra.Algebra.Equiv
 public import Mathlib.Algebra.Algebra.Hom
 public import Mathlib.Algebra.Algebra.Rat
 
@@ -15,43 +16,77 @@ public import Mathlib.Algebra.Algebra.Rat
 
 @[expose] public section
 
+variable {R S : Type*} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S]
 
 namespace RingHom
 
-variable {R S : Type*}
-
 /-- Reinterpret a `RingHom` as a `ℚ`-algebra homomorphism. This actually yields an equivalence,
 see `RingHom.equivRatAlgHom`. -/
-def toRatAlgHom [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) : R →ₐ[ℚ] S :=
+def toRatAlgHom (f : R →+* S) : R →ₐ[ℚ] S :=
   { f with commutes' := f.map_rat_algebraMap }
 
 @[simp]
-theorem toRatAlgHom_toRingHom [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) :
+theorem toRatAlgHom_toRingHom (f : R →+* S) :
     ↑f.toRatAlgHom = f :=
   RingHom.ext fun _x => rfl
 
 @[simp]
-theorem toRatAlgHom_apply [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) (x : R) :
+theorem toRatAlgHom_apply (f : R →+* S) (x : R) :
     f.toRatAlgHom x = f x :=
   rfl
 
 end RingHom
 
-section
-
-variable {R S : Type*}
-
 @[simp]
-theorem AlgHom.toRingHom_toRatAlgHom [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S]
-    (f : R →ₐ[ℚ] S) : (f : R →+* S).toRatAlgHom = f :=
+theorem AlgHom.toRingHom_toRatAlgHom (f : R →ₐ[ℚ] S) : (f : R →+* S).toRatAlgHom = f :=
   AlgHom.ext fun _x => rfl
 
 variable (R) (S) in
 /-- The equivalence between `RingHom` and `ℚ`-algebra homomorphisms. -/
 @[simps]
-def RingHom.equivRatAlgHom [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] :
-    (R →+* S) ≃ (R →ₐ[ℚ] S) where
+def RingHom.equivRatAlgHom : (R →+* S) ≃ (R →ₐ[ℚ] S) where
   toFun := RingHom.toRatAlgHom
   invFun := AlgHom.toRingHom
 
-end
+namespace RingEquiv
+
+/-- Reinterpret a `RingEquiv` as a `ℚ`-algebra isomorphism. This actually yields an
+equivalence, see `RingEquiv.equivRatAlgEquiv`. -/
+@[simps! -isSimp apply]
+def toRatAlgEquiv (f : R ≃+* S) : R ≃ₐ[ℚ] S where
+  toEquiv := f
+  __ := f.toRingHom.toRatAlgHom
+
+@[simp]
+theorem coe_toRatAlgEquiv (f : R ≃+* S) : ⇑f.toRatAlgEquiv = ⇑f := rfl
+
+@[simp]
+theorem toRingEquiv_toRatAlgEquiv (f : R ≃+* S) :
+    f.toRatAlgEquiv = f :=
+  rfl
+
+theorem toAlgHom_toRatAlgEquiv (f : R ≃+* S) :
+    f.toRatAlgEquiv.toAlgHom = (f : R →+* S).toRatAlgHom :=
+  rfl
+
+@[simp]
+theorem symm_toRatAlgEquiv (f : R ≃+* S) :
+    f.toRatAlgEquiv.symm = f.symm.toRatAlgEquiv :=
+  rfl
+
+end RingEquiv
+
+@[simp]
+theorem AlgEquiv.toRatAlgEquiv_toRingEquiv (f : R ≃ₐ[ℚ] S) : (f : R ≃+* S).toRatAlgEquiv = f :=
+  rfl
+
+variable (R) (S) in
+/-- The equivalence between `RingEquiv` and `ℚ`-algebra isomorphisms. -/
+@[simps apply symm_apply]
+def RingEquiv.equivRatAlgEquiv : (R ≃+* S) ≃ (R ≃ₐ[ℚ] S) where
+  toFun := RingEquiv.toRatAlgEquiv
+  invFun := AlgEquiv.toRingEquiv
+
+lemma RingEquiv.toRatAlgEquiv_injective :
+    Function.Injective (RingEquiv.toRatAlgEquiv : (R ≃+* S) → _) :=
+  (RingEquiv.equivRatAlgEquiv R S).injective

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -316,6 +316,46 @@ instance botCharacteristic : Characteristic (⊥ : Subgroup G) :=
 instance topCharacteristic : Characteristic (⊤ : Subgroup G) :=
   characteristic_iff_map_le.mpr fun _ϕ => le_top
 
+@[to_additive]
+instance characteristic_sup [H.Characteristic] [K.Characteristic] :
+    (H ⊔ K).Characteristic := by
+  simp_all [characteristic_iff_map_eq, map_sup]
+
+@[to_additive]
+instance characteristic_iSup {ι : Sort*} {H : ι → Subgroup G} [∀ i, (H i).Characteristic] :
+    (⨆ i, H i).Characteristic := by
+  simp_all [characteristic_iff_map_eq, map_iSup]
+
+@[to_additive]
+theorem characteristic_biSup {ι : Type*} {s : Set ι} {H : ι → Subgroup G}
+    (h : ∀ i ∈ s, (H i).Characteristic) : (⨆ i ∈ s, H i).Characteristic := by
+  simp [← iSup_subtype'', characteristic_iSup, h]
+
+@[to_additive]
+theorem characteristic_sSup {Hs : Set (Subgroup G)} (h : ∀ H ∈ Hs, H.Characteristic) :
+    (sSup Hs).Characteristic := by
+  simp [sSup_eq_iSup', characteristic_iSup, h]
+
+@[to_additive]
+instance characteristic_inf [H.Characteristic] [K.Characteristic] :
+    (H ⊓ K).Characteristic := by
+  simp_all [characteristic_iff_comap_eq, comap_inf]
+
+@[to_additive]
+instance characteristic_iInf {ι : Sort*} {H : ι → Subgroup G} [∀ i, (H i).Characteristic] :
+    (⨅ i, H i).Characteristic := by
+  simp_all [characteristic_iff_comap_eq, comap_iInf]
+
+@[to_additive]
+theorem characteristic_biInf {ι : Type*} {s : Set ι} {H : ι → Subgroup G}
+    (h : ∀ i ∈ s, (H i).Characteristic) : (⨅ i ∈ s, H i).Characteristic := by
+  simp [← iInf_subtype'', characteristic_iInf, h]
+
+@[to_additive]
+theorem characteristic_sInf {Hs : Set (Subgroup G)} (h : ∀ H ∈ Hs, H.Characteristic) :
+    (sInf Hs).Characteristic := by
+  simp [sInf_eq_iInf', characteristic_iInf, h]
+
 /-- If `H` is a characteristic subgroup of `G`, then every automorphism of `G` induces an
 automorphism of `H`. -/
 @[to_additive (attr := simps!)

Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

@@ -372,7 +372,7 @@ variable [CompleteSpace F]
 /-- The set of differentiability points of a function taking values in a complete space is
 Borel-measurable. -/
 theorem measurableSet_of_differentiableAt : MeasurableSet { x | DifferentiableAt 𝕜 f x } := by
-  have : IsComplete (univ : Set (E →L[𝕜] F)) := complete_univ
+  have : IsComplete (univ : Set (E →L[𝕜] F)) := isComplete_univ
   convert! measurableSet_of_differentiableAt_of_isComplete 𝕜 f this
   simp
 
@@ -700,7 +700,7 @@ variable [CompleteSpace F]
 Borel-measurable. -/
 theorem measurableSet_of_differentiableWithinAt_Ici :
     MeasurableSet { x | DifferentiableWithinAt ℝ f (Ici x) x } := by
-  have : IsComplete (univ : Set F) := complete_univ
+  have : IsComplete (univ : Set F) := isComplete_univ
   convert! measurableSet_of_differentiableWithinAt_Ici_of_isComplete f this
   simp
 
@@ -893,7 +893,7 @@ variable [CompleteSpace F]
 values in a complete space is Borel-measurable. -/
 theorem measurableSet_of_differentiableAt_with_param (hf : Continuous f.uncurry) :
     MeasurableSet {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2} := by
-  have : IsComplete (univ : Set (E →L[𝕜] F)) := complete_univ
+  have : IsComplete (univ : Set (E →L[𝕜] F)) := isComplete_univ
   convert! measurableSet_of_differentiableAt_of_isComplete_with_param hf this
   simp
 

Mathlib/Analysis/Convex/Continuous.lean

@@ -233,3 +233,96 @@ protected lemma ConcaveOn.locallyLipschitz (hf : ConcaveOn ℝ univ f) : Locally
 
 -- proof_wanted ConcaveOn.continuousOn_intrinsicInterior (hf : ConcaveOn ℝ C f) :
 --     ContinuousOn f (intrinsicInterior ℝ C)
+
+section Intervals
+
+lemma ConvexOn.continuousOn_Ici {f : ℝ → ℝ} {y : ℝ} (hf_cvx : ConvexOn ℝ (Ici y) f)
+    (hf_cont : ContinuousWithinAt f (Ici y) y) :
+    ContinuousOn f (Ici y) := by
+  intro x hx
+  rcases eq_or_lt_of_le (α := ℝ) hx with rfl | hxy
+  · exact hf_cont
+  · have h := hf_cvx.continuousOn_interior x
+    simp only [nonempty_Iio, interior_Ici', mem_Ioi] at h
+    rw [continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hxy)] at h
+    exact (h hxy).continuousWithinAt
+
+lemma ConcaveOn.continuousOn_Ici {f : ℝ → ℝ} {y : ℝ} (hf_cnv : ConcaveOn ℝ (Ici y) f)
+    (hf_cont : ContinuousWithinAt f (Ici y) y) :
+    ContinuousOn f (Ici y) := by
+  simpa using hf_cnv.neg.continuousOn_Ici hf_cont.neg
+
+lemma ConvexOn.continuousOn_Iic {f : ℝ → ℝ} {y : ℝ} (hf_cvx : ConvexOn ℝ (Iic y) f)
+    (hf_cont : ContinuousWithinAt f (Iic y) y) :
+    ContinuousOn f (Iic y) := by
+  intro x hx
+  rcases eq_or_lt_of_le (α := ℝ) hx with rfl | hxy
+  · exact hf_cont
+  · have h := hf_cvx.continuousOn_interior x
+    simp only [nonempty_Ioi, interior_Iic', mem_Iio] at h
+    rw [continuousWithinAt_iff_continuousAt (Iio_mem_nhds hxy)] at h
+    exact (h hxy).continuousWithinAt
+
+lemma ConcaveOn.continuousOn_Iic {f : ℝ → ℝ} {y : ℝ} (hf_cnv : ConcaveOn ℝ (Iic y) f)
+    (hf_cont : ContinuousWithinAt f (Iic y) y) :
+    ContinuousOn f (Iic y) := by
+  simpa using hf_cnv.neg.continuousOn_Iic hf_cont.neg
+
+lemma ConvexOn.continuousOn_Ioc {f : ℝ → ℝ} {y z : ℝ} (hf_cvx : ConvexOn ℝ (Ioc y z) f)
+    (hf_cont : ContinuousWithinAt f (Iic z) z) :
+    ContinuousOn f (Ioc y z) := by
+  intro x hx
+  rcases eq_or_lt_of_le (α := ℝ) hx.2 with rfl | hxz
+  · rw [continuousWithinAt_Ioc_iff_Iic hx.1]
+    exact hf_cont
+  · have h := hf_cvx.continuousOn_interior x
+    simp only [interior_Ioc, mem_Ioo, hx.1, hxz, and_self, forall_const] at h
+    rw [continuousWithinAt_iff_continuousAt (Ioo_mem_nhds hx.1 hxz)] at h
+    exact h.continuousWithinAt
+
+lemma ConcaveOn.continuousOn_Ioc {f : ℝ → ℝ} {y z : ℝ} (hf_cnv : ConcaveOn ℝ (Ioc y z) f)
+    (hf_cont : ContinuousWithinAt f (Iic z) z) :
+    ContinuousOn f (Ioc y z) := by
+  simpa using hf_cnv.neg.continuousOn_Ioc hf_cont.neg
+
+lemma ConvexOn.continuousOn_Ico {f : ℝ → ℝ} {y z : ℝ} (hf_cvx : ConvexOn ℝ (Ico y z) f)
+    (hf_cont : ContinuousWithinAt f (Ici y) y) :
+    ContinuousOn f (Ico y z) := by
+  intro x hx
+  rcases eq_or_lt_of_le (α := ℝ) hx.1 with rfl | hyx
+  · rw [continuousWithinAt_Ico_iff_Ici hx.2]
+    exact hf_cont
+  · have h := hf_cvx.continuousOn_interior x
+    simp only [interior_Ico, mem_Ioo, hyx, hx.2, and_self, forall_const] at h
+    rw [continuousWithinAt_iff_continuousAt (Ioo_mem_nhds hyx hx.2)] at h
+    exact h.continuousWithinAt
+
+lemma ConcaveOn.continuousOn_Ico {f : ℝ → ℝ} {y z : ℝ} (hf_cnv : ConcaveOn ℝ (Ico y z) f)
+    (hf_cont : ContinuousWithinAt f (Ici y) y) :
+    ContinuousOn f (Ico y z) := by
+  simpa using hf_cnv.neg.continuousOn_Ico hf_cont.neg
+
+lemma ConvexOn.continuousOn_Icc {f : ℝ → ℝ} {y z : ℝ} (hf_cvx : ConvexOn ℝ (Icc y z) f)
+    (hyz : y < z)
+    (hfy : ContinuousWithinAt f (Ici y) y) (hfz : ContinuousWithinAt f (Iic z) z) :
+    ContinuousOn f (Icc y z) := by
+  suffices ContinuousOn f (Ico y z) ∧ ContinuousOn f (Ioc y z) by
+    intro x hx
+    rcases eq_or_lt_of_le (α := ℝ) hx.1 with rfl | hyx
+    · exact hfy.mono (by grind)
+    rcases eq_or_lt_of_le (α := ℝ) hx.2 with rfl | hxz
+    · exact hfz.mono (by grind)
+    have hx := this.1 x (by grind)
+    rw [continuousWithinAt_iff_continuousAt (Ico_mem_nhds hyx hxz)] at hx
+    exact hx.continuousWithinAt
+  refine ⟨ConvexOn.continuousOn_Ico ?_ hfy, ConvexOn.continuousOn_Ioc ?_ hfz⟩
+  · exact hf_cvx.subset Ico_subset_Icc_self (convex_Ico y z)
+  · exact hf_cvx.subset Ioc_subset_Icc_self (convex_Ioc y z)
+
+lemma ConcaveOn.continuousOn_Icc {f : ℝ → ℝ} {y z : ℝ} (hf_cnv : ConcaveOn ℝ (Icc y z) f)
+    (hyz : y < z)
+    (hfy : ContinuousWithinAt f (Ici y) y) (hfz : ContinuousWithinAt f (Iic z) z) :
+    ContinuousOn f (Icc y z) := by
+  simpa using hf_cnv.neg.continuousOn_Icc hyz hfy.neg hfz.neg
+
+end Intervals

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

@@ -68,8 +68,6 @@ namespace ContinuousLinearMap
 
 variable [CompleteSpace E] [CompleteSpace G]
 
--- Note: made noncomputable to stop excess compilation
--- https://github.com/leanprover-community/mathlib4/issues/7103
 /-- The adjoint, as a continuous conjugate-linear map. This is only meant as an auxiliary
 definition for the main definition `adjoint`, where this is bundled as a conjugate-linear isometric
 equivalence. -/