From c10d9bc1c8e481eb623c555f57897eab3a1fb24d Mon Sep 17 00:00:00 2001 From: Noah Walker <30136151+NoahW314@users.noreply.github.com> Date: Mon, 3 Aug 2026 08:23:08 +0000 Subject: [PATCH 01/16] chore: rename `FiniteMultiplicity.not_unit` to `FiniteMultiplicity.not_isUnit` (#42390) Co-authored-by: NoahW314 --- Mathlib/RingTheory/Multiplicity.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/Mathlib/RingTheory/Multiplicity.lean b/Mathlib/RingTheory/Multiplicity.lean index 32e3fff999..307d2ecda3 100644 --- a/Mathlib/RingTheory/Multiplicity.lean +++ b/Mathlib/RingTheory/Multiplicity.lean @@ -185,10 +185,13 @@ theorem FiniteMultiplicity.not_iff_forall : ¬FiniteMultiplicity a b ↔ ∀ n : (by simpa [FiniteMultiplicity] using h), by simp [FiniteMultiplicity]; tauto⟩ -theorem FiniteMultiplicity.not_unit (h : FiniteMultiplicity a b) : ¬IsUnit a := +theorem FiniteMultiplicity.not_isUnit (h : FiniteMultiplicity a b) : ¬IsUnit a := let ⟨n, hn⟩ := h hn ∘ IsUnit.dvd ∘ IsUnit.pow (n + 1) +@[deprecated (since := "2026-08-02")] +alias FiniteMultiplicity.not_unit := FiniteMultiplicity.not_isUnit + theorem FiniteMultiplicity.mul_left {c : α} : FiniteMultiplicity a (b * c) → FiniteMultiplicity a b := fun ⟨n, hn⟩ => ⟨n, fun h => hn (h.trans (dvd_mul_right _ _))⟩ @@ -290,7 +293,7 @@ theorem emultiplicity_eq_ofNat {a b n : ℕ} [n.AtLeastTwo] : @[simp] theorem FiniteMultiplicity.not_of_isUnit_left (b : α) (ha : IsUnit a) : ¬FiniteMultiplicity a b := - (·.not_unit ha) + (·.not_isUnit ha) theorem FiniteMultiplicity.not_of_one_left (b : α) : ¬ FiniteMultiplicity 1 b := by simp @@ -667,7 +670,7 @@ theorem multiplicity_self {a : α} : multiplicity a a = 1 := by simp only [sq, mul_assoc, mul_eq_mul_left_iff] at hv obtain hv | rfl := hv · have : IsUnit a := .of_mul_eq_one v hv.symm - simpa [this] using ha.not_unit + simpa [this] using ha.not_isUnit · simpa using ha.ne_zero · simp [ha] From 64e0afda5236d382ce3267152e03fe3f2ef46944 Mon Sep 17 00:00:00 2001 From: Felix Pernegger <188575194+felixpernegger@users.noreply.github.com> Date: Mon, 3 Aug 2026 08:55:58 +0000 Subject: [PATCH 02/16] doc(Topology): fix typo in weak space docstring (#42379) Co-authored-by: Batixx --- Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean b/Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean index 2651255c98..5ccc1d3c8d 100644 --- a/Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean +++ b/Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean @@ -196,7 +196,7 @@ end Ring end WeakDual -/-- The weak topology is the topology coarsest topology on `E` such that all functionals +/-- The weak topology is the coarsest topology on `E` such that all functionals `fun x => v x` are continuous. -/ def WeakSpace (𝕜 E) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] := From c0032752b47af314b015a7b411123fa4ac99bbaf Mon Sep 17 00:00:00 2001 From: Noah Walker <30136151+NoahW314@users.noreply.github.com> Date: Mon, 3 Aug 2026 08:56:01 +0000 Subject: [PATCH 03/16] chore: rename `Prime.not_unit` to `Prime.not_isUnit` (#42385) Co-authored-by: NoahW314 --- Mathlib/Algebra/BigOperators/Associated.lean | 2 +- Mathlib/Algebra/GroupWithZero/Associated.lean | 2 +- Mathlib/Algebra/IsPrimePow.lean | 2 +- Mathlib/Algebra/Prime/Defs.lean | 13 ++++++++----- Mathlib/Algebra/Squarefree/Basic.lean | 2 +- Mathlib/Data/Nat/Multiplicity.lean | 4 ++-- Mathlib/NumberTheory/FLT/Three.lean | 2 +- Mathlib/RingTheory/ChainOfDivisors.lean | 6 +++--- Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean | 2 +- Mathlib/RingTheory/Multiplicity.lean | 8 ++++---- .../Polynomial/Cyclotomic/Factorization.lean | 2 +- Mathlib/RingTheory/Polynomial/RationalRoot.lean | 4 ++-- .../RingTheory/UniqueFactorizationDomain/Basic.lean | 7 ++++--- .../RingTheory/UniqueFactorizationDomain/Defs.lean | 2 +- .../UniqueFactorizationDomain/FactorSet.lean | 2 +- .../UniqueFactorizationDomain/Multiplicity.lean | 2 +- .../NormalizedFactors.lean | 4 ++-- Mathlib/RingTheory/Unramified/LocalStructure.lean | 2 +- Mathlib/RingTheory/Valuation/PrimeMultiplicity.lean | 5 +++-- 19 files changed, 39 insertions(+), 34 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Associated.lean b/Mathlib/Algebra/BigOperators/Associated.lean index e87c5cd634..1c2fd5b822 100644 --- a/Mathlib/Algebra/BigOperators/Associated.lean +++ b/Mathlib/Algebra/BigOperators/Associated.lean @@ -73,7 +73,7 @@ theorem Associated.prod {M : Type*} [CommMonoid M] {ι : Type*} (s : Finset ι) theorem exists_associated_mem_of_dvd_prod [CommMonoidWithZero M₀] [IsCancelMulZero M₀] {p : M₀} (hp : Prime p) {s : Multiset M₀} : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q := - Multiset.induction_on s (by simp [mt isUnit_iff_dvd_one.2 hp.not_unit]) fun a s ih hs hps => by + Multiset.induction_on s (by simp [mt isUnit_iff_dvd_one.2 hp.not_isUnit]) fun a s ih hs hps => by rw [Multiset.prod_cons] at hps rcases hp.dvd_or_dvd hps with h | h · have hap := hs a (Multiset.mem_cons.2 (Or.inl rfl)) diff --git a/Mathlib/Algebra/GroupWithZero/Associated.lean b/Mathlib/Algebra/GroupWithZero/Associated.lean index de3d8bd038..e3ffb429a6 100644 --- a/Mathlib/Algebra/GroupWithZero/Associated.lean +++ b/Mathlib/Algebra/GroupWithZero/Associated.lean @@ -234,7 +234,7 @@ protected theorem Associated.prime [CommMonoidWithZero M] {p q : M} (h : p ~ᵤ Prime q := ⟨h.ne_zero_iff.1 hp.ne_zero, let ⟨u, hu⟩ := h - ⟨fun ⟨v, hv⟩ => hp.not_unit ⟨v * u⁻¹, by simp [hv, hu.symm]⟩, by + ⟨fun ⟨v, hv⟩ => hp.not_isUnit ⟨v * u⁻¹, by simp [hv, hu.symm]⟩, by rw [← hu] simp only [Units.isUnit, IsUnit.mul_right_dvd] intro a b diff --git a/Mathlib/Algebra/IsPrimePow.lean b/Mathlib/Algebra/IsPrimePow.lean index 2db84a2c50..54089849dd 100644 --- a/Mathlib/Algebra/IsPrimePow.lean +++ b/Mathlib/Algebra/IsPrimePow.lean @@ -45,7 +45,7 @@ theorem not_isPrimePow_zero [NoZeroDivisors R] : ¬IsPrimePow (0 : R) := by theorem IsPrimePow.not_unit {n : R} (h : IsPrimePow n) : ¬IsUnit n := let ⟨_p, _k, hp, hk, hn⟩ := h - hn ▸ (isUnit_pow_iff hk.ne').not.mpr hp.not_unit + hn ▸ (isUnit_pow_iff hk.ne').not.mpr hp.not_isUnit theorem IsUnit.not_isPrimePow {n : R} (h : IsUnit n) : ¬IsPrimePow n := fun h' => h'.not_unit h diff --git a/Mathlib/Algebra/Prime/Defs.lean b/Mathlib/Algebra/Prime/Defs.lean index 47228fb3dd..dd31ae9758 100644 --- a/Mathlib/Algebra/Prime/Defs.lean +++ b/Mathlib/Algebra/Prime/Defs.lean @@ -51,11 +51,14 @@ include hp theorem ne_zero : p ≠ 0 := hp.1 -theorem not_unit : ¬IsUnit p := +theorem not_isUnit : ¬IsUnit p := hp.2.1 +@[deprecated (since := "2026-08-02")] +alias not_unit := not_isUnit + theorem not_dvd_one : ¬p ∣ 1 := - mt (isUnit_of_dvd_one ·) hp.not_unit + mt (isUnit_of_dvd_one ·) hp.not_isUnit theorem ne_one : p ≠ 1 := fun h => hp.2.1 (h.symm ▸ isUnit_one) @@ -76,7 +79,7 @@ theorem dvd_of_dvd_pow {a : M} {n : ℕ} (h : p ∣ a ^ n) : p ∣ a := by | zero => rw [pow_zero] at h have := isUnit_of_dvd_one h - have := not_unit hp + have := not_isUnit hp contradiction | succ n ih => rw [pow_succ'] at h @@ -93,7 +96,7 @@ end Prime theorem not_prime_zero : ¬Prime (0 : M) := fun h => h.ne_zero rfl @[simp] -theorem not_prime_one : ¬Prime (1 : M) := fun h => h.not_unit isUnit_one +theorem not_prime_one : ¬Prime (1 : M) := fun h => h.not_isUnit isUnit_one end Prime @@ -147,7 +150,7 @@ section CancelCommMonoidWithZero variable [CommMonoidWithZero M] [IsCancelMulZero M] {p : M} protected theorem Prime.irreducible (hp : Prime p) : Irreducible p := - ⟨hp.not_unit, fun a b ↦ by + ⟨hp.not_isUnit, fun a b ↦ by rintro rfl exact (hp.dvd_or_dvd dvd_rfl).symm.imp (isUnit_of_dvd_one <| (mul_dvd_mul_iff_right <| right_ne_zero_of_mul hp.ne_zero).mp <| diff --git a/Mathlib/Algebra/Squarefree/Basic.lean b/Mathlib/Algebra/Squarefree/Basic.lean index 0730696dc8..a3fb87e99d 100644 --- a/Mathlib/Algebra/Squarefree/Basic.lean +++ b/Mathlib/Algebra/Squarefree/Basic.lean @@ -185,7 +185,7 @@ theorem pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right {k : ℕ} p ^ k ∣ y := by by_cases hxp : p ∣ x · obtain ⟨x', rfl⟩ := hxp - have hx' : ¬ p ∣ x' := fun contra ↦ hp.not_unit <| hx p (mul_dvd_mul_left p contra) + have hx' : ¬ p ∣ x' := fun contra ↦ hp.not_isUnit <| hx p (mul_dvd_mul_left p contra) replace h : p ^ k ∣ x' * y := by rw [pow_succ', mul_assoc] at h exact (mul_dvd_mul_iff_left hp.ne_zero).mp h diff --git a/Mathlib/Data/Nat/Multiplicity.lean b/Mathlib/Data/Nat/Multiplicity.lean index 9a65a42698..46024dc213 100644 --- a/Mathlib/Data/Nat/Multiplicity.lean +++ b/Mathlib/Data/Nat/Multiplicity.lean @@ -79,7 +79,7 @@ theorem emultiplicity_eq_card_pow_dvd {m n b : ℕ} (hm : m ≠ 1) (hn : 0 < n) namespace Prime theorem emultiplicity_one {p : ℕ} (hp : p.Prime) : emultiplicity p 1 = 0 := - emultiplicity_of_one_right hp.prime.not_unit + emultiplicity_of_one_right hp.prime.not_isUnit theorem emultiplicity_mul {p m n : ℕ} (hp : p.Prime) : emultiplicity p (m * n) = emultiplicity p m + emultiplicity p n := @@ -93,7 +93,7 @@ theorem emultiplicity_self {p : ℕ} (hp : p.Prime) : emultiplicity p p = 1 := (Nat.finiteMultiplicity_iff.2 ⟨hp.ne_one, hp.pos⟩).emultiplicity_self theorem emultiplicity_pow_self {p n : ℕ} (hp : p.Prime) : emultiplicity p (p ^ n) = n := - _root_.emultiplicity_pow_self hp.ne_zero hp.prime.not_unit n + _root_.emultiplicity_pow_self hp.ne_zero hp.prime.not_isUnit n /-- **Legendre's Theorem** diff --git a/Mathlib/NumberTheory/FLT/Three.lean b/Mathlib/NumberTheory/FLT/Three.lean index 3741a513e2..272b0dff8b 100644 --- a/Mathlib/NumberTheory/FLT/Three.lean +++ b/Mathlib/NumberTheory/FLT/Three.lean @@ -212,7 +212,7 @@ variable [NumberField K] [IsCyclotomicExtension {3} ℚ K] /-- For any `S' : Solution'`, the multiplicity of `λ` in `S'.c` is finite. -/ lemma Solution'.multiplicity_lambda_c_finite : FiniteMultiplicity (hζ.toInteger - 1) S'.c := - .of_not_isUnit hζ.zeta_sub_one_prime'.not_unit S'.hc + .of_not_isUnit hζ.zeta_sub_one_prime'.not_isUnit S'.hc /-- Given `S' : Solution'`, `S'.multiplicity` is the multiplicity of `λ` in `S'.c`, as a natural number. -/ diff --git a/Mathlib/RingTheory/ChainOfDivisors.lean b/Mathlib/RingTheory/ChainOfDivisors.lean index 908e92259e..90fcb0b18e 100644 --- a/Mathlib/RingTheory/ChainOfDivisors.lean +++ b/Mathlib/RingTheory/ChainOfDivisors.lean @@ -75,7 +75,7 @@ theorem exists_chain_of_prime_pow {p : Associates M} {n : ℕ} (hn : n ≠ 0) (h exact Nat.lt_succ_of_le (Nat.one_le_iff_ne_zero.mpr hn) · exact Associates.dvdNotUnit_iff_lt.mp ⟨pow_ne_zero n hp.ne_zero, p ^ (m - n : ℕ), - not_isUnit_of_not_isUnit_dvd hp.not_unit (dvd_pow dvd_rfl (Nat.sub_pos_of_lt h).ne'), + not_isUnit_of_not_isUnit_dvd hp.not_isUnit (dvd_pow dvd_rfl (Nat.sub_pos_of_lt h).ne'), (pow_mul_pow_sub p h.le).symm⟩ · obtain ⟨i, i_le, hi⟩ := (dvd_prime_pow hp n).1 h rw [associated_iff_eq] at hi @@ -118,7 +118,7 @@ theorem eq_second_of_chain_of_prime_dvd {p q r : Associates M} {n : ℕ} (hn : n · rw [Fin.le_iff_val_le_val, Fin.val_one, Nat.succ_le_iff, ← Fin.val_zero (n.succ + 1), ← Fin.lt_def, Fin.pos_iff_ne_zero] rintro rfl - exact hp.not_unit (first_of_chain_isUnit h₁ @h₂) + exact hp.not_isUnit (first_of_chain_isUnit h₁ @h₂) obtain rfl | ⟨j, rfl⟩ := i.eq_zero_or_eq_succ · cases hi refine @@ -289,7 +289,7 @@ theorem map_prime_of_factor_orderIso {m p : Associates M} {n : Associates N} (hn · rw [Ne, ← Associates.isUnit_iff_eq_bot, Associates.isUnit_iff_eq_one, coe_factor_orderIso_map_eq_one_iff _ d] rintro rfl - exact (prime_of_normalized_factor 1 hp).not_unit isUnit_one + exact (prime_of_normalized_factor 1 hp).not_isUnit isUnit_one · have : b ≤ n := le_trans (le_of_lt hb) (d ⟨p, dvd_of_mem_normalizedFactors hp⟩).prop obtain ⟨x, hx⟩ := d.surjective ⟨b, this⟩ rw [← Subtype.coe_mk (p := (· ≤ n)) b this, ← hx] at hb diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean index b80abb2c4a..5bec1fe98c 100644 --- a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean +++ b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean @@ -102,7 +102,7 @@ theorem isPrime_of_prime {P : Ideal A} (h : Prime P) : IsPrime P := by refine ⟨?_, fun hxy => ?_⟩ · rintro rfl rw [← one_eq_top] at h - exact h.not_unit isUnit_one + exact h.not_isUnit isUnit_one · simp only [← dvd_span_singleton, ← span_singleton_mul_span_singleton] at hxy ⊢ exact h.dvd_or_dvd hxy diff --git a/Mathlib/RingTheory/Multiplicity.lean b/Mathlib/RingTheory/Multiplicity.lean index 307d2ecda3..3738ea2d55 100644 --- a/Mathlib/RingTheory/Multiplicity.lean +++ b/Mathlib/RingTheory/Multiplicity.lean @@ -709,13 +709,13 @@ theorem Finset.emultiplicity_prod {β : Type*} {p : α} (hp : Prime p) (s : Fins induction s using Finset.induction with | empty => simp only [Finset.sum_empty, Finset.prod_empty] - exact emultiplicity_of_one_right hp.not_unit + exact emultiplicity_of_one_right hp.not_isUnit | insert a s has ih => simpa [has, ← ih] using emultiplicity_mul hp theorem emultiplicity_pow {p a : α} (hp : Prime p) {k : ℕ} : emultiplicity p (a ^ k) = k * emultiplicity p a := by induction k with - | zero => simp [emultiplicity_of_one_right hp.not_unit] + | zero => simp [emultiplicity_of_one_right hp.not_isUnit] | succ k hk => simp [pow_succ, emultiplicity_mul hp, hk, add_mul] protected theorem FiniteMultiplicity.multiplicity_pow {p a : α} (hp : Prime p) @@ -736,11 +736,11 @@ theorem multiplicity_pow_self {p : α} (h0 : p ≠ 0) (hu : ¬IsUnit p) (n : ℕ theorem emultiplicity_pow_self_of_prime {p : α} (hp : Prime p) (n : ℕ) : emultiplicity p (p ^ n) = n := - emultiplicity_pow_self hp.ne_zero hp.not_unit n + emultiplicity_pow_self hp.ne_zero hp.not_isUnit n theorem multiplicity_pow_self_of_prime {p : α} (hp : Prime p) (n : ℕ) : multiplicity p (p ^ n) = n := - multiplicity_pow_self hp.ne_zero hp.not_unit n + multiplicity_pow_self hp.ne_zero hp.not_isUnit n end CancelCommMonoidWithZero diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Factorization.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Factorization.lean index 2d1410358a..431665ffb3 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Factorization.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Factorization.lean @@ -159,7 +159,7 @@ theorem normalizedFactors_cyclotomic_card : (normalizedFactors (cyclotomic n K)) (pos_of_ne_zero <| f_ne_zero hK) _ _).mp (hn.pow_left f)) ((CharP.cast_eq_zero_iff K p _).mp H) have hP : P ∈ normalizedFactors (cyclotomic n K) := count_pos.mp (by lia) - refine (prime_of_normalized_factor _ hP).not_unit (squarefree_cyclotomic n K P ?_) + refine (prime_of_normalized_factor _ hP).not_isUnit (squarefree_cyclotomic n K P ?_) have : {P, P} ≤ normalizedFactors (cyclotomic n K) := by refine le_iff_count.mpr (fun Q ↦ ?_) by_cases hQ : Q = P diff --git a/Mathlib/RingTheory/Polynomial/RationalRoot.lean b/Mathlib/RingTheory/Polynomial/RationalRoot.lean index ce4be7bb11..5afbbad979 100644 --- a/Mathlib/RingTheory/Polynomial/RationalRoot.lean +++ b/Mathlib/RingTheory/Polynomial/RationalRoot.lean @@ -74,7 +74,7 @@ theorem num_dvd_of_is_root {p : A[X]} {r : K} (hr : aeval r p = 0) : num A r ∣ · simp_all [nonZeroDivisors.coe_ne_zero] · refine dvd_of_dvd_mul_left_of_no_prime_factors hr ?_ this intro q dvd_num dvd_denom_pow hq - apply hq.not_unit + apply hq.not_isUnit exact num_den_reduced A r dvd_num (hq.dvd_of_dvd_pow dvd_denom_pow) convert! dvd_term_of_isRoot_of_dvd_terms 0 (num_isRoot_scaleRoots_of_aeval_eq_zero hr) _ · rw [pow_zero, mul_one] @@ -93,7 +93,7 @@ theorem den_dvd_of_is_root {p : A[X]} {r : K} (hr : aeval r p = 0) : dvd_of_dvd_mul_left_of_no_prime_factors (mem_nonZeroDivisors_iff_ne_zero.mp (den A r).2) ?_ this intro q dvd_den dvd_num_pow hq - apply hq.not_unit + apply hq.not_isUnit exact num_den_reduced A r (hq.dvd_of_dvd_pow dvd_num_pow) dvd_den rw [← coeff_scaleRoots_natDegree] apply dvd_term_of_isRoot_of_dvd_terms _ (num_isRoot_scaleRoots_of_aeval_eq_zero hr) diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean b/Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean index 9481b12ea0..cf1ec92d32 100644 --- a/Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean +++ b/Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean @@ -80,7 +80,7 @@ theorem prime_factors_unique [CommMonoidWithZero α] [IsCancelMulZero α] : exact Multiset.rel_zero_left.2 <| Multiset.eq_zero_of_forall_notMem fun x hx => have : IsUnit g.prod := by simpa [associated_one_iff_isUnit] using h.symm - (hg x hx).not_unit <| + (hg x hx).not_isUnit <| isUnit_iff_dvd_one.2 <| (Multiset.dvd_prod hx).trans (isUnit_iff_dvd_one.1 this) | cons p f ih => intro g hf hg hfg @@ -420,8 +420,9 @@ variable {R : Type*} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] theorem isRelPrime_iff_no_prime_factors {a b : R} (ha : a ≠ 0) : IsRelPrime a b ↔ ∀ ⦃d⦄, d ∣ a → d ∣ b → ¬Prime d := - ⟨fun h _ ha hb ↦ (·.not_unit <| h ha hb), fun h ↦ WfDvdMonoid.isRelPrime_of_no_irreducible_factors - (ha ·.1) fun _ irr ha hb ↦ h ha hb (UniqueFactorizationMonoid.irreducible_iff_prime.mp irr)⟩ + ⟨fun h _ ha hb ↦ (·.not_isUnit <| h ha hb), + fun h ↦ WfDvdMonoid.isRelPrime_of_no_irreducible_factors + (ha ·.1) fun _ irr ha hb ↦ h ha hb (UniqueFactorizationMonoid.irreducible_iff_prime.mp irr)⟩ /-- Euclid's lemma: if `a ∣ b * c` and `a` and `c` have no common prime factors, `a ∣ b`. Compare `IsCoprime.dvd_of_dvd_mul_left`. -/ diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean b/Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean index 38d0e574bf..96559aad31 100644 --- a/Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean +++ b/Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean @@ -153,7 +153,7 @@ theorem exists_prime_factors (a : α) : lemma exists_prime_iff : (∃ (p : α), Prime p) ↔ ∃ (x : α), x ≠ 0 ∧ ¬ IsUnit x := by - refine ⟨fun ⟨p, hp⟩ ↦ ⟨p, hp.ne_zero, hp.not_unit⟩, fun ⟨x, hx₀, hxu⟩ ↦ ?_⟩ + refine ⟨fun ⟨p, hp⟩ ↦ ⟨p, hp.ne_zero, hp.not_isUnit⟩, fun ⟨x, hx₀, hxu⟩ ↦ ?_⟩ obtain ⟨f, hf, -⟩ := WfDvdMonoid.exists_irreducible_factor hxu hx₀ exact ⟨f, UniqueFactorizationMonoid.irreducible_iff_prime.mp hf⟩ diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean b/Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean index 813990ae38..ea862e1026 100644 --- a/Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean +++ b/Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean @@ -412,7 +412,7 @@ theorem coprime_iff_inf_one {a b : α} (ha0 : a ≠ 0) (hb0 : b ≠ 0) : Associates.mk a ⊓ Associates.mk b = 1 ↔ ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d := by constructor · intro hg p ha hb hp - refine (Associates.prime_mk.mpr hp).not_unit (isUnit_of_dvd_one ?_) + refine (Associates.prime_mk.mpr hp).not_isUnit (isUnit_of_dvd_one ?_) rw [← hg] exact le_inf (mk_le_mk_of_dvd ha) (mk_le_mk_of_dvd hb) · contrapose diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean b/Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean index 00bd185a99..9b279f43be 100644 --- a/Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean +++ b/Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean @@ -48,7 +48,7 @@ theorem FiniteMultiplicity.of_not_isUnit [CommMonoidWithZero α] [IsCancelMulZer theorem FiniteMultiplicity.of_prime_left [CommMonoidWithZero α] [IsCancelMulZero α] [WfDvdMonoid α] {a b : α} (ha : Prime a) (hb : b ≠ 0) : FiniteMultiplicity a b := - .of_not_isUnit ha.not_unit hb + .of_not_isUnit ha.not_isUnit hb namespace UniqueFactorizationMonoid diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean b/Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean index fda34bb2a0..13ba0a3bee 100644 --- a/Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean +++ b/Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean @@ -252,7 +252,7 @@ theorem disjoint_normalizedFactors {a b : α} (hc : IsRelPrime a b) : intro x hxa hxb have x_dvd_a := dvd_of_mem_normalizedFactors hxa have x_dvd_b := dvd_of_mem_normalizedFactors hxb - exact (prime_of_normalized_factor x hxa).not_unit (hc x_dvd_a x_dvd_b) + exact (prime_of_normalized_factor x hxa).not_isUnit (hc x_dvd_a x_dvd_b) theorem exists_associated_prime_pow_of_unique_normalized_factor {p r : α} (h : ∀ {m}, m ∈ normalizedFactors r → m = p) (hr : r ≠ 0) : ∃ i : ℕ, Associated (p ^ i) r := by @@ -283,7 +283,7 @@ theorem normalizedFactors_pos (x : α) (hx : x ≠ 0) : 0 < normalizedFactors x · intro h hx obtain ⟨p, hp⟩ := Multiset.exists_mem_of_ne_zero h.ne' exact - (prime_of_normalized_factor _ hp).not_unit + (prime_of_normalized_factor _ hp).not_isUnit (isUnit_of_dvd_unit (dvd_of_mem_normalizedFactors hp) hx) · intro h obtain ⟨p, hp⟩ := exists_mem_normalizedFactors hx h diff --git a/Mathlib/RingTheory/Unramified/LocalStructure.lean b/Mathlib/RingTheory/Unramified/LocalStructure.lean index 65e65f19a0..3aa963a14f 100644 --- a/Mathlib/RingTheory/Unramified/LocalStructure.lean +++ b/Mathlib/RingTheory/Unramified/LocalStructure.lean @@ -196,7 +196,7 @@ private lemma exists_hasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_ ring · rw [dvd_add_left (dvd_mul_of_dvd_right (dvd_pow (by simp [m, minpoly.dvd_iff]) (by simp)) _), ← isUnit_iff_dvd_one] - exact hm.not_unit + exact hm.not_isUnit have hm' : derivative m ≠ 0 := (separable_iff_derivative_ne_zero hm.irreducible).mp (IsSeparable.isSeparable ..) suffices ¬m ∣ derivative (q.map (algebraMap R _)) by diff --git a/Mathlib/RingTheory/Valuation/PrimeMultiplicity.lean b/Mathlib/RingTheory/Valuation/PrimeMultiplicity.lean index 24b07c6462..7c4c875b72 100644 --- a/Mathlib/RingTheory/Valuation/PrimeMultiplicity.lean +++ b/Mathlib/RingTheory/Valuation/PrimeMultiplicity.lean @@ -18,8 +18,9 @@ variable {R : Type*} [CommRing R] [IsDomain R] {p : R} /-- `multiplicity` of a prime in an integral domain as an additive valuation to `ℕ∞`. -/ noncomputable def multiplicity_addValuation (hp : Prime p) : AddValuation R ℕ∞ := - AddValuation.of (emultiplicity p) (emultiplicity_zero _) (emultiplicity_of_one_right hp.not_unit) - (fun _ _ => min_le_emultiplicity_add) fun _ _ => emultiplicity_mul hp + AddValuation.of (emultiplicity p) (emultiplicity_zero _) + (emultiplicity_of_one_right hp.not_isUnit) + (fun _ _ => min_le_emultiplicity_add) fun _ _ => emultiplicity_mul hp @[simp] theorem multiplicity_addValuation_apply {hp : Prime p} {r : R} : From 533312790e4cb6b1a2b6e999cd48e52d7184bfb6 Mon Sep 17 00:00:00 2001 From: Noah Walker <30136151+NoahW314@users.noreply.github.com> Date: Mon, 3 Aug 2026 08:56:03 +0000 Subject: [PATCH 04/16] chore: rename a lemma containing `not_unit` (#42387) Co-authored-by: NoahW314 --- Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean | 2 +- Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean b/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean index f4c1f0e4f5..dc8da4b559 100644 --- a/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean +++ b/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean @@ -56,7 +56,7 @@ theorem exists_maximalIdeal_pow_eq_of_principal [IsNoetherianRing R] [IsLocalRin have hx' := IsDiscreteValuationRing.irreducible_of_span_eq_maximalIdeal x this hx have H' : ∀ r : R, r ≠ 0 → r ∈ nonunits R → ∃ n : ℕ, Associated (x ^ n) r := by intro r hr₁ hr₂ - obtain ⟨f, hf₁, rfl, hf₂⟩ := (WfDvdMonoid.not_unit_iff_exists_factors_eq r hr₁).mp hr₂ + obtain ⟨f, hf₁, rfl, hf₂⟩ := (WfDvdMonoid.not_isUnit_iff_exists_factors_eq r hr₁).mp hr₂ have : ∀ b ∈ f, Associated x b := by intro b hb exact Irreducible.associated_of_dvd hx' (hf₁ b hb) ((H b).mp (hf₁ b hb).1) diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean b/Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean index 96559aad31..1b734daf56 100644 --- a/Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean +++ b/Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean @@ -84,7 +84,7 @@ theorem exists_factors (a : α) : rw [s.prod_cons i] exact hs.2.mul_left i⟩ -theorem not_unit_iff_exists_factors_eq (a : α) (hn0 : a ≠ 0) : +theorem not_isUnit_iff_exists_factors_eq (a : α) (hn0 : a ≠ 0) : ¬IsUnit a ↔ ∃ f : Multiset α, (∀ b ∈ f, Irreducible b) ∧ f.prod = a ∧ f ≠ ∅ := ⟨fun hnu => by obtain ⟨f, hi, u, rfl⟩ := exists_factors a hn0 @@ -98,6 +98,9 @@ theorem not_unit_iff_exists_factors_eq (a : α) (hn0 : a ≠ 0) : let ⟨b, h⟩ := Multiset.exists_mem_of_ne_zero hne not_isUnit_of_not_isUnit_dvd (hi b h).not_isUnit <| he ▸ Multiset.dvd_prod h⟩ +@[deprecated (since := "2026-08-02")] +alias not_unit_iff_exists_factors_eq := not_isUnit_iff_exists_factors_eq + theorem isRelPrime_of_no_irreducible_factors {x y : α} (nonzero : ¬(x = 0 ∧ y = 0)) (H : ∀ z : α, Irreducible z → z ∣ x → ¬z ∣ y) : IsRelPrime x y := isRelPrime_of_no_nonunits_factors nonzero fun _z znu znz zx zy ↦ From d586c71e87ddf1c4fef06a739cdd3b733fd8b64d Mon Sep 17 00:00:00 2001 From: Noah Walker <30136151+NoahW314@users.noreply.github.com> Date: Mon, 3 Aug 2026 08:56:05 +0000 Subject: [PATCH 05/16] chore: rename `IsPrimePow.not_unit` to `IsPrimePow.not_isUnit` (#42389) Co-authored-by: NoahW314 --- Mathlib/Algebra/IsPrimePow.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/IsPrimePow.lean b/Mathlib/Algebra/IsPrimePow.lean index 54089849dd..25d76180c6 100644 --- a/Mathlib/Algebra/IsPrimePow.lean +++ b/Mathlib/Algebra/IsPrimePow.lean @@ -43,11 +43,14 @@ theorem not_isPrimePow_zero [NoZeroDivisors R] : ¬IsPrimePow (0 : R) := by rw [eq_zero_of_pow_eq_zero hx] simp -theorem IsPrimePow.not_unit {n : R} (h : IsPrimePow n) : ¬IsUnit n := +theorem IsPrimePow.not_isUnit {n : R} (h : IsPrimePow n) : ¬IsUnit n := let ⟨_p, _k, hp, hk, hn⟩ := h hn ▸ (isUnit_pow_iff hk.ne').not.mpr hp.not_isUnit -theorem IsUnit.not_isPrimePow {n : R} (h : IsUnit n) : ¬IsPrimePow n := fun h' => h'.not_unit h +@[deprecated (since := "2026-08-02")] +alias IsPrimePow.not_unit := IsPrimePow.not_isUnit + +theorem IsUnit.not_isPrimePow {n : R} (h : IsUnit n) : ¬IsPrimePow n := fun h' => h'.not_isUnit h theorem not_isPrimePow_one : ¬IsPrimePow (1 : R) := isUnit_one.not_isPrimePow From 49c3708b8696eca37c065f6f9612d48fb53d19fd Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com> Date: Mon, 3 Aug 2026 10:53:42 +0000 Subject: [PATCH 06/16] chore: remove unused `have`/`let` (#42395) This PR removes some unused `have`/`let` that have been caught using the `unusedHavesSuffices` linter from batteries. Unfortunately, the linter has quite a few false positives as well. See also https://github.com/leanprover-community/batteries/pull/1932 --- Mathlib/AlgebraicGeometry/Modules/Sheaf.lean | 3 --- Mathlib/CategoryTheory/Limits/Types/Products.lean | 1 - Mathlib/CategoryTheory/Sites/CoproductSheafCondition.lean | 3 --- Mathlib/CategoryTheory/Sites/LeftExact.lean | 1 - Mathlib/Data/Fin/VecNotation.lean | 1 - Mathlib/LinearAlgebra/FreeModule/ModN.lean | 1 - Mathlib/Tactic/Ring/Common.lean | 1 - 7 files changed, 11 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Modules/Sheaf.lean b/Mathlib/AlgebraicGeometry/Modules/Sheaf.lean index 3f59592d59..c1a0de32bf 100644 --- a/Mathlib/AlgebraicGeometry/Modules/Sheaf.lean +++ b/Mathlib/AlgebraicGeometry/Modules/Sheaf.lean @@ -476,9 +476,6 @@ set_option backward.isDefEq.respectTransparency.types false in set_option backward.defeqAttrib.useBackward true in /-- Restriction along the composition is isomorphic to the composition of restrictions. -/ def restrictFunctorComp : restrictFunctor (f ≫ g) ≅ restrictFunctor g ⋙ restrictFunctor f := - have : (f.opensFunctor ⋙ g.opensFunctor).IsContinuous - (Opens.grothendieckTopology X) (Opens.grothendieckTopology Z) := - Functor.isContinuous_comp _ _ _ (Opens.grothendieckTopology _) _ SheafOfModules.pushforwardNatIso _ (NatIso.ofComponents fun _ ↦ eqToIso (by simp)) ≪≫ SheafOfModules.pushforwardCongr (by ext : 3; simp [← Functor.map_comp, SheafedSpace.sheaf]) ≪≫ (SheafOfModules.pushforwardComp _ _).symm diff --git a/Mathlib/CategoryTheory/Limits/Types/Products.lean b/Mathlib/CategoryTheory/Limits/Types/Products.lean index 812c639881..426d1d10ba 100644 --- a/Mathlib/CategoryTheory/Limits/Types/Products.lean +++ b/Mathlib/CategoryTheory/Limits/Types/Products.lean @@ -229,7 +229,6 @@ noncomputable def productLimitCone : π := Discrete.natTrans (fun ⟨j⟩ => ↾fun f => (equivShrink (∀ j, F j)).symm f j) } isLimit := - have : Small.{u} (∀ j, F j) := inferInstance { lift := fun s => ↾fun x => (equivShrink _) (fun j => s.π.app ⟨j⟩ x) uniq := fun s m w => ConcreteCategory.hom_ext _ _ fun x => Shrink.ext (funext fun j => by simpa using! ConcreteCategory.congr_hom (w ⟨j⟩) x) } diff --git a/Mathlib/CategoryTheory/Sites/CoproductSheafCondition.lean b/Mathlib/CategoryTheory/Sites/CoproductSheafCondition.lean index 7c09039b9d..b8c38dff4b 100644 --- a/Mathlib/CategoryTheory/Sites/CoproductSheafCondition.lean +++ b/Mathlib/CategoryTheory/Sites/CoproductSheafCondition.lean @@ -45,9 +45,6 @@ def PreZeroHypercover.isLimitSigmaOfIsColimitEquiv (E : PreZeroHypercover.{w} S) [PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F] : IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃ IsLimit (E.toPreOneHypercover.multifork F) := by - have : HasPullback (Cofan.IsColimit.desc hc E.f) (Cofan.IsColimit.desc hc E.f) := - inferInstanceAs <| HasPullback - ((E.sigmaOfIsColimit hc).f ⟨⟩) ((E.sigmaOfIsColimit hc).f ⟨⟩) let c' : Cofan E.toPreOneHypercover.Y' := Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y (i₁ := ⟨⟩) (i₂ := ⟨⟩) ⟨⟩) diff --git a/Mathlib/CategoryTheory/Sites/LeftExact.lean b/Mathlib/CategoryTheory/Sites/LeftExact.lean index 6b60331028..67dc248a00 100644 --- a/Mathlib/CategoryTheory/Sites/LeftExact.lean +++ b/Mathlib/CategoryTheory/Sites/LeftExact.lean @@ -135,7 +135,6 @@ def liftToPlusObjLimitObj {K : Type s} [SmallCategory K] [FinCategory K] [ReflectsLimitsOfShape K (forget D)] (F : K ⥤ Cᵒᵖ ⥤ D) (X : C) (S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))) : S.pt ⟶ (J.plusObj (limit F)).obj (op X) := - let x := (J.Cover X)ᵒᵖ let F' := F ⋙ J.diagramFunctor D X let e := colimitLimitIso (F ⋙ J.diagramFunctor D X) let t : J.diagram (limit F) X ≅ limit (F ⋙ J.diagramFunctor D X) := diff --git a/Mathlib/Data/Fin/VecNotation.lean b/Mathlib/Data/Fin/VecNotation.lean index eb4325f5b3..d1173584d1 100644 --- a/Mathlib/Data/Fin/VecNotation.lean +++ b/Mathlib/Data/Fin/VecNotation.lean @@ -197,7 +197,6 @@ dsimproc cons_val (Matrix.vecCons _ _ _) := fun e => do if let Expr.lit (.natVal length) := etailn_whnf then pure (length, false, q(OfNat.ofNat $etailn_whnf)) else if let some ((base : Q(ℕ)), offset) ← (Meta.isOffset? etailn_whnf).run then - let offset_e : Q(ℕ) := mkNatLit offset pure (offset, true, q($base + $offset)) else pure (0, true, etailn) diff --git a/Mathlib/LinearAlgebra/FreeModule/ModN.lean b/Mathlib/LinearAlgebra/FreeModule/ModN.lean index 7efba9a166..5328a0db8f 100644 --- a/Mathlib/LinearAlgebra/FreeModule/ModN.lean +++ b/Mathlib/LinearAlgebra/FreeModule/ModN.lean @@ -63,7 +63,6 @@ set_option backward.isDefEq.respectTransparency false in /-- Given a free module `G` over `ℤ`, construct the corresponding basis of `G / ⟨n⟩` over `ℤ / nℤ`. -/ noncomputable def basis {ι : Type*} (b : Basis ι ℤ G) : Basis ι (ZMod n) (ModN G n) := by - set ψ : G →+ G := zsmulAddGroupHom n set nG := LinearMap.range (LinearMap.lsmul ℤ G n) set H := G ⧸ nG set φ : G →ₗ[ℤ] H := nG.mkQ diff --git a/Mathlib/Tactic/Ring/Common.lean b/Mathlib/Tactic/Ring/Common.lean index 1e801aaa61..59b90ac16b 100644 --- a/Mathlib/Tactic/Ring/Common.lean +++ b/Mathlib/Tactic/Ring/Common.lean @@ -481,7 +481,6 @@ section /-- Get the leading coefficient of an `ExProd`. -/ def ExProd.coeff {e : Q($α)} : - have : Inhabited <| Σ c, bt c := ⟨default, default⟩ ExProd bt sα e → Σ c, bt c | .const q => ⟨_, q⟩ | .mul _ _ v => v.coeff From e76b996718f27fb278e4f046c7e94537e033fb92 Mon Sep 17 00:00:00 2001 From: Akhil Mathew <269628265+j2d9w5xtjn-png@users.noreply.github.com> Date: Mon, 3 Aug 2026 11:34:52 +0000 Subject: [PATCH 07/16] feat(Counterexamples): a finite free group scheme of order four not killed by four (#41748) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds a `Counterexamples/` file resolving a question of Grothendieck in the negative. ## Statement Grothendieck asked whether a finite locally free group scheme of order `n` is killed by `n`. Deligne proved this holds for **commutative** group schemes. This file gives a counterexample in the non-commutative case. Over the base ring `R = ℤ[a, b] / (a³, b³, a²b + 2)`, the coordinate algebra A = R[U, V] / (U² − abU + b²V, V² − a²V) is a Hopf algebra, finite free of rank four over `R`, whose associated affine group scheme has order four but is **not killed by four**. Concretely, the fourth convolution power of the identity is not the convolution unit: `Counterexample.GrothendieckPower.counterexample : Nontrivial R ∧ Module.Free R A ∧ Module.Finite R A ∧ Module.finrank R A = 4 ∧ powerMap 4 ≠ (Algebra.ofId R A).comp counit` ## Disclosure As stated in the module docstring, and per mathlib policy: the construction of this group scheme and its formalization were carried out with the AI assistants Codex (OpenAI) and Claude (Anthropic), under the direction of the author, who takes responsibility for the contribution. Co-authored-by: Yaël Dillies Co-authored-by: Kevin Buzzard --- Counterexamples.lean | 1 + Counterexamples/GrothendieckPower.lean | 1000 +++++++++++++++++++ Mathlib/Algebra/QuadraticAlgebra/Basic.lean | 4 + docs/references.bib | 19 + 4 files changed, 1024 insertions(+) create mode 100644 Counterexamples/GrothendieckPower.lean diff --git a/Counterexamples.lean b/Counterexamples.lean index 80c2aea1ae..9534f98b13 100644 --- a/Counterexamples.lean +++ b/Counterexamples.lean @@ -10,6 +10,7 @@ public import Counterexamples.DirectSumIsInternal public import Counterexamples.DiscreteTopologyNonDiscreteUniformity public import Counterexamples.EulerSumOfPowers public import Counterexamples.Girard +public import Counterexamples.GrothendieckPower public import Counterexamples.HeawoodUnitDistance public import Counterexamples.HomogeneousPrimeNotPrime public import Counterexamples.InvertibleModuleNotIdeal diff --git a/Counterexamples/GrothendieckPower.lean b/Counterexamples/GrothendieckPower.lean new file mode 100644 index 0000000000..d407bdbdb9 --- /dev/null +++ b/Counterexamples/GrothendieckPower.lean @@ -0,0 +1,1000 @@ +/- +Copyright (c) 2026 Akhil Mathew. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Akhil Mathew +-/ +module + +public import Mathlib.Algebra.Category.CommHopfAlgCat +public import Mathlib.Algebra.QuadraticAlgebra.Basic +public import Mathlib.Algebra.Ring.GeomSum +public import Mathlib.Data.FunLike.Fintype +public import Mathlib.LinearAlgebra.Dimension.Free +public import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition +public import Mathlib.RingTheory.Coalgebra.GroupLike +public import Mathlib.Tactic.LinearCombination +public import Mathlib.Tactic.NormNum.BigOperators + +/-! +# A finite free group scheme of rank four that is not killed by four + +Grothendieck asked whether a finite locally free group scheme of order `n` is killed by `n`; +Deligne proved that this holds for commutative group schemes. This file formalizes a +counterexample in the non-commutative case: an affine group scheme, finite free of rank four +over the base ring `R = ℤ[a, b] / (a³, b³, a²b + 2)`, whose fourth power map is not trivial. +Note that `R` is a finite ring of size `2^9` satisfying `4 = 0` but `2 ≠ 0`. + +The coordinate Hopf algebra of the counterexample is `A = R[U, V] / (U² - abU + b²V, V² - a²V)`, +built as a `QuadraticAlgebra` over the `QuadraticAlgebra` `B := R[V] / (V² - a²V)`. +It is finite free of rank four over `R`. With +`lambda = (1 + aU) * (1 + bV)`, the comultiplication is determined by + +* `Δ(U) = U ⊗ 1 + lambda ⊗ U`, +* `Δ(V) = V ⊗ lambda + 1 ⊗ V`, + +and `lambda` is group-like (that is, `Δ(lambda) = lambda ⊗ lambda`). +The counit sends both `U` and `V` to zero. The `n`th convolution power of +the identity — the coordinate map of the pointwise `n`th power `x ↦ xⁿ` of the +group scheme — sends `U` to `(1 + lambda + ⋯ + lambdaⁿ⁻¹) · U`. For `n = 4` this +is `2bUV ≠ 0`, while the eighth convolution power is the convolution unit +(the composite of the counit with the unit map of `A`) and in particular sends `U` to `0`. +In particular the seventh convolution power supplies an antipode, so `A` is a Hopf +algebra, and the associated group scheme has order four but is not killed by four. + +## Main definitions + +* `Counterexample.GrothendieckPower.R`: the base ring `ℤ[a, b] / (a³, b³, a²b + 2)`. +* `Counterexample.GrothendieckPower.A`: the coordinate algebra, finite free of rank four + over `R`. +* `Counterexample.GrothendieckPower.instHopfAlgebra`: the Hopf algebra structure on `A`. +* `Counterexample.GrothendieckPower.powerMap`: the `n`-th convolution power of the identity + of `A`, i.e. the coordinate map of the pointwise `n`-th power of the group scheme. +* `Counterexample.GrothendieckPower.affineGroupScheme`: the counterexample as a group object + in the opposite of the category of commutative `R`-algebras, through Mathlib's + antiequivalence with commutative Hopf algebras. + +## Main results + +* `Counterexample.GrothendieckPower.finrank_A`: `A` has rank four over `R`. Note that + `A` is also finite and free over `R`, so `A ≅ R⁴` as an `R`-module. +* `Counterexample.GrothendieckPower.powerMap_four_U_ne_zero`: the fourth power map is not + the convolution unit, since it sends `U` to `2bUV ≠ 0`. +* `Counterexample.GrothendieckPower.powerMap_eight`: the eighth power map is the convolution + unit. +* `Counterexample.GrothendieckPower.counterexample`: the combined statement: over the + nontrivial ring `R`, the algebra `A` is finite free of rank four and its fourth power map + is not the convolution unit. +* `Counterexample.GrothendieckPower.exists_hopfAlgebra_not_killed_by_finrank`: the negative + answer to Grothendieck's question, spelled out as an existence statement: there is a + nontrivial commutative ring and a commutative Hopf algebra, free of finite rank over it, + whose convolution power map at the exponent equal to its rank is not the convolution unit. +* `Counterexample.GrothendieckPower.orderOf_universalPoint`: the universal `A`-valued point + of the group scheme has order exactly eight. +* `Counterexample.GrothendieckPower.not_isCocomm`: `A` is not cocommutative, i.e. the group + scheme is noncommutative, as forced by Deligne's theorem for commutative group schemes. +* `Counterexample.GrothendieckPower.id_pow_affineGroupScheme_four_ne_one`: the group-scheme + formulation, through Mathlib's antiequivalence between commutative Hopf algebras and + affine group schemes: on the corresponding group object in `(CommAlgCat R)ᵒᵖ`, the + pointwise fourth power map — the fourth power `𝟙 _ ^ 4` of the identity in the convolution + monoid of endomorphisms — is not the constant-unit endomorphism. + +## Implementation notes + +Nontriviality of the base ring (concretely, `2b ≠ 0` in `R`) is certified by an explicit +model: the regular representation of `R` on `M = ℤ/4 × ℤ/4 × (ℤ/2)⁵`, with the actions of +`a` and `b` given by explicit additive endomorphisms and all relations checked +by `decide +kernel`. + +The polynomial identities underlying the comultiplication and the power-map computations are +proved once in an arbitrary commutative ring satisfying the relations of `R` +(`law_relations_generic`, `law_lambda_generic`, `theta_identities_generic`) using +`linear_combination`, and then transported along algebra maps. + +The generators are given short names in each successive algebra (`aB`, `bB`, `aA`, `bA`) and +in the tensor square (`a₁`, `b₁`, `u₁`, `v₁`, `u₂`, `v₂`, `l₁`, `l₂`). These are `abbrev`s, +so that they unfold definitionally; their only purpose is to keep the statements of the +polynomial certificates and of the coproduct construction readable. + +The construction of this group scheme as well as its formalization were carried out by the +AI assistants Codex (OpenAI) and Claude (Anthropic). + +## References + +* [F. Oort, J. Tate, *Group schemes of prime order*][oorttate1970]: Deligne's proof that a + commutative finite locally free group scheme is killed by its order is reproduced in §1, + and the question for possibly non-commutative group schemes is raised on p. 5. +* [J. Tate, *Finite flat group schemes*][tate1997]: records the question as open in §3.8. + +## Tags + +group scheme, Hopf algebra, counterexample +-/ + +@[expose] public section + +namespace Counterexample.GrothendieckPower + +private theorem quadratic_lift_omega {C S : Type*} [CommSemiring C] [Ring S] + {c l : C} [Algebra C S] (x : S) (hx : x * x = c • 1 + l • x) : + QuadraticAlgebra.lift (R := C) ⟨x, hx⟩ QuadraticAlgebra.omega = x := + congr_arg Subtype.val + (QuadraticAlgebra.lift.symm_apply_apply ⟨x, hx⟩) + +/-! +### An explicit faithful model of the base ring + +The base ring `R = ℤ[a, b] / (a³, b³, a²b + 2)` is nontrivial, but this is not syntactically +obvious from its presentation. We certify it by exhibiting an explicit `R`-module: the +regular representation of `R` on `ℤ/4 × ℤ/4 × (ℤ/2)⁵`, with `a` and `b` acting through +explicit commuting additive endomorphisms. All required relations are closed by `decide +kernel`. +-/ + +/-- Reduction modulo `2`, as a ring homomorphism `ℤ/4 → ℤ/2`. -/ +def reduce : ZMod 4 →+* ZMod 2 := ZMod.castHom (by norm_num : 2 ∣ 4) _ + +/-- The additive map `ℤ/2 → ℤ/4` sending `1` to `2`. -/ +def double : ZMod 2 →+ ZMod 4 := ZMod.lift 2 ⟨2 • Int.castAddHom (ZMod 4), by decide⟩ + +@[simp] theorem reduce_double (x : ZMod 2) : reduce (double x) = 0 := by + fin_cases x <;> decide + +@[simp] theorem double_reduce (x : ZMod 4) : double (reduce x) = 2 * x := by + fin_cases x <;> decide + +/-- The additive group `ℤ/4 × ℤ/4 × (ℤ/2)⁵`, carrier of the regular representation of the +base ring `R := ℤ[a, b] / (a³, b³, a²b + 2)` (and in particular isomorphic to `R` +as an additive group). -/ +abbrev M := ZMod 4 × ZMod 4 × (Fin 5 → ZMod 2) + +/-- The additive endomorphism of `M` realizing multiplication by the generator `a` (the class +of the first variable) of the base ring `R = ℤ[a, b] / (a³, b³, a²b + 2)`, in its regular +representation. -/ +def aEnd : AddMonoid.End M where + toFun x := + (double (x.2.2 2), double (x.2.2 4), + ![reduce x.1, x.2.2 0, reduce x.2.1, 0, x.2.2 3]) + map_zero' := by simp + map_add' x y := by simp + +/-- The additive endomorphism of `M` realizing multiplication by the generator `b` (the class +of the second variable) of the base ring `R = ℤ[a, b] / (a³, b³, a²b + 2)`, in its regular +representation. -/ +def bEnd : AddMonoid.End M where + toFun x := + (double (x.2.2 1), x.1, + ![0, 0, x.2.2 0, reduce x.2.1, x.2.2 2]) + map_zero' := by simp + map_add' x y := by simp + +theorem aEnd_bEnd_comm : aEnd * bEnd = bEnd * aEnd := by decide +kernel + +theorem aEnd_cube : aEnd ^ 3 = 0 := by decide +kernel + +theorem bEnd_cube : bEnd ^ 3 = 0 := by decide +kernel + +theorem aEnd_sq_mul_bEnd : aEnd ^ 2 * bEnd + 2 = 0 := by decide +kernel + +theorem two_mul_bEnd_ne_zero : 2 * bEnd ≠ 0 := by decide +kernel + +private theorem generators_commute {x y : AddMonoid.End M} + (hx : x ∈ ({aEnd, bEnd} : Set (AddMonoid.End M))) + (hy : y ∈ ({aEnd, bEnd} : Set (AddMonoid.End M))) : x * y = y * x := by + simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hx hy + rcases hx with rfl | rfl <;> rcases hy with rfl | rfl <;> simp [aEnd_bEnd_comm] + +/-- The commutative subring of `AddMonoid.End M` generated by `aEnd` and `bEnd`. -/ +def WitnessRing := Subring.closure ({aEnd, bEnd} : Set (AddMonoid.End M)) + +open scoped IsMulCommutative + +instance : IsMulCommutative WitnessRing := + Subring.isMulCommutative_closure fun _ hx _ hy ↦ generators_commute hx hy + +/-- The element `aEnd`, as an element of `WitnessRing`. -/ +def aw : WitnessRing := ⟨aEnd, Subring.subset_closure (Set.mem_insert _ _)⟩ + +/-- The element `bEnd`, as an element of `WitnessRing`. -/ +def bw : WitnessRing := + ⟨bEnd, Subring.subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))⟩ + +@[simp] theorem aw_cube : aw ^ 3 = 0 := Subtype.ext aEnd_cube + +@[simp] theorem bw_cube : bw ^ 3 = 0 := Subtype.ext bEnd_cube + +@[simp] theorem witness_relation : aw ^ 2 * bw + 2 = 0 := + Subtype.ext aEnd_sq_mul_bEnd + +theorem two_bw_ne_zero : (2 : WitnessRing) * bw ≠ 0 := fun h ↦ + two_mul_bEnd_ne_zero (congr_arg Subtype.val h) + +instance : Nontrivial WitnessRing := ⟨⟨(2 : WitnessRing) * bw, 0, two_bw_ne_zero⟩⟩ + +/-! +### The base ring `R = ℤ[a, b] / (a³, b³, a²b + 2)` +-/ + +noncomputable section + +open MvPolynomial + +/-- The polynomial ring `ℤ[a, b]`. -/ +abbrev P := MvPolynomial (Fin 2) ℤ + +/-- The polynomial variable `a`. -/ +abbrev ap : P := X 0 + +/-- The polynomial variable `b`. -/ +abbrev bp : P := X 1 + +/-- The ideal `(a³, b³, a²b + 2)` of `ℤ[a, b]`. -/ +def baseIdeal : Ideal P := + Ideal.span ({ap ^ 3, bp ^ 3, ap ^ 2 * bp + C 2} : Set P) + +/-- The base ring `R = ℤ[a, b] / (a³, b³, a²b + 2)`. -/ +abbrev R := P ⧸ baseIdeal + +/-- The class of the variable `a` in the base ring `R`. -/ +def a : R := Ideal.Quotient.mk baseIdeal ap + +/-- The class of the variable `b` in the base ring `R`. -/ +def b : R := Ideal.Quotient.mk baseIdeal bp + +@[simp] theorem a_cube : a ^ 3 = 0 := + Ideal.Quotient.eq_zero_iff_mem.2 <| Ideal.subset_span (by simp) + +@[simp] theorem b_cube : b ^ 3 = 0 := + Ideal.Quotient.eq_zero_iff_mem.2 <| Ideal.subset_span (by simp) + +@[simp] theorem base_relation : a ^ 2 * b + 2 = 0 := + Ideal.Quotient.eq_zero_iff_mem.2 <| Ideal.subset_span (by simp) + +/-- Evaluation of integer polynomials at `(aw, bw)` in `WitnessRing`. -/ +def evalWitness : P →+* WitnessRing := + eval₂Hom (Int.castRingHom WitnessRing) ![aw, bw] + +theorem baseIdeal_le_ker_evalWitness : baseIdeal ≤ RingHom.ker evalWitness := by + rw [baseIdeal, Ideal.span_le] + intro p hp + simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hp + rcases hp with rfl | rfl | rfl <;> simp [evalWitness, ap, bp] + +/-- The ring map `R → WitnessRing`, giving an action of `R` on `M`. -/ +def witnessHom : R →+* WitnessRing := + Ideal.Quotient.lift baseIdeal evalWitness baseIdeal_le_ker_evalWitness + +@[simp] theorem witnessHom_b : witnessHom b = bw := by + simp [witnessHom, b, evalWitness, bp] + +theorem two_b_ne_zero : (2 : R) * b ≠ 0 := by + intro h + apply two_bw_ne_zero + simpa [map_ofNat] using congr_arg witnessHom h + +instance : Nontrivial R := ⟨⟨(2 : R) * b, 0, two_b_ne_zero⟩⟩ + +/-! +### The coordinate algebra `A = R[U, V] / (U² - abU + b²V, V² - a²V)` + +The algebra `A` is realized as two nested `QuadraticAlgebra`s, so that its finite freeness of +rank four over `R` follows from the corresponding facts for each step of the tower. +-/ + +open scoped QuadraticAlgebra + +/-- The intermediate quadratic algebra `B = R[V] / (V² - a²V)`. -/ +abbrev B := QuadraticAlgebra R 0 (a ^ 2) + +/-- The generator `VB` of `B`, satisfying `VB² = a²·VB`. -/ +abbrev VB : B := ω + +@[simp] theorem VB_relation : VB ^ 2 = algebraMap R B (a ^ 2) * VB := by + simp [pow_two, QuadraticAlgebra.omega_mul_omega_eq_algebraMap] + +/-- The image of `a` in `B`. -/ +abbrev aB : B := algebraMap R B a + +/-- The image of `b` in `B`. -/ +abbrev bB : B := algebraMap R B b + +/-- The coordinate algebra `A = B[U] / (U² - abU + b²V) = R[U, V] / (U² - abU + b²V, V² - a²V)`, +finite free of rank four over the base ring `R`. -/ +abbrev A := QuadraticAlgebra B (-(bB ^ 2) * VB) (aB * bB) + +/-- The generator `U` of `A`, satisfying `U² = abU - b²V`. -/ +abbrev U : A := ω + +/-- The image `V` of `VB` in `A`. -/ +abbrev V : A := algebraMap B A VB + +/-- The image `aA` of `a` in `A`. -/ +abbrev aA : A := algebraMap R A a + +/-- The image `bA` of `b` in `A`. -/ +abbrev bA : A := algebraMap R A b + +@[simp] theorem U_relation : + U ^ 2 = algebraMap R A (a * b) * U - algebraMap R A (b ^ 2) * V := by + rw [pow_two] + unfold U V + rw [QuadraticAlgebra.omega_mul_omega_eq_mk] + ext <;> simp [VB, aB, bB, pow_two, IsScalarTower.algebraMap_apply R B A] + +@[simp] theorem V_relation : V ^ 2 = algebraMap R A (a ^ 2) * V := by + change (algebraMap B A VB) ^ 2 = algebraMap R A (a ^ 2) * algebraMap B A VB + rw [← map_pow, VB_relation, map_mul, IsScalarTower.algebraMap_apply R B A] + +instance : Module.Free R A := + Module.Free.trans (S := B) + +instance : Module.Finite R A := + Module.Finite.trans B A + +theorem finrank_B : Module.finrank R B = 2 := + QuadraticAlgebra.finrank_eq_two _ _ + +theorem finrank_A_over_B : Module.finrank B A = 2 := + QuadraticAlgebra.finrank_eq_two _ _ + +theorem finrank_A : Module.finrank R A = 4 := by + rw [← Module.finrank_mul_finrank R B A, finrank_B, finrank_A_over_B] + +/-! +### The universal property of `A` + +An `R`-algebra map out of `A = R[U, V] / (U² - abU + b²V, V² - a²V)` amounts to a pair of +elements of the target satisfying the two defining relations. The construction goes through +the tower `R → B → A`: the image of `V` determines an `R`-algebra map out of +`B = R[V] / (V² - a²V)`, which makes the target a `B`-algebra, and the image of `U` then +determines a quadratic lift out of `A`. The `B`-algebra structure depends on the chosen +image of `V`, so it is kept local to the construction and never becomes an instance: the +coproduct below, for example, uses a `B`-algebra structure on `A ⊗[R] A` different from the +canonical one through the left tensor factor. +-/ + +section UniversalProperty + +variable {S : Type*} [CommRing S] [Algebra R S] + +/-- The `R`-algebra map `B →ₐ[R] S` sending `VB` to a root of `X² - a²X`. -/ +def mkAlgHomB (v : S) (hv : v ^ 2 = algebraMap R S (a ^ 2) * v) : + B →ₐ[R] S := + QuadraticAlgebra.lift ⟨v, by rw [zero_smul, zero_add, Algebra.smul_def, ← pow_two, hv]⟩ + +theorem mkAlgHomB_VB (v : S) (hv : v ^ 2 = algebraMap R S (a ^ 2) * v) : + mkAlgHomB v hv VB = v := + quadratic_lift_omega v _ + +/-- If `S` is an arbitrary `R`-algebra, then to give an `R`-algebra map `A →ₐ[R] S` +it suffices to give a pair of elements `u` and `v` in `S` satisfying the +equations `v²=a²v` and `u²=abu-b²v`. -/ +def mkAlgHom (u v : S) (hv : v ^ 2 = algebraMap R S (a ^ 2) * v) + (hu : u ^ 2 = algebraMap R S (a * b) * u - algebraMap R S (b ^ 2) * v) : + A →ₐ[R] S := + let : Algebra B S := (mkAlgHomB v hv).toRingHom.toAlgebra + have : IsScalarTower R B S := + .of_algebraMap_eq fun r ↦ ((mkAlgHomB v hv).commutes r).symm + AlgHom.restrictScalars R (QuadraticAlgebra.lift + ⟨u, show u * u = mkAlgHomB v hv (-(bB ^ 2) * VB) * 1 + mkAlgHomB v hv (aB * bB) * u by + rw [mul_one, map_mul, map_mul, map_neg, map_pow, mkAlgHomB_VB, + (mkAlgHomB v hv).commutes, (mkAlgHomB v hv).commutes] + linear_combination hu + u * map_mul (algebraMap R S) a b - + v * map_pow (algebraMap R S) b 2⟩ : A →ₐ[B] S) + +theorem mkAlgHom_U {u v : S} (hv : v ^ 2 = algebraMap R S (a ^ 2) * v) + (hu : u ^ 2 = algebraMap R S (a * b) * u - algebraMap R S (b ^ 2) * v) : + mkAlgHom u v hv hu U = u := by + let : Algebra B S := (mkAlgHomB v hv).toRingHom.toAlgebra + exact quadratic_lift_omega u _ + +theorem mkAlgHom_V {u v : S} (hv : v ^ 2 = algebraMap R S (a ^ 2) * v) + (hu : u ^ 2 = algebraMap R S (a * b) * u - algebraMap R S (b ^ 2) * v) : + mkAlgHom u v hv hu V = v := by + let : Algebra B S := (mkAlgHomB v hv).toRingHom.toAlgebra + exact ((QuadraticAlgebra.lift _ : A →ₐ[B] S).commutes VB).trans (mkAlgHomB_VB v hv) + +end UniversalProperty + +/-! +### The comultiplication + +The polynomial identities behind the coproduct are proved once, in an arbitrary commutative +ring whose distinguished elements satisfy the relations of `R`, by `linear_combination` +certificates; they are then transported to the tensor square along the two inclusions. +-/ + +private theorem law_relations_generic {S : Type*} [CommRing S] + {a b u₁ v₁ u₂ v₂ : S} + (ha : a ^ 3 = 0) (hb : b ^ 3 = 0) (hab : a ^ 2 * b + 2 = 0) + (hv₁ : v₁ ^ 2 = a ^ 2 * v₁) (hu₁ : u₁ ^ 2 = a * b * u₁ - b ^ 2 * v₁) + (hv₂ : v₂ ^ 2 = a ^ 2 * v₂) (hu₂ : u₂ ^ 2 = a * b * u₂ - b ^ 2 * v₂) : + let l₁ := (1 + a * u₁) * (1 + b * v₁) + let l₂ := (1 + a * u₂) * (1 + b * v₂) + let dv := v₁ * l₂ + v₂ + let du := u₁ + l₁ * u₂ + dv ^ 2 = a ^ 2 * dv ∧ du ^ 2 = a * b * du - b ^ 2 * dv := by + grind + +private theorem law_lambda_generic {S : Type*} [CommRing S] + {a b u₁ v₁ u₂ v₂ : S} + (ha : a ^ 3 = 0) (hb : b ^ 3 = 0) (hab : a ^ 2 * b + 2 = 0) + (hv₁ : v₁ ^ 2 = a ^ 2 * v₁) + (hv₂ : v₂ ^ 2 = a ^ 2 * v₂) (hu₂ : u₂ ^ 2 = a * b * u₂ - b ^ 2 * v₂) : + letI l₁ := (1 + a * u₁) * (1 + b * v₁) + letI l₂ := (1 + a * u₂) * (1 + b * v₂) + letI dv := v₁ * l₂ + v₂ + letI du := u₁ + l₁ * u₂ + (1 + a * du) * (1 + b * dv) = l₁ * l₂ := by + grind + +/-- The group-like unit `(1+aU)(1+bV)` of `A` controlling the semidirect-product law. -/ +def lambda : A := (1 + aA * U) * (1 + bA * V) + +private theorem mapped_relations {S : Type*} [CommRing S] [Algebra R S] + (f : A →ₐ[R] S) : + letI aa := f aA + letI bb := f bA + letI uu := f U + letI vv := f V + aa ^ 3 = 0 ∧ bb ^ 3 = 0 ∧ aa ^ 2 * bb + 2 = 0 ∧ + vv ^ 2 = aa ^ 2 * vv ∧ uu ^ 2 = aa * bb * uu - bb ^ 2 * vv := by + split_ands + · simp [aA, ← map_pow, a_cube] + · simp [bA, ← map_pow, b_cube] + · rw [← map_ofNat f] + suffices f (aA ^ 2 * bA + 2) = 0 by simpa + suffices aA ^ 2 * bA + 2 = 0 by simp [this] + suffices algebraMap R A (a ^ 2 * b + 2) = 0 by simpa [aA, bA, -base_relation] + simp + · rw [← map_pow, V_relation, map_mul] + simp [aA, ← map_pow] + · have h : U ^ 2 = aA * bA * U - bA ^ 2 * V := by + simp [aA, bA, map_pow, map_mul] + simpa only [map_pow, map_sub, map_mul] using congr_arg f h + +open scoped TensorProduct + +/-- The inclusion of the left tensor factor `A → A ⊗[R] A`. -/ +abbrev left : A →ₐ[R] A ⊗[R] A := Algebra.TensorProduct.includeLeft + +/-- The inclusion of the right tensor factor `A → A ⊗[R] A`. -/ +abbrev right : A →ₐ[R] A ⊗[R] A := Algebra.TensorProduct.includeRight + +/-- The image of `a` in `A ⊗[R] A`. -/ +abbrev a₁ : A ⊗[R] A := left aA + +/-- The image of `b` in `A ⊗[R] A`. -/ +abbrev b₁ : A ⊗[R] A := left bA + +private theorem right_aA : right aA = a₁ := by + change (1 : A) ⊗ₜ[R] aA = aA ⊗ₜ[R] (1 : A) + rw [show aA = a • (1 : A) from Algebra.algebraMap_eq_smul_one a] + exact (TensorProduct.tmul_smul a 1 1).trans (TensorProduct.smul_tmul' a 1 1).symm + +private theorem right_bA : right bA = b₁ := by + change (1 : A) ⊗ₜ[R] bA = bA ⊗ₜ[R] (1 : A) + rw [show bA = b • (1 : A) from Algebra.algebraMap_eq_smul_one b] + exact (TensorProduct.tmul_smul b 1 1).trans (TensorProduct.smul_tmul' b 1 1).symm + +/-- The element `U ⊗ₜ 1` in `A ⊗ A`. -/ +abbrev u₁ : A ⊗[R] A := left U + +/-- The element `V ⊗ₜ 1` in `A ⊗ A`. -/ +abbrev v₁ : A ⊗[R] A := left V + +/-- The element `1 ⊗ₜ U` in `A ⊗ A`. -/ +abbrev u₂ : A ⊗[R] A := right U + +/-- The element `1 ⊗ₜ V` in `A ⊗ A`. -/ +abbrev v₂ : A ⊗[R] A := right V + +/-- The element `λ ⊗ₜ 1 = (1+aU)(1+bV) ⊗ₜ 1` in `A ⊗ A`. -/ +abbrev l₁ : A ⊗[R] A := (1 + a₁ * u₁) * (1 + b₁ * v₁) + +/-- The element `1 ⊗ₜ λ = 1 ⊗ₜ (1+aU)(1+bV)` in `A ⊗ A`. -/ +abbrev l₂ : A ⊗[R] A := (1 + a₁ * u₂) * (1 + b₁ * v₂) + +/-- The element `δ_V := V ⊗ₜ λ + 1 ⊗ₜ V` which will be the image of V under the comultiplication +on A. -/ +def deltaV : A ⊗[R] A := v₁ * l₂ + v₂ + +/-- The element `δ_U := U ⊗ₜ 1 + λ ⊗ₜ U` which will be the image of U under the comultiplication +on A. -/ +def deltaU : A ⊗[R] A := u₁ + l₁ * u₂ + +/-- The proof that `δ_V` and `δ_U` satisfy the same relations as `V` and `U`. -/ +private theorem delta_relations : + deltaV ^ 2 = a₁ ^ 2 * deltaV ∧ + deltaU ^ 2 = a₁ * b₁ * deltaU - b₁ ^ 2 * deltaV := by + obtain ⟨ha₁, hb₁, hab₁, hv₁', hu₁'⟩ := mapped_relations (S := A ⊗[R] A) left + obtain ⟨_, _, _, hv₂', hu₂'⟩ := mapped_relations (S := A ⊗[R] A) right + simp only [right_aA, right_bA] at hv₂' hu₂' + exact law_relations_generic ha₁ hb₁ hab₁ hv₁' hu₁' hv₂' hu₂' + +/-- The proof that `δ_λ := (1+aδ_U)(1+bδ_V) = λ ⊗ₜ λ` in `A ⊗ A`. -/ +private theorem delta_lambda : + (1 + a₁ * deltaU) * (1 + b₁ * deltaV) = l₁ * l₂ := by + obtain ⟨ha₁, hb₁, hab₁, hv₁', -⟩ := mapped_relations (S := A ⊗[R] A) left + obtain ⟨-, -, -, hv₂', hu₂'⟩ := mapped_relations (S := A ⊗[R] A) right + simp only [right_aA, right_bA] at hv₂' hu₂' + exact law_lambda_generic ha₁ hb₁ hab₁ hv₁' hv₂' hu₂' + +private theorem a₁_smul : a₁ = a • 1 := by + change (aA ⊗ₜ[R] (1 : A)) = a • 1 + rw [show aA = a • (1 : A) from Algebra.algebraMap_eq_smul_one a] + exact TensorProduct.smul_tmul' a 1 1 + +private theorem b₁_smul : b₁ = b • 1 := by + change (bA ⊗ₜ[R] (1 : A)) = b • 1 + rw [show bA = b • (1 : A) from Algebra.algebraMap_eq_smul_one b] + exact TensorProduct.smul_tmul' b 1 1 + +/-- The coproduct algebra homomorphism, sending `U` to `δ_U` and `V` to `δ_V`. -/ +def comul : A →ₐ[R] A ⊗[R] A := + mkAlgHom deltaU deltaV + (by rw [← left.commutes (a ^ 2), map_pow, map_pow]; exact delta_relations.1) + (by rw [← left.commutes (a * b), ← left.commutes (b ^ 2), map_mul, map_mul, map_pow, + map_pow]; exact delta_relations.2) + +theorem comul_U : comul U = deltaU := mkAlgHom_U _ _ + +theorem comul_V : comul V = deltaV := mkAlgHom_V _ _ + +theorem comul_aA : comul aA = a₁ := by + rw [comul.commutes, Algebra.algebraMap_eq_smul_one, ← a₁_smul] + +theorem comul_bA : comul bA = b₁ := by + rw [comul.commutes, Algebra.algebraMap_eq_smul_one, ← b₁_smul] + +theorem left_lambda : left lambda = l₁ := by + simp only [lambda, map_mul, map_add, map_one] + +theorem right_lambda : right lambda = l₂ := by + simp only [lambda, map_mul, map_add, map_one, right_aA, right_bA] + +@[simp] theorem comul_lambda : comul lambda = left lambda * right lambda := by + rw [left_lambda, right_lambda] + simpa [lambda, map_mul, map_add, comul_aA, comul_bA, comul_U, comul_V] using delta_lambda + +@[simp] theorem comul_U_formula : + comul U = left U + left lambda * right U := by + rw [comul_U, left_lambda] + rfl + +@[simp] theorem comul_V_formula : + comul V = left V * right lambda + right V := by + rw [comul_V, right_lambda] + rfl + +/-- Two `R`-algebra maps out of `A` agree if they agree on `U` and `V`. -/ +theorem algHom_ext {S : Type*} [Semiring S] [Algebra R S] + {f g : A →ₐ[R] S} (hU : f U = g U) (hv : f V = g V) : f = g := by + ext x + have h_embed (z : B) : + algebraMap B A z = algebraMap R A z.re + algebraMap R A z.im * V := by + have hz : z = algebraMap R B z.re + algebraMap R B z.im * VB := by + calc + z = ⟨z.re, z.im⟩ := rfl + _ = algebraMap R B z.re + z.im • VB := + QuadraticAlgebra.mk_eq_add_smul_omega z.re z.im + _ = algebraMap R B z.re + algebraMap R B z.im * VB := by + apply QuadraticAlgebra.ext <;> simp [VB] + calc + algebraMap B A z = algebraMap B A + (algebraMap R B z.re + algebraMap R B z.im * VB) := congr_arg _ hz + _ = algebraMap R A z.re + algebraMap R A z.im * V := by + rw [map_add, map_mul, ← IsScalarTower.algebraMap_apply R B A, + ← IsScalarTower.algebraMap_apply R B A] + have hB (z : B) : f (algebraMap B A z) = g (algebraMap B A z) := by + rw [h_embed] + simp only [map_add, map_mul] + rw [f.commutes, f.commutes, g.commutes, g.commutes, hv] + have hx : x = algebraMap B A x.re + algebraMap B A x.im * U := by + apply QuadraticAlgebra.ext <;> simp [U] + rw [hx, map_add, map_mul, map_add, map_mul, hB x.re, hB x.im, hU] + +/-! +### The counit and the bialgebra structure +-/ + +/-- The counit algebra homomorphism, sending `U` and `V` to zero. -/ +def counit : A →ₐ[R] R := + mkAlgHom 0 0 (by simp) (by simp) + +@[simp] theorem counit_V : counit V = 0 := mkAlgHom_V _ _ + +@[simp] theorem counit_U : counit U = 0 := mkAlgHom_U _ _ + +@[simp] theorem counit_lambda : counit lambda = 1 := by + simp [lambda] + +theorem comul_coassoc : + (Algebra.TensorProduct.assoc R R R A A A).toAlgHom.comp + ((Algebra.TensorProduct.map comul (.id R A)).comp comul) = + (Algebra.TensorProduct.map (.id R A) comul).comp comul := by + apply algHom_ext + · simp [comul_U_formula, comul_lambda, Algebra.TensorProduct.one_def, + TensorProduct.add_tmul, TensorProduct.tmul_add, add_assoc] + · simp [comul_V_formula, comul_lambda, Algebra.TensorProduct.one_def, + TensorProduct.add_tmul, TensorProduct.tmul_add, add_assoc] + +theorem counit_left : + (Algebra.TensorProduct.map counit (.id R A)).comp comul = + (Algebra.TensorProduct.lid R A).symm := by + apply algHom_ext + · simp [counit_lambda] + · simp + +theorem counit_right : + (Algebra.TensorProduct.map (.id R A) counit).comp comul = + (Algebra.TensorProduct.rid R R A).symm := by + apply algHom_ext + · simp + · simp [counit_lambda] + +/-- The bialgebra structure underlying the counterexample. -/ +instance instBialgebra : Bialgebra R A := + Bialgebra.ofAlgHom comul counit comul_coassoc counit_left counit_right + +private theorem bialgebra_comulAlgHom : Bialgebra.comulAlgHom R A = comul := rfl +private theorem bialgebra_counitAlgHom : Bialgebra.counitAlgHom R A = counit := rfl + +/-- The coordinate `lambda` is a group-like element of `A`. -/ +theorem isGroupLikeElem_lambda : IsGroupLikeElem R lambda where + counit_eq_one := by + rw [← Bialgebra.counitAlgHom_apply (R := R), bialgebra_counitAlgHom] + exact counit_lambda + comul_eq_tmul_self := by + rw [← Bialgebra.comulAlgHom_apply (R := R), bialgebra_comulAlgHom, comul_lambda] + simp + +/-! +### The convolution power maps + +The `n`-th power map of the group scheme (pointwise `x ↦ xⁿ`) corresponds, on coordinate +rings, to the `n`th convolution power of the identity of `A`. On the skew-primitive +coordinates it is controlled by the geometric sum +`1 + lambda + ⋯ + lambdaⁿ⁻¹`, which we compute from the square-zero element +`theta = lambda - 1`. +-/ + +/-- The square-zero part of the group-like coordinate. -/ +def theta : A := lambda - 1 + +private theorem theta_identities_generic {S : Type*} [CommRing S] + {aa bb uu vv : S} + (ha : aa ^ 3 = 0) (hb : bb ^ 3 = 0) (hab : aa ^ 2 * bb + 2 = 0) + (hv : vv ^ 2 = aa ^ 2 * vv) + (hu : uu ^ 2 = aa * bb * uu - bb ^ 2 * vv) : + letI th := (1 + aa * uu) * (1 + bb * vv) - 1 + th ^ 2 = 0 ∧ 2 * th = 2 * bb * vv := by + grind + +theorem theta_sq : theta ^ 2 = 0 := by + obtain ⟨ha, hb, hab, hv, hu⟩ := mapped_relations (AlgHom.id R A) + exact (theta_identities_generic ha hb hab hv hu).1 + +theorem two_theta : 2 * theta = 2 * bA * V := by + obtain ⟨ha, hb, hab, hv, hu⟩ := mapped_relations (AlgHom.id R A) + exact (theta_identities_generic ha hb hab hv hu).2 + +open WithConv + +/-- The universal point, in the convolution monoid of `R`-algebra endomorphisms. -/ +def universalPoint : WithConv (A →ₐ[R] A) := + toConv (AlgHom.id R A) + +/-- The `n`th convolution power of the identity of `A`: the coordinate ring map of the +pointwise `n`th power map of the group scheme. -/ +def powerMap (n : ℕ) : A →ₐ[R] A := + (universalPoint ^ n).ofConv + +@[simp] theorem powerMap_zero_apply (x : A) : powerMap 0 x = algebraMap R A (counit x) := by + rfl + +@[simp] theorem powerMap_one_apply (x : A) : powerMap 1 x = x := + congr_arg (fun f : WithConv (A →ₐ[R] A) ↦ f.ofConv x) (pow_one universalPoint) + +theorem powerMap_succ_U (n : ℕ) : + powerMap (n + 1) U = powerMap n U + powerMap n lambda * U := by + change (universalPoint ^ (n + 1)).ofConv U = _ + rw [pow_succ universalPoint n, AlgHom.convMul_apply, ← Bialgebra.comulAlgHom_apply, + bialgebra_comulAlgHom, comul_U_formula] + simp [universalPoint, powerMap] + +theorem powerMap_succ_V (n : ℕ) : + powerMap (n + 1) V = powerMap n V * lambda + V := by + change (universalPoint ^ (n + 1)).ofConv V = _ + rw [pow_succ universalPoint n, AlgHom.convMul_apply, ← Bialgebra.comulAlgHom_apply, + bialgebra_comulAlgHom, comul_V_formula] + simp [universalPoint, powerMap] + +theorem powerMap_succ_lambda (n : ℕ) : + powerMap (n + 1) lambda = powerMap n lambda * lambda := by + change (universalPoint ^ (n + 1)).ofConv lambda = _ + rw [pow_succ universalPoint n, AlgHom.convMul_apply, ← Bialgebra.comulAlgHom_apply, + bialgebra_comulAlgHom, comul_lambda] + simp [universalPoint, powerMap] + +theorem four_eq_zero : (4 : A) = 0 := by + obtain ⟨ha, _, hab, _, _⟩ := mapped_relations (AlgHom.id R A) + change aA ^ 3 = 0 at ha + change aA ^ 2 * bA + 2 = 0 at hab + linear_combination -(aA ^ 2 * bA - 2) * hab + aA * bA ^ 2 * ha + +theorem lambda_eq_one_add_theta : lambda = 1 + theta := by + unfold theta + ring + +theorem lambda_pow_four : lambda ^ 4 = 1 := by + have ht (k : ℕ) (hk : 2 ≤ k) : theta ^ k = 0 := pow_eq_zero_of_le hk theta_sq + rw [lambda_eq_one_add_theta] + linear_combination theta * four_eq_zero + 6 * theta_sq + 4 * ht 3 (by norm_num) + + ht 4 (by norm_num) + +theorem powerMap_lambda (n : ℕ) : powerMap n lambda = lambda ^ n := by + induction n with + | zero => simp [powerMap_zero_apply, counit_lambda] + | succ n ih => rw [powerMap_succ_lambda, ih, pow_succ lambda n] + +theorem powerMap_U (n : ℕ) : powerMap n U = (∑ i ∈ Finset.range n, lambda ^ i) * U := by + induction n with + | zero => simp [powerMap_zero_apply, counit_U] + | succ n ih => rw [powerMap_succ_U, ih, powerMap_lambda, geom_sum_succ']; ring + +theorem powerMap_V (n : ℕ) : powerMap n V = V * ∑ i ∈ Finset.range n, lambda ^ i := by + induction n with + | zero => simp [powerMap_zero_apply, counit_V] + | succ n ih => rw [powerMap_succ_V, ih, geom_sum_succ]; ring + +theorem geom_sum_four : ∑ i ∈ Finset.range 4, lambda ^ i = 2 * bA * V := by + have ht (k : ℕ) (hk : 2 ≤ k) : theta ^ k = 0 := pow_eq_zero_of_le hk theta_sq + simp only [Finset.sum_range_succ, Finset.sum_range_zero, zero_add, lambda_eq_one_add_theta] + linear_combination two_theta + (1 + theta) * four_eq_zero + 4 * theta_sq + ht 3 (by norm_num) + +theorem powerMap_four_U : powerMap 4 U = 2 * bA * U * V := by + rw [powerMap_U, geom_sum_four] + ring + +theorem two_b_U_V_ne_zero : 2 * bA * U * V ≠ 0 := by + intro h + have hOuter := congr_arg (fun x : A ↦ x.im) h + have hInner := congr_arg (fun x : B ↦ x.im) hOuter + apply two_b_ne_zero + simpa [bA, U, V, VB, IsScalarTower.algebraMap_apply R B A] using hInner + +theorem powerMap_four_U_ne_zero : powerMap 4 U ≠ 0 := by + rw [powerMap_four_U] + exact two_b_U_V_ne_zero + +theorem powerMap_four_V : powerMap 4 V = 0 := by + rw [powerMap_V, geom_sum_four] + have hv : V ^ 2 = aA ^ 2 * V := by + simp [aA, map_pow] + have hab : aA ^ 2 * bA + 2 = 0 := by + obtain ⟨_, _, hab, _, _⟩ := mapped_relations (AlgHom.id R A) + simpa using hab + rw [show V * (2 * bA * V) = 2 * bA * V ^ 2 by ring, hv] + linear_combination 2 * V * hab - V * four_eq_zero + +theorem geom_sum_eight : ∑ i ∈ Finset.range 8, lambda ^ i = 0 := by + have ht (k : ℕ) (hk : 2 ≤ k) : theta ^ k = 0 := pow_eq_zero_of_le hk theta_sq + simp only [Finset.sum_range_succ, Finset.sum_range_zero, zero_add, lambda_eq_one_add_theta] + linear_combination (2 + 7 * theta) * four_eq_zero + 56 * theta_sq + + 70 * ht 3 (by norm_num) + 56 * ht 4 (by norm_num) + 28 * ht 5 (by norm_num) + + 8 * ht 6 (by norm_num) + ht 7 (by norm_num) + +theorem powerMap_eight_U : powerMap 8 U = 0 := by + rw [powerMap_U, geom_sum_eight, zero_mul] + +theorem powerMap_eight_V : powerMap 8 V = 0 := by + rw [powerMap_V, geom_sum_eight, mul_zero] + +theorem powerMap_eight : powerMap 8 = (Algebra.ofId R A).comp counit := by + apply algHom_ext + · simp [powerMap_eight_U] + · simp [powerMap_eight_V] + +theorem universalPoint_pow_eight : universalPoint ^ 8 = 1 := + WithConv.ext powerMap_eight + +theorem universalPoint_pow_four_ne_one : universalPoint ^ 4 ≠ 1 := by + intro h + have h' : powerMap 4 = powerMap 0 := congr_arg WithConv.ofConv h + exact powerMap_four_U_ne_zero (by simpa using DFunLike.congr_fun h' U) + +/-- In the group of `A`-valued points of the group scheme, the universal point has order +exactly eight: an element of order eight on a group scheme of order four. -/ +theorem orderOf_universalPoint : orderOf universalPoint = 8 := by + simpa using orderOf_eq_prime_pow (p := 2) (n := 2) universalPoint_pow_four_ne_one + universalPoint_pow_eight + +/-! +### The Hopf algebra structure and the main statement + +Since the eighth convolution power of the identity is the convolution unit, the seventh +convolution power is a two-sided convolution inverse of the identity, that is, an antipode. +-/ + +private theorem powerMap_seven_mul_universalPoint : + toConv (powerMap 7) * universalPoint = 1 := by + simpa [powerMap, ← pow_succ] using universalPoint_pow_eight + +private theorem universalPoint_mul_powerMap_seven : + universalPoint * toConv (powerMap 7) = 1 := by + simpa [powerMap, ← pow_succ'] using universalPoint_pow_eight + +theorem antipode_right_identity : + ((Algebra.TensorProduct.lift (powerMap 7) (.id R A) fun _ ↦ Commute.all _).comp + (Bialgebra.comulAlgHom R A)) = + (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R A) := by + have h := congr_arg WithConv.ofConv powerMap_seven_mul_universalPoint + change + (Algebra.TensorProduct.lmul' R).comp + ((Algebra.TensorProduct.map (powerMap 7) (.id R A)).comp + (Bialgebra.comulAlgHom R A)) = + (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R A) at h + rw [← AlgHom.comp_assoc, Algebra.TensorProduct.lmul'_comp_map] at h + exact h + +theorem antipode_left_identity : + ((Algebra.TensorProduct.lift (.id R A) (powerMap 7) fun _ _ ↦ Commute.all _ _).comp + (Bialgebra.comulAlgHom R A)) = + (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R A) := by + have h := congr_arg WithConv.ofConv universalPoint_mul_powerMap_seven + change + (Algebra.TensorProduct.lmul' R).comp + ((Algebra.TensorProduct.map (.id R A) (powerMap 7)).comp + (Bialgebra.comulAlgHom R A)) = + (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R A) at h + rw [← AlgHom.comp_assoc, Algebra.TensorProduct.lmul'_comp_map] at h + exact h + +/-- The Hopf `R`-algebra structure on `A`. -/ +instance instHopfAlgebra : HopfAlgebra R A := + HopfAlgebra.ofAlgHom (powerMap 7) antipode_right_identity antipode_left_identity + +/-- The bundled commutative Hopf algebra representing the affine group scheme. -/ +def coordinateHopfAlgebra : CommHopfAlgCat R := + CommHopfAlgCat.of R A + +/-- The formal counterexample: over the nontrivial base ring `R`, the commutative Hopf +algebra `A` is finite free of rank four, and its fourth power map is not the convolution +unit. + +The freeness and finiteness conjuncts guarantee that the `Module.finrank` conjunct expresses +the honest rank of `A` over `R`. -/ +theorem counterexample : + Nontrivial R ∧ Module.Free R A ∧ Module.Finite R A ∧ Module.finrank R A = 4 ∧ + powerMap 4 ≠ (Algebra.ofId R A).comp counit := by + refine ⟨inferInstance, inferInstance, inferInstance, finrank_A, ?_⟩ + intro h + apply powerMap_four_U_ne_zero + simp [h] + +/-- **Grothendieck's question has a negative answer.** Grothendieck asked whether every finite +locally free group scheme of order `n` is killed by `n` — equivalently, whether the `n`-th +convolution power of the identity of a commutative Hopf algebra that is free of rank `n` over +the base ring is always the convolution unit `1` (the composite of the counit with the unit). +This is false: there is a nontrivial commutative ring `S` and a commutative `S`-Hopf algebra +`H`, free of finite rank over `S`, whose `(Module.finrank S H)`-th convolution power of the +identity is not the convolution unit. The witness is the rank-four Hopf algebra `A` over `R`; +see `counterexample`. -/ +theorem exists_hopfAlgebra_not_killed_by_finrank : + ∃ (S : Type) (_ : CommRing S) (_ : Nontrivial S) (H : Type) (_ : CommRing H) + (_ : HopfAlgebra S H) (_ : Module.Free S H) (_ : Module.Finite S H), + 0 < Module.finrank S H ∧ + WithConv.toConv (AlgHom.id S H) ^ Module.finrank S H ≠ 1 := by + refine ⟨R, inferInstance, inferInstance, A, inferInstance, inferInstance, inferInstance, + inferInstance, ?_, ?_⟩ + · rw [finrank_A]; norm_num + · rw [finrank_A] + have h8 : orderOf (WithConv.toConv (AlgHom.id R A)) = 8 := orderOf_universalPoint + exact pow_ne_one_of_lt_orderOf (by norm_num) (by rw [h8]; norm_num) + +/-! +### Non-cocommutativity + +By Deligne's theorem, a commutative finite locally free group scheme is killed by its order, +so the group scheme represented by `A` is necessarily noncommutative; equivalently, `A` is +not cocommutative. We verify this directly: the coefficient functional of `U` distinguishes +`Δ(U)` from its swap. +-/ + +/-- The `R`-linear coefficient functional of `U` in the basis `1, V, U, U * V` of `A`. -/ +private def coeffU : A →ₗ[R] R where + toFun x := x.im.re + map_add' _ _ := rfl + map_smul' _ _ := rfl + +/-- The `R`-linear coefficient functional of `V` in the basis `1, V, U, U * V` of `A`. -/ +private def coeffV : A →ₗ[R] R where + toFun x := x.re.im + map_add' _ _ := rfl + map_smul' _ _ := rfl + +/-- The Hopf algebra `A` is not cocommutative; equivalently, the affine group scheme it +represents is noncommutative. This is forced by Deligne's theorem, which affirms +Grothendieck's question for commutative group schemes. -/ +theorem not_isCocomm : ¬Coalgebra.IsCocomm R A := by + intro h + have hU := DFunLike.congr_fun h.comm_comp_comul U + simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, + ← Bialgebra.comulAlgHom_apply (R := R), bialgebra_comulAlgHom] at hU + rw [comul_U_formula] at hU + simp only [map_add, Algebra.TensorProduct.includeLeft_apply, + Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul, one_mul, + mul_one, TensorProduct.comm_tmul] at hU + have h2 := congr_arg (fun z ↦ TensorProduct.lid R R (TensorProduct.map coeffU coeffV z)) hU + have hV1 : coeffV 1 = 0 := rfl + have hVU : coeffV U = 0 := rfl + have hU1 : coeffU 1 = 0 := rfl + have hUU : coeffU U = 1 := rfl + have hVlam : coeffV lambda = b := by + change lambda.re.im = b + simp [lambda, aA, bA, U, V, VB, IsScalarTower.algebraMap_apply R B A] + simp only [map_add, TensorProduct.map_tmul, TensorProduct.lid_tmul, hV1, hVU, hVlam, hU1, + hUU, smul_eq_mul, one_mul, mul_zero, add_zero, zero_add] at h2 + exact two_b_ne_zero (by rw [h2, mul_zero]) + +/-! +### The group-scheme formulation + +Mathlib's antiequivalence `commHopfAlgCatEquivCogrpCommAlgCat` identifies commutative Hopf +algebras over `R` with group objects in `(CommAlgCat R)ᵒᵖ`, the opposite of the category of +commutative `R`-algebras. This opposite category is the category of affine schemes over `R` +(via the `Spec` antiequivalence), so these group objects are exactly the affine group schemes +over `R`; here the group object is `op A`, the algebraic incarnation of `Spec A`. We work +entirely on the algebra side and do not use `AlgebraicGeometry.Spec`, as Mathlib does not yet +connect commutative Hopf algebras to group objects in `AlgebraicGeometry.Scheme`. This +section transports the counterexample across that equivalence: the pointwise fourth power map +of the resulting group object is not the constant-unit endomorphism. +-/ + +open CategoryTheory MonObj Opposite + +/-- On the group object `op A` in `(CommAlgCat R)ᵒᵖ` — the affine group scheme corresponding +to `A` — the pointwise `n`-th power map `𝟙 _ ^ n` (the `n`-th power of the identity in the +convolution monoid `CategoryTheory.Hom.monoid` of endomorphisms; for a group scheme, the +morphism `x ↦ xⁿ`, which is not in general a homomorphism) corresponds to the `n`-th +convolution power of the identity of `A`. -/ +theorem id_pow_op_unop_hom (n : ℕ) : + (𝟙 (op (CommAlgCat.of R A)) ^ n).unop.hom = powerMap n := by + induction n with + | zero => rfl + | succ n ih => + have h : (𝟙 (op (CommAlgCat.of R A)) ^ (n + 1)).unop.hom = + (Algebra.TensorProduct.lift (powerMap n) (AlgHom.id R A) + fun _ _ ↦ Commute.all _ _).comp + (Bialgebra.comulAlgHom R A) := by + simp only [pow_succ, Hom.mul_def, unop_comp, CommAlgCat.hom_comp, + CommAlgCat.mul_op_of_unop_hom, CommAlgCat.lift_unop_hom, unop_id, CommAlgCat.hom_id, + ih] + rw [h, ← Algebra.TensorProduct.lmul'_comp_map, AlgHom.comp_assoc] + rfl + +/-- The pointwise fourth power map of the group object `op A` in `(CommAlgCat R)ᵒᵖ` — the +affine group scheme corresponding to `A` — is not the constant-unit endomorphism `1`. -/ +theorem id_pow_op_four_ne_one : 𝟙 (op (CommAlgCat.of R A)) ^ 4 ≠ 1 := by + intro h + have h' : powerMap 4 = powerMap 0 := by + rw [← id_pow_op_unop_hom, ← id_pow_op_unop_hom, pow_zero, h] + exact powerMap_four_U_ne_zero (by simpa using DFunLike.congr_fun h' U) + +/-- The rank-four counterexample as an affine group scheme: the group object in the opposite +of the category of commutative `R`-algebras corresponding to `coordinateHopfAlgebra` under +Mathlib's antiequivalence `commHopfAlgCatEquivCogrpCommAlgCat`. -/ +def affineGroupScheme : Grp (CommAlgCat R)ᵒᵖ := + ((commHopfAlgCatEquivCogrpCommAlgCat R).functor.obj coordinateHopfAlgebra).unop + +theorem affineGroupScheme_X : affineGroupScheme.X = op (CommAlgCat.of R A) := rfl + +/-- The order-four affine group scheme corresponding to `A` (the group object in +`(CommAlgCat R)ᵒᵖ`) is not killed by four: its pointwise fourth power map — the fourth power +of the identity in the convolution monoid of endomorphisms — is not the constant-unit +endomorphism `1`. -/ +theorem id_pow_affineGroupScheme_four_ne_one : 𝟙 affineGroupScheme.X ^ 4 ≠ 1 := + id_pow_op_four_ne_one + +end + +end Counterexample.GrothendieckPower diff --git a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean index d4c878ac16..9eed3c5bf4 100644 --- a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean +++ b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean @@ -71,6 +71,10 @@ theorem omega_mul_omega_eq_add : (ω : QuadraticAlgebra R a b) * ω = a • 1 + b • ω := by ext <;> simp +theorem omega_mul_omega_eq_algebraMap : + (ω : QuadraticAlgebra R a b) * ω = algebraMap R _ a + algebraMap R _ b * ω := by + simp [omega_mul_omega_eq_add, Algebra.algebraMap_eq_smul_one] + @[simp] theorem omega_mul_mk (x y : R) : (ω : QuadraticAlgebra R a b) * ⟨x, y⟩ = ⟨a * y, x + b * y⟩ := by ext <;> simp diff --git a/docs/references.bib b/docs/references.bib index 0864bf21e7..a5c810a596 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -4680,6 +4680,15 @@ @Book{ Okninski1991 year = {1991} } +@Article{ oorttate1970, + author = {Oort, Frans and Tate, John}, + title = {Group schemes of prime order}, + journal = {Ann. Sci. \'{E}cole Norm. Sup. (4)}, + volume = {3}, + year = {1970}, + pages = {1--21} +} + @Article{ ore33, issn = {0003486X, 19398980}, url = {http://www.jstor.org/stable/1968173}, @@ -5809,6 +5818,16 @@ @Book{ tao2010 url = {https://terrytao.files.wordpress.com/2010/02/epsilon.pdf} } +@InCollection{ tate1997, + author = {Tate, John}, + title = {Finite flat group schemes}, + booktitle = {Modular forms and {F}ermat's last theorem ({B}oston, {MA}, + 1995)}, + pages = {121--154}, + publisher = {Springer, New York}, + year = {1997} +} + @Article{ Taylor-Wiles-FLT, author = {Taylor, Richard and Wiles, Andrew}, title = {Ring-theoretic properties of certain {H}ecke algebras}, From 8d2ab6981b5112e5f3e7cde2f37d2996a7865e45 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Mon, 3 Aug 2026 13:47:15 +0000 Subject: [PATCH 08/16] refactor(RingTheory/DedekindDomain): make `IsDedekindDomainInv` private (#42392) Make `IsDedekindDomainInv` private, because is the same as `IsDedekindDomain`. See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/three.20dedekind.20domains/near/574535735). --- .../DedekindDomain/Ideal/Basic.lean | 287 +++++++++--------- 1 file changed, 144 insertions(+), 143 deletions(-) diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean b/Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean index e328c4ba9d..fa2d336e15 100644 --- a/Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean +++ b/Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean @@ -20,14 +20,12 @@ Further results on the structure of ideals in a Dedekind domain are found in ## Main definitions -- `IsDedekindDomainInv` alternatively defines a Dedekind domain as an integral domain where - every nonzero fractional ideal is invertible. -- `isDedekindDomainInv_iff` shows that this does not depend on the choice of field of - fractions. +- `isDedekindDomain_iff_mul_inv_cancel` shows an integral domain is + a Dedekind domain iff every nonzero fractional ideal is invertible. ## Main results: -- `isDedekindDomain_iff_isDedekindDomainInv` +- `isDedekindDomain_iff_mul_inv_cancel` - `Ideal.uniqueFactorizationMonoid` ## Implementation notes @@ -49,40 +47,18 @@ to add a `(h : ¬ IsField A)` assumption whenever this is explicitly needed. dedekind domain, dedekind ring -/ -@[expose] public section - variable (R A K : Type*) [CommRing R] [CommRing A] [Field K] open scoped nonZeroDivisors Polynomial -section Inverse - -section IsDedekindDomainInv - -variable [IsDomain A] -/-- A Dedekind domain is an integral domain such that every fractional ideal has an inverse. - -This is equivalent to `IsDedekindDomain`. -In particular we provide a `CommGroupWithZero` instance, -assuming `IsDedekindDomain A`, which implies `IsDedekindDomainInv`. For **integral** domain, -`IsDedekindDomain`(`Inv`) implies only `Ideal.isCancelMulZero`. --/ -def IsDedekindDomainInv : Prop := - ∀ I ≠ (⊥ : FractionalIdeal A⁰ (FractionRing A)), I * I⁻¹ = 1 - -open FractionalIdeal +public section Inverse -variable {R A K} +variable [Algebra A K] [IsFractionRing A K] -theorem isDedekindDomainInv_iff [Algebra A K] [IsFractionRing A K] : - IsDedekindDomainInv A ↔ ∀ I ≠ (⊥ : FractionalIdeal A⁰ K), I * I⁻¹ = 1 := by - let h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := - FractionalIdeal.mapEquiv (FractionRing.algEquiv A K) - refine h.toEquiv.forall_congr (fun {x} => ?_) - rw [← h.toEquiv.apply_eq_iff_eq] - simp [h] +variable {A K} -theorem FractionalIdeal.adjoinIntegral_eq_one_of_isUnit [Algebra A K] [IsFractionRing A K] (x : K) +variable {R} [IsDomain A] in +theorem FractionalIdeal.adjoinIntegral_eq_one_of_isUnit (x : K) (hx : IsIntegral A x) (hI : IsUnit (adjoinIntegral A⁰ x hx)) : adjoinIntegral A⁰ x hx = 1 := by set I := adjoinIntegral A⁰ x hx have mul_self : IsIdempotentElem I := by @@ -92,92 +68,6 @@ theorem FractionalIdeal.adjoinIntegral_eq_one_of_isUnit [Algebra A K] [IsFractio convert! congr_arg (· * I⁻¹) mul_self <;> simp only [(mul_inv_cancel_iff_isUnit K).mpr hI, mul_assoc, mul_one] -namespace IsDedekindDomainInv - -variable [Algebra A K] [IsFractionRing A K] (h : IsDedekindDomainInv A) {I J : FractionalIdeal A⁰ K} -include h - -/-- `IsDedekindDomainInv A` implies that fractional ideals over it form a commutative group with -zero. -/ -noncomputable abbrev commGroupWithZero : CommGroupWithZero (FractionalIdeal A⁰ K) where - inv_zero := inv_zero' _ - mul_inv_cancel := isDedekindDomainInv_iff.mp h - div_eq_mul_inv I J := by - obtain rfl | hJ := eq_or_ne J 0 - · simp [inv_zero'] - refine le_antisymm ?_ ((FractionalIdeal.le_div_iff_mul_le hJ).2 ?_) - · suffices I / J * J ≤ I by - simpa [mul_assoc, isDedekindDomainInv_iff.mp h _ hJ] using mul_left_mono (a := J⁻¹) this - simp [FractionalIdeal.mul_le, mem_div_iff_of_ne_zero hJ] - · rw [mul_assoc, mul_comm _ J, isDedekindDomainInv_iff.mp h _ hJ, mul_one] - -theorem isNoetherianRing : IsNoetherianRing A := by - let := h.commGroupWithZero (K := FractionRing A) - refine isNoetherianRing_iff.mpr ⟨fun I : Ideal A => ?_⟩ - by_cases hI : I = ⊥ - · rw [hI]; apply Submodule.fg_bot - have hI : (I : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hI - exact I.fg_of_isUnit (IsFractionRing.injective A (FractionRing A)) hI.isUnit - -theorem integrallyClosed : IsIntegrallyClosed A := by - let := h.commGroupWithZero (K := FractionRing A) - -- It suffices to show that for integral `x`, - -- `A[x]` (which is a fractional ideal) is in fact equal to `A`. - refine (isIntegrallyClosed_iff (FractionRing A)).mpr (fun {x hx} => ?_) - rw [← Set.mem_range, ← Algebra.mem_bot, ← Subalgebra.mem_toSubmodule, Algebra.toSubmodule_bot, - Submodule.one_eq_span, ← coe_spanSingleton A⁰ (1 : FractionRing A), spanSingleton_one, ← - FractionalIdeal.adjoinIntegral_eq_one_of_isUnit x hx (Ne.isUnit _)] - · exact mem_adjoinIntegral_self A⁰ x hx - · exact fun h => one_ne_zero (eq_zero_iff.mp h 1 (Algebra.adjoin A {x}).one_mem) - -open Ring - -theorem dimensionLEOne : DimensionLEOne A := by - -- We're going to show that `P` is maximal because any (maximal) ideal `M` - -- that is strictly larger would be `⊤`. - let := h.commGroupWithZero (K := FractionRing A) - constructor - rintro P P_ne hP - refine Ideal.isMaximal_def.mpr ⟨hP.ne_top, fun M hM => ?_⟩ - -- We may assume `P` and `M` (as fractional ideals) are nonzero. - have P'_ne : (P : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr P_ne - have M'_ne : (M : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hM.ne_bot - -- In particular, we'll show `M⁻¹ * P ≤ P` - suffices (M⁻¹ : FractionalIdeal A⁰ (FractionRing A)) * P ≤ P by - rw [eq_top_iff, ← coeIdeal_le_coeIdeal (FractionRing A), coeIdeal_top] - calc - (1 : FractionalIdeal A⁰ (FractionRing A)) = (↑M)⁻¹ * P * ((↑P)⁻¹ * M) := by - simp [mul_assoc, *] - _ ≤ P * ((↑P)⁻¹ * M) := by gcongr - _ = M := by simp [*] - -- Suppose we have `x ∈ M⁻¹ * P`, then in fact `x = algebraMap _ _ y` for some `y`. - intro x hx - have le_one : (M⁻¹ : FractionalIdeal A⁰ (FractionRing A)) * P ≤ 1 := by - rw [← inv_mul_cancel₀ M'_ne]; gcongr - obtain ⟨y, _hy, rfl⟩ := (mem_coeIdeal _).mp (le_one hx) - -- Since `M` is strictly greater than `P`, let `z ∈ M \ P`. - obtain ⟨z, hzM, hzp⟩ := SetLike.exists_of_lt hM - -- We have `z * y ∈ M * (M⁻¹ * P) = P`. - have zy_mem := mul_mem_mul (mem_coeIdeal_of_mem A⁰ hzM) hx - rw [← map_mul, ← mul_assoc, mul_inv_cancel₀ M'_ne, one_mul] at zy_mem - obtain ⟨zy, hzy, zy_eq⟩ := (mem_coeIdeal A⁰).mp zy_mem - rw [IsFractionRing.injective A (FractionRing A) zy_eq] at hzy - -- But `P` is a prime ideal, so `z ∉ P` implies `y ∈ P`, as desired. - exact mem_coeIdeal_of_mem A⁰ (Or.resolve_left (hP.mem_or_mem hzy) hzp) - -/-- Showing one side of the equivalence between the definitions -`IsDedekindDomainInv` and `IsDedekindDomain` of Dedekind domains. -/ -theorem isDedekindDomain : IsDedekindDomain A := - { h.isNoetherianRing, h.dimensionLEOne, h.integrallyClosed with } - -end IsDedekindDomainInv - -end IsDedekindDomainInv - -variable [Algebra A K] [IsFractionRing A K] - -variable {A K} - theorem FractionalIdeal.one_mem_inv_coe_ideal [IsDomain A] {I : Ideal A} (hI : I ≠ ⊥) : (1 : K) ∈ (I : FractionalIdeal A⁰ K)⁻¹ := by rw [mem_inv_iff (coeIdeal_ne_zero.mpr hI)] @@ -324,19 +214,145 @@ theorem coe_ideal_mul_inv (I : Ideal A) (hI0 : I ≠ ⊥) : I * (I : FractionalI | zero => rw [pow_zero]; exact one_mem_inv_coe_ideal hI0 | succ i ih => rw [pow_succ']; exact x_mul_mem _ ih +end FractionalIdeal + +end Inverse + +section IsDedekindDomainInv + +/-- An integral domain is a Dedekind domain if every fractional ideal has an inverse. +This is an auxiliary definition used to +prove `isDedekindDomain_iff_mul_inv_cancel` and `FractionalIdeal.semifield`. -/ +def IsDedekindDomainInv [IsDomain A] : Prop := + ∀ I ≠ (⊥ : FractionalIdeal A⁰ (FractionRing A)), I * I⁻¹ = 1 + +open FractionalIdeal + +variable {A K} [Algebra A K] [IsFractionRing A K] + +variable {R} in +theorem isDedekindDomainInv_iff [IsDomain A] : + IsDedekindDomainInv A ↔ ∀ I ≠ (⊥ : FractionalIdeal A⁰ K), I * I⁻¹ = 1 := by + let h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := + FractionalIdeal.mapEquiv (FractionRing.algEquiv A K) + refine h.toEquiv.forall_congr (fun {x} => ?_) + rw [← h.toEquiv.apply_eq_iff_eq] + simp [h] + +namespace IsDedekindDomainInv + +variable (K) [IsDomain A] (h : IsDedekindDomainInv A) {I J : FractionalIdeal A⁰ K} +include h + +/-- `IsDedekindDomainInv A` implies that fractional ideals over it form a commutative group with +zero. -/ +noncomputable abbrev commGroupWithZero : CommGroupWithZero (FractionalIdeal A⁰ K) where + inv_zero := inv_zero' _ + mul_inv_cancel := isDedekindDomainInv_iff.mp h + div_eq_mul_inv I J := by + obtain rfl | hJ := eq_or_ne J 0 + · simp [inv_zero'] + refine le_antisymm ?_ ((FractionalIdeal.le_div_iff_mul_le hJ).2 ?_) + · suffices I / J * J ≤ I by + simpa [mul_assoc, isDedekindDomainInv_iff.mp h _ hJ] using mul_left_mono (a := J⁻¹) this + simp [FractionalIdeal.mul_le, mem_div_iff_of_ne_zero hJ] + · rw [mul_assoc, mul_comm _ J, isDedekindDomainInv_iff.mp h _ hJ, mul_one] + +theorem isNoetherianRing : IsNoetherianRing A := by + let := h.commGroupWithZero (FractionRing A) + refine isNoetherianRing_iff.mpr ⟨fun I : Ideal A => ?_⟩ + by_cases hI : I = ⊥ + · rw [hI]; apply Submodule.fg_bot + have hI : (I : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hI + exact I.fg_of_isUnit (IsFractionRing.injective A (FractionRing A)) hI.isUnit + +theorem integrallyClosed : IsIntegrallyClosed A := by + let := h.commGroupWithZero (FractionRing A) + -- It suffices to show that for integral `x`, + -- `A[x]` (which is a fractional ideal) is in fact equal to `A`. + refine (isIntegrallyClosed_iff (FractionRing A)).mpr (fun {x hx} => ?_) + rw [← Set.mem_range, ← Algebra.mem_bot, ← Subalgebra.mem_toSubmodule, Algebra.toSubmodule_bot, + Submodule.one_eq_span, ← coe_spanSingleton A⁰ (1 : FractionRing A), spanSingleton_one, ← + FractionalIdeal.adjoinIntegral_eq_one_of_isUnit x hx (Ne.isUnit _)] + · exact mem_adjoinIntegral_self A⁰ x hx + · exact fun h => one_ne_zero (eq_zero_iff.mp h 1 (Algebra.adjoin A {x}).one_mem) + +open Ring + +theorem dimensionLEOne : DimensionLEOne A := by + -- We're going to show that `P` is maximal because any (maximal) ideal `M` + -- that is strictly larger would be `⊤`. + let := h.commGroupWithZero (K := FractionRing A) + constructor + rintro P P_ne hP + refine Ideal.isMaximal_def.mpr ⟨hP.ne_top, fun M hM => ?_⟩ + -- We may assume `P` and `M` (as fractional ideals) are nonzero. + have P'_ne : (P : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr P_ne + have M'_ne : (M : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hM.ne_bot + -- In particular, we'll show `M⁻¹ * P ≤ P` + suffices (M⁻¹ : FractionalIdeal A⁰ (FractionRing A)) * P ≤ P by + rw [eq_top_iff, ← coeIdeal_le_coeIdeal (FractionRing A), coeIdeal_top] + calc + (1 : FractionalIdeal A⁰ (FractionRing A)) = (↑M)⁻¹ * P * ((↑P)⁻¹ * M) := by + simp [mul_assoc, *] + _ ≤ P * ((↑P)⁻¹ * M) := by gcongr + _ = M := by simp [*] + -- Suppose we have `x ∈ M⁻¹ * P`, then in fact `x = algebraMap _ _ y` for some `y`. + intro x hx + have le_one : (M⁻¹ : FractionalIdeal A⁰ (FractionRing A)) * P ≤ 1 := by + rw [← inv_mul_cancel₀ M'_ne]; gcongr + obtain ⟨y, _hy, rfl⟩ := (mem_coeIdeal _).mp (le_one hx) + -- Since `M` is strictly greater than `P`, let `z ∈ M \ P`. + obtain ⟨z, hzM, hzp⟩ := SetLike.exists_of_lt hM + -- We have `z * y ∈ M * (M⁻¹ * P) = P`. + have zy_mem := mul_mem_mul (mem_coeIdeal_of_mem A⁰ hzM) hx + rw [← map_mul, ← mul_assoc, mul_inv_cancel₀ M'_ne, one_mul] at zy_mem + obtain ⟨zy, hzy, zy_eq⟩ := (mem_coeIdeal A⁰).mp zy_mem + rw [IsFractionRing.injective A (FractionRing A) zy_eq] at hzy + -- But `P` is a prime ideal, so `z ∉ P` implies `y ∈ P`, as desired. + exact mem_coeIdeal_of_mem A⁰ (Or.resolve_left (hP.mem_or_mem hzy) hzp) + +end IsDedekindDomainInv + +/-- `IsDedekindDomain` and `IsDedekindDomainInv` are equivalent ways +to express that an integral domain is a Dedekind domain. -/ +theorem isDedekindDomain_iff_isDedekindDomainInv [IsDomain A] : + IsDedekindDomain A ↔ IsDedekindDomainInv A := by + refine ⟨fun _ I hI => ?_, fun h => + { h.isNoetherianRing, h.dimensionLEOne, h.integrallyClosed with }⟩ + obtain ⟨a, J, ha, hJ⟩ := exists_eq_spanSingleton_mul (K := FractionRing A) I + suffices h₂ : I * (spanSingleton A⁰ (algebraMap _ _ a) * (J : FractionalIdeal A⁰ _)⁻¹) = 1 by + rw [mul_inv_cancel_iff] + exact ⟨spanSingleton A⁰ (algebraMap _ _ a) * (J : FractionalIdeal A⁰ _)⁻¹, h₂⟩ + subst hJ + rw [mul_assoc, mul_left_comm (J : FractionalIdeal A⁰ _), coe_ideal_mul_inv, mul_one, + spanSingleton_mul_spanSingleton, inv_mul_cancel₀, spanSingleton_one] + · exact mt ((injective_iff_map_eq_zero (algebraMap A _)).mp (IsFractionRing.injective A _) _) ha + · exact coeIdeal_ne_zero.mp (right_ne_zero_of_mul hI) + +public theorem isDedekindDomain_iff_mul_inv_cancel [IsDomain A] : + IsDedekindDomain A ↔ ∀ I ≠ (⊥ : FractionalIdeal A⁰ K), I * I⁻¹ = 1 := + isDedekindDomain_iff_isDedekindDomainInv.trans isDedekindDomainInv_iff + +end IsDedekindDomainInv + +public section IsDedekindDomain + +variable {R A} +variable [IsDedekindDomain A] [Algebra A K] [IsFractionRing A K] + +open FractionalIdeal Ideal + +namespace FractionalIdeal + noncomputable instance semifield : Semifield (FractionalIdeal A⁰ K) where __ := coeIdeal_injective.nontrivial __ : CommSemiring (FractionalIdeal A⁰ K) := inferInstance - __ := IsDedekindDomainInv.commGroupWithZero fun I hI ↦ by - obtain ⟨a, J, ha, hJ⟩ := exists_eq_spanSingleton_mul (K := FractionRing A) I - suffices h₂ : I * (spanSingleton A⁰ (algebraMap _ _ a) * (J : FractionalIdeal A⁰ _)⁻¹) = 1 by - rw [mul_inv_cancel_iff] - exact ⟨spanSingleton A⁰ (algebraMap _ _ a) * (J : FractionalIdeal A⁰ _)⁻¹, h₂⟩ - subst hJ - rw [mul_assoc, mul_left_comm (J : FractionalIdeal A⁰ _), coe_ideal_mul_inv, mul_one, - spanSingleton_mul_spanSingleton, inv_mul_cancel₀, spanSingleton_one] - · exact mt ((injective_iff_map_eq_zero (algebraMap A _)).mp (IsFractionRing.injective A _) _) ha - · exact coeIdeal_ne_zero.mp (right_ne_zero_of_mul hI) + inv_zero := inv_zero' K + mul_inv_cancel := isDedekindDomain_iff_mul_inv_cancel.mp ‹_› + div_eq_mul_inv := by + let := (isDedekindDomain_iff_isDedekindDomainInv.mp ‹_›).commGroupWithZero K + exact div_eq_mul_inv nnqsmul := _ instance : PosMulStrictMono (FractionalIdeal A⁰ K) := PosMulMono.toPosMulStrictMono @@ -365,21 +381,6 @@ instance : PosMulReflectLE (Ideal A) where end FractionalIdeal -/-- `IsDedekindDomain` and `IsDedekindDomainInv` are equivalent ways -to express that an integral domain is a Dedekind domain. -/ -theorem isDedekindDomain_iff_isDedekindDomainInv [IsDomain A] : - IsDedekindDomain A ↔ IsDedekindDomainInv A := - ⟨fun _h _I => mul_inv_cancel₀, fun h => h.isDedekindDomain⟩ - -end Inverse - -section IsDedekindDomain - -variable {R A} -variable [IsDedekindDomain A] [Algebra A K] [IsFractionRing A K] - -open FractionalIdeal Ideal - noncomputable instance Ideal.isCancelMulZero : IsCancelMulZero (Ideal A) := Function.Injective.isCancelMulZero (coeIdealHom A⁰ (FractionRing A)) coeIdeal_injective (map_zero _) (map_mul _) From 93594942ef3b93fae5272d7bf368676ff40f8eb1 Mon Sep 17 00:00:00 2001 From: Kevin Wilson <1527442+khwilson@users.noreply.github.com> Date: Mon, 3 Aug 2026 14:17:52 +0000 Subject: [PATCH 09/16] feat(Topology/Semicontinuity/Hemicontinuity): sequential characterizations of hemicontinuity (#40377) We prove two things: First, we prove a sequential characterization of lower hemicontinuity in terms of sequences. `LowerHemicontinuousAt.of_sequences` Second, we show that upper and lower hemicontinuity are preserved under uniform limits in the Hausdorff uniformity. N.B. the increase in imports comes from importing uniformity structures (including the Hausdorff uniformity). If preferred, I can break these uniform convergence lemmas out into their own file to minimize imports in this file. AI Disclosure: Initial proof outlined by me, lean statement written by me, initial draft of lean proof provided by claude code, then I provided edits, comments, and docstrings - [x] depends on: #38601 Co-authored-by: Kevin H Wilson --- .../Semicontinuity/Hemicontinuity.lean | 179 +++++++++++++++++- 1 file changed, 174 insertions(+), 5 deletions(-) diff --git a/Mathlib/Topology/Semicontinuity/Hemicontinuity.lean b/Mathlib/Topology/Semicontinuity/Hemicontinuity.lean index b7271bbeb3..818c5ace81 100644 --- a/Mathlib/Topology/Semicontinuity/Hemicontinuity.lean +++ b/Mathlib/Topology/Semicontinuity/Hemicontinuity.lean @@ -9,6 +9,9 @@ public import Mathlib.Topology.Semicontinuity.Defs public import Mathlib.Topology.NhdsWithin public import Mathlib.Topology.Separation.Regular public import Mathlib.Topology.Defs.Sequences +public import Mathlib.Topology.UniformSpace.Closeds +public import Mathlib.Topology.UniformSpace.UniformConvergence +import Mathlib.Topology.UniformSpace.Compact import Mathlib.Topology.Sequences /-! # Hemicontinuity @@ -21,9 +24,13 @@ public section open Set Filter Topology -variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β] +variable {α β : Type*} [TopologicalSpace α] variable {f g : α → Set β} {s : Set α} {x : α} +section facts + +variable [TopologicalSpace β] + /-! ### Basic facts -/ lemma upperHemicontinuousWithinAt_iff_forall_isOpen : @@ -392,18 +399,84 @@ lemma UpperHemicontinuousAt.mem_of_tendsto {ι : Type*} [RegularSpace β] {x₀ simp only [← subset_interior_iff_mem_nhdsSet, preimage_ofPred_eq, mem_ofPred_eq] at hn exact interior_subset <| hn hyn +/-- **Sequential characterization of lower hemicontinuity**: +A set-valued function `f : α → Set β` is lower hemicontinuous at `x₀ : α` if for every sequence +`x : ℕ → α` tending to `x₀` and every `y₀ ∈ f x₀`, there exists a sequence `y : ℕ → β` with +`y n ∈ f (x n)` for all `n` that tends to `y₀`. -/ +lemma LowerHemicontinuousAt.of_sequences {x₀ : α} [(𝓝 x₀).IsCountablyGenerated] + (h : ∀ x : ℕ → α, Tendsto x atTop (𝓝 x₀) → + ∀ y₀ ∈ f x₀, ∃ y : ℕ → β, (∀ n, y n ∈ f (x n)) ∧ Tendsto y atTop (𝓝 y₀)) : + LowerHemicontinuousAt f x₀ := by + rw [lowerHemicontinuousAt_iff] + intro U hU ⟨y₀, hy₀f, hy₀U⟩ + by_contra hc + rw [Filter.not_eventually] at hc + obtain ⟨x, hx, hxU⟩ := exists_seq_forall_of_frequently hc + obtain ⟨y, hy_mem, hy_lim⟩ := h x hx y₀ hy₀f + obtain ⟨n, hn⟩ := (hy_lim.eventually (hU.mem_nhds hy₀U)).exists + exact hxU n ⟨y n, hy_mem n, hn⟩ + +/-- **Sequential characterization of lower hemicontinuity**: +If `f : α → Set β` is lower hemicontinuous at `x₀`, `y₀ ∈ f x₀`, `𝓝 y₀` is countably generated, and +`x : ℕ → α` tends to `x₀`, then there is a companion sequence `y : ℕ → β` that tends to `y₀` with +`y n ∈ f (x n)` for all sufficiently large `n`. + +This is a partial converse of `LowerHemicontinuousAt.of_sequences`. -/ +lemma LowerHemicontinuousAt.exists_seq_tendsto {x₀ : α} (hf : LowerHemicontinuousAt f x₀) + {x : ℕ → α} (hx : Tendsto x atTop (𝓝 x₀)) {y₀ : β} (hy₀ : y₀ ∈ f x₀) + [(𝓝 y₀).IsCountablyGenerated] : + ∃ y : ℕ → β, (∀ᶠ n in atTop, y n ∈ f (x n)) ∧ Tendsto y atTop (𝓝 y₀) := by + classical + obtain ⟨U, hU, hUbasis⟩ := (nhds_basis_opens y₀).exists_antitone_subbasis + have hev (k) : ∀ᶠ n in atTop, (f (x n) ∩ U k).Nonempty := + hx.eventually <| (lowerHemicontinuousAt_iff.mp hf) (U k) (hU k).2 ⟨y₀, hy₀, (hU k).1⟩ + -- For each `n`, find the largest `k ≤ n` where `U k` intersects `f (x n)`. + let g : ℕ → ℕ := fun n ↦ Nat.findGreatest (fun k ↦ (f (x n) ∩ U k).Nonempty) n + have key (n k) (hkn : k ≤ n) (hk : (f (x n) ∩ U k).Nonempty) : (f (x n) ∩ U (g n)).Nonempty := + Nat.findGreatest_spec (P := fun k ↦ (f (x n) ∩ U k).Nonempty) hkn hk + -- Define `y n` to be some element of `f (x n) ∩ U (g n)` (or be arbitrary) + let y : ℕ → β := fun n ↦ if h : (f (x n) ∩ U (g n)).Nonempty then h.some else y₀ + have hy (n) (h : (f (x n) ∩ U (g n)).Nonempty) : y n ∈ f (x n) ∩ U (g n) := by + simpa only [y, dif_pos h] using h.some_mem + refine ⟨y, (hev 0).mono (by grind), ?_⟩ + -- Have to show for all `k`, eventually, all `y n ∈ U k`. + rw [hUbasis.tendsto_right_iff] + intro k _ + filter_upwards [hev k, eventually_ge_atTop k] with n hk hkn + exact hUbasis.antitone (Nat.le_findGreatest hkn hk) (hy n (key n k hkn hk)).2 + +/-- **Lower hemicontinuity along a countably generated filter** (subsequence form): +if `f : α → Set β` is lower hemicontinuous at `x₀`, `y₀ ∈ f x₀`, `𝓝 y₀` is countably generated and +`x : ι → α` tends to `x₀` along a nontrivial countably generated filter `l`, then some sequence +`u : ℕ → ι` converging to `l` admits a companion `y : ℕ → β` tending to `y₀` with +`y k ∈ f (x (u k))` eventually. + +For a general filter one must pass to the subsequence `u`: the "same-index" conclusion already +fails for `l = pure i₀` (which is `NeBot` and countably generated). When `l = atTop` one may take +`u = id`, recovering `LowerHemicontinuousAt.exists_seq_tendsto`. -/ +lemma LowerHemicontinuousAt.exists_subseq_tendsto {ι : Type*} {l : Filter ι} [l.NeBot] + [l.IsCountablyGenerated] {x₀ : α} (hf : LowerHemicontinuousAt f x₀) {x : ι → α} + (hx : Tendsto x l (𝓝 x₀)) {y₀ : β} (hy₀ : y₀ ∈ f x₀) [(𝓝 y₀).IsCountablyGenerated] : + ∃ (u : ℕ → ι) (y : ℕ → β), Tendsto u atTop l ∧ + (∀ᶠ k in atTop, y k ∈ f (x (u k))) ∧ Tendsto y atTop (𝓝 y₀) := by + obtain ⟨u, hu⟩ := Filter.exists_seq_tendsto l + obtain ⟨y, hy_mem, hy_lim⟩ := hf.exists_seq_tendsto (hx.comp hu) hy₀ + exact ⟨u, y, hu, hy_mem, hy_lim⟩ + + + +end facts + /-! ### Open lower sections -/ -omit [TopologicalSpace β] in /-- A correspondence `f : α → Set β` has open lower sections if and only if its *lower inverse* -(i.e., `b : β ↦ (f ⁻¹' (Iic {b}ᶜ))ᶜ = {x | b ∈ f x}`) sends every point to an open set. -/ +(i.e., `b : β ↦ (f ⁻¹' Iic {b}ᶜ)ᶜ = {x | b ∈ f x}`) sends every point to an open set. -/ lemma hasOpenLowerSections_iff_isOpen_compl_preimage_Iic_compl : HasOpenLowerSections f ↔ ∀ b, IsOpen (f ⁻¹' Iic {b}ᶜ)ᶜ := by have h (b : β) : (f ⁻¹' (Iic {b}ᶜ))ᶜ = {x | b ∈ f x} := by simp [Set.ext_iff, Iic, Set.mem_compl_iff] simp_rw [h, hasOpenLowerSections_iff_isOpen] -omit [TopologicalSpace β] in /-- A correspondence `f : α → Set β` has open lower sections if and only if its *upper inverse* (i.e., `b : β ↦ f ⁻¹' (Iic {b}ᶜ) = {x | b ∉ f x}`) sends every point to a closed set. -/ lemma hasOpenLowerSections_iff_isClosed_preimage_Iic : @@ -415,7 +488,7 @@ lemma hasOpenLowerSections_iff_isClosed_preimage_Iic : /-- A lower hemicontinuous function intersected with a function with an open graph is lower hemicontinuous. -/ -lemma LowerHemicontinuous.inter_hasOpenCGraph {f g : α → Set β} +lemma LowerHemicontinuous.inter_hasOpenCGraph [TopologicalSpace β] {f g : α → Set β} (hf : LowerHemicontinuous f) (hg : HasOpenCGraph g) : LowerHemicontinuous (fun x ↦ f x ∩ g x) := by simp_rw [lowerHemicontinuous_iff_isOpen_inter_nonempty] at ⊢ hf @@ -427,3 +500,99 @@ lemma LowerHemicontinuous.inter_hasOpenCGraph {f g : α → Set β} ⟨hxU, y, hyf, hyt, hyV⟩⟩ intro x' ⟨hx'U, z, hzf, hzt, hzV⟩ exact ⟨z, ⟨hzf, hUV (Set.mk_mem_prod hx'U hzV)⟩, hzt⟩ + +/-! ### Uniform Limits + +Like continuity, hemicontinuity is preserved under certain uniform limits, where the uniformity on +the target `Set β` is the Hausdorff uniformity. In this section, we prove this result for both +lower hemicontinuous and upper hemicontinuous limits. +-/ + +section limits + +variable {ι : Type*} {F : ι → α → Set β} {l : Filter ι} [NeBot l] +variable [UniformSpace β] +open UniformSpace +attribute [local instance] UniformSpace.hausdorff + +/-- A net of lower hemicontinuous set-valued functions converging uniformly on `s` (along a +filter `l`) in the Hausdorff uniformity has a lower hemicontinuous limit on `s` -/ +theorem TendstoUniformlyOn.lowerHemicontinuousOn (htendsto : TendstoUniformlyOn F f l s) + (hF : ∀ n, LowerHemicontinuousOn (F n) s) : LowerHemicontinuousOn f s := by + rw [lowerHemicontinuousOn_iff] + intro x₀ hx₀s + rw [lowerHemicontinuousWithinAt_iff] + intro V hV ⟨y₀, hy₀f, hy₀V⟩ + -- Obtain entourages W, U ∈ 𝓤 β with U ○ U ○ U ⊆ W + obtain ⟨W, hW, hWsub⟩ := UniformSpace.mem_nhds_iff.mp (hV.mem_nhds hy₀V) + obtain ⟨U₁, hU₁, hU₁sym, hU₁comp⟩ := comp_symm_mem_uniformity_sets hW + obtain ⟨U, hU, hUsym, hUcomp⟩ := comp_symm_mem_uniformity_sets hU₁ + have hU_le_U₁ : U ⊆ U₁ := fun _p hp => hUcomp ⟨_, refl_mem_uniformity hU, hp⟩ + -- Eventually, ⟨f x, F N x⟩ ∈ hausdorffEntourage U for all x ∈ s + have hHU : hausdorffEntourage U ∈ @uniformity (Set β) (UniformSpace.hausdorff (α := β)) := + (mem_lift'_sets monotone_hausdorffEntourage).mpr ⟨U, hU, le_refl _⟩ + obtain ⟨N, hN⟩ := (htendsto (hausdorffEntourage U) hHU).exists + -- In which case, ⟨y₀, z₀⟩ ∈ U for some z₀ ∈ F N x₀ + obtain ⟨z₀, hz₀FN, hz₀y₀⟩ := + ((mem_hausdorffEntourage U (f x₀) (F N x₀)).mp (hN x₀ hx₀s)).1 hy₀f + -- By lower hemicontinuity, a ball around z₀ intersects all x in a neighborhood of x₀ + obtain ⟨U', ⟨hU'mem, hU'open⟩, hU'sub⟩ := uniformity_hasBasis_open.mem_iff.mp hU + have hmeet₀ : (F N x₀ ∩ ball z₀ U').Nonempty := ⟨z₀, hz₀FN, mem_ball_self z₀ hU'mem⟩ + have hSmeet : ∀ᶠ x in 𝓝[s] x₀, (F N x ∩ ball z₀ U').Nonempty := + lowerHemicontinuousWithinAt_iff.mp (hF _ _ hx₀s) _ (isOpen_ball _ hU'open) hmeet₀ + filter_upwards [hSmeet, self_mem_nhdsWithin] with x ⟨w, hwFN, hwball⟩ hx_s + obtain ⟨v, hvf, hvw⟩ := ((mem_hausdorffEntourage U (f x) (F N x)).mp (hN x hx_s)).2 hwFN + exact ⟨v, hvf, hWsub <| hU₁comp + ⟨w, hUcomp ⟨z₀, hz₀y₀, hU'sub hwball⟩, hU_le_U₁ (hUsym.symm _ _ hvw)⟩⟩ + +/-- If a net of upper hemicontinuous set-valued functions converges uniformly +(along a filter `l`) in the Hausdorff uniformity to a set-valued function `f` with +compact values, then `f` is upper hemicontinuous -/ +theorem TendstoUniformlyOn.upperHemicontinuousOn (htendsto : TendstoUniformlyOn F f l s) + (hF : ∀ n, UpperHemicontinuousOn (F n) s) (hf_compact : ∀ x ∈ s, IsCompact (f x)) : + UpperHemicontinuousOn f s := by + -- A function `f` is upper hemicontinuous at `x₀` if for all open `u` with `f x₀ ⊆ u`, then + -- `f x ⊆ u` for all `x` near `x₀` + rw [upperHemicontinuousOn_iff_forall_isOpen] + intro x₀ hx₀s u hu hx₀u + -- Find an open entourage `U` such that `U ○ U.symm ⊆ u` + obtain ⟨W, hW, _, hWu⟩ := lebesgue_number_of_compact_open (hf_compact x₀ hx₀s) hu hx₀u + obtain ⟨V, hV, hVsym, hVcomp⟩ := comp_symm_mem_uniformity_sets hW + obtain ⟨U, ⟨hUmem, hUopen⟩, hUsub⟩ := uniformity_hasBasis_open.mem_iff.mp hV + -- Then choose a sufficiently large `N` such that `⟨f x, F N x⟩ ∈ hausdorffEntourage U` + -- for all `x ∈ s` + have hHU : hausdorffEntourage U ∈ @uniformity _ (UniformSpace.hausdorff (α := β)) := + (mem_lift'_sets monotone_hausdorffEntourage).mpr ⟨U, hUmem, le_refl _⟩ + obtain ⟨N, hN⟩ := (htendsto (hausdorffEntourage U) hHU).exists + have hFN_image : F N x₀ ⊆ U.image (f x₀) := ((mem_hausdorffEntourage ..).mp (hN x₀ hx₀s)).2 + -- Upper hemicontinuity implies `F N x ⊆ U.image (f x₀)` for `x` near `x₀` + simp_rw [upperHemicontinuousOn_iff] at hF + have hFN_uhc : ∀ᶠ x in 𝓝[s] x₀, F N x ⊆ U.image (f x₀) := + (hF N x₀ hx₀s).forall_isOpen _ hUopen.relImage hFN_image + -- For such a nearby `x`, show `f x ⊆ u` by taking `y ∈ f x`, + filter_upwards [hFN_uhc, self_mem_nhdsWithin] with x hFNx hx_s + intro y hy + -- finding a `z ∈ F N x` such that `(y, z) ∈ U` and then some `y₀ ∈ f x₀` such that `⟨y₀, z⟩ ∈ U` + obtain ⟨z, hzFN, hyz⟩ := ((mem_hausdorffEntourage U (f x) (F N x)).mp (hN x hx_s)).1 hy + obtain ⟨y₀, hy₀f, hy₀z⟩ := hFNx hzFN + -- then use that `U ○ U.symm ⊆ u` to conclude + exact hWu y₀ hy₀f (hVcomp ⟨z, hUsub hy₀z, hVsym.symm _ _ (hUsub hyz)⟩) + +/-- A net of lower hemicontinuous set-valued functions converging uniformly (along a +filter `l`) in the Hausdorff uniformity has a lower hemicontinuous limit -/ +theorem TendstoUniformly.lowerHemicontinuous (htendsto : TendstoUniformly F f l) + (hF : ∀ n, LowerHemicontinuous (F n)) : LowerHemicontinuous f := by + rw [← lowerHemicontinuousOn_univ_iff] + exact htendsto.tendstoUniformlyOn.lowerHemicontinuousOn (fun n ↦ (hF n).lowerHemicontinuousOn _) + +/-- If a net of upper hemicontinuous set-valued functions converges uniformly +(along a filter `l`) in the Hausdorff uniformity to a set-valued function `f` with +compact values, then `f` is upper hemicontinuous -/ +theorem TendstoUniformly.upperHemicontinuous (htendsto : TendstoUniformly F f l) + (hF : ∀ n, UpperHemicontinuous (F n)) (hf_compact : ∀ x, IsCompact (f x)) : + UpperHemicontinuous f := by + rw [← upperHemicontinuousOn_univ_iff] + exact htendsto.tendstoUniformlyOn.upperHemicontinuousOn + (fun n ↦ (hF n).upperHemicontinuousOn _) (fun x _ ↦ hf_compact x) + +end limits From 51e6992efd06126df61a496bebf8f49482a4e129 Mon Sep 17 00:00:00 2001 From: Garmelon <11077553+Garmelon@users.noreply.github.com> Date: Mon, 3 Aug 2026 14:29:46 +0000 Subject: [PATCH 10/16] chore: bump toolchain to v4.33.0-rc2 (#42401) Co-authored-by: Joscha --- lake-manifest.json | 18 +++++++++--------- lean-toolchain | 2 +- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 71d2d1d50d..1f8331b1fe 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0", + "rev": "123d15766ba49356c02ebad2a4462dfe12d79899", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0498c7c070c143a3bf7379f4d99a2c63bb9d9715", + "rev": "f5c090429dff3cf66cb65562526c9ea6e8edfbcb", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "18a90119a5d316358fde6c86e0ca24e59212e32c", + "rev": "bb3469a87774349fe01898d8bf2fc6a1ce6411ca", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b1436dc749e722c9920036b52cdc43b3451d0b69", + "rev": "222c58dad7706a6e7cae46c0edd65ea881d3ee27", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "57d3325be72a842920813bcb40f96a6f7393c185", + "rev": "7db8190085343afde2f5d2cdcc9bac719b6ec02c", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d", + "rev": "ef42f8944eaf5b6cbfbe75d1917d824c7dd6cf33", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0ecf8993df88c044962426c2cbca0de5717d6150", + "rev": "76e1c118b0700b4ceafe99532e887d6431625e1a", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,10 +75,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "da07ca808b6718cb2aed14dba154e5a08b8f8ecf", + "rev": "1319485273bf87833fa472afbcefdedecb16b45f", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0-rc1", + "inputRev": "v4.33.0-rc2", "inherited": true, "configFile": "lakefile.toml"}], "name": "mathlib", diff --git a/lean-toolchain b/lean-toolchain index fd85b262bf..c084c7fbe5 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0-rc1 +leanprover/lean4:v4.33.0-rc2 From 8cbb95e6e08446476813711ab8f45e59d4fda94d Mon Sep 17 00:00:00 2001 From: "mathlib-update-dependencies[bot]" <258990618+mathlib-update-dependencies[bot]@users.noreply.github.com> Date: Mon, 3 Aug 2026 15:25:41 +0000 Subject: [PATCH 11/16] chore: update Mathlib dependencies 2026-08-03 (#42403) This PR updates the Mathlib dependencies. From a89f32337e6e90d086e57fb05e6faa29ea288a80 Mon Sep 17 00:00:00 2001 From: Weiyi Wang Date: Mon, 3 Aug 2026 20:51:17 +0000 Subject: [PATCH 12/16] feat(Topology/InfiniteSum): non-negativity of tprod (#42184) --- Mathlib/Algebra/BigOperators/Finprod.lean | 4 ++-- .../Topology/Algebra/InfiniteSum/Order.lean | 19 +++++++++++++++++++ 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Finprod.lean b/Mathlib/Algebra/BigOperators/Finprod.lean index 1619e29b84..c6a54e4366 100644 --- a/Mathlib/Algebra/BigOperators/Finprod.lean +++ b/Mathlib/Algebra/BigOperators/Finprod.lean @@ -256,8 +256,8 @@ theorem finprod_induction {f : α → M} (p : M → Prop) (hp₀ : p 1) split_ifs exacts [Finset.prod_induction _ _ hp₁ hp₀ fun i _ => hp₂ _, hp₀] -theorem finprod_nonneg {R : Type*} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] - {f : α → R} (hf : ∀ x, 0 ≤ f x) : +theorem finprod_nonneg {R : Type*} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] + [PosMulMono R] {f : α → R} (hf : ∀ x, 0 ≤ f x) : 0 ≤ ∏ᶠ x, f x := finprod_induction (fun x => 0 ≤ x) zero_le_one (fun _ _ => mul_nonneg) hf diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Order.lean b/Mathlib/Topology/Algebra/InfiniteSum/Order.lean index c12a5cce20..b4f1deac69 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Order.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Order.lean @@ -234,6 +234,25 @@ protected theorem Multipliable.one_lt_tprod [L.LeAtTop] [L.NeBot] (hsum : Multip end OrderedCommGroup +section WithZero + +variable [CommMonoidWithZero α] [TopologicalSpace α] [Preorder α] [ZeroLEOneClass α] + [PosMulMono α] [ClosedIciTopology α] + +theorem HasProd.nonneg [L.NeBot] {f : ι → α} (hf : ∀ i, 0 ≤ f i) {a : α} (h : HasProd f a L) : + 0 ≤ a := + ge_of_tendsto' h fun s ↦ s.prod_nonneg fun i _ ↦ hf i + +theorem tprod_nonneg {f : ι → α} (hf : ∀ i, 0 ≤ f i) : + 0 ≤ ∏'[L] x, f x := by + by_cases h : Multipliable f L + · by_cases hbot : L.NeBot + · exact h.hasProd.nonneg hf + · simpa [tprod_bot hbot] using finprod_nonneg hf + · simp [tprod_eq_one_of_not_multipliable h] + +end WithZero + section CanonicallyOrderedMul variable [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] From 17d24e4dd354e256108f135211c73430e6b1e771 Mon Sep 17 00:00:00 2001 From: TJHeeringa <16029718+TJHeeringa@users.noreply.github.com> Date: Mon, 3 Aug 2026 21:26:50 +0000 Subject: [PATCH 13/16] refactor(Algebra/Module/Equiv): update name and refactor API ofLinearEquiv (#40865) Change the name of `LinearEquiv.ofLinear` to `LinearEquiv.ofLinearMap` and change the API. This replaces `_apply` by `coe_`, introduces `_symm`, which makes `_symm_apply` and `_symm_toLinearMap` redundant, and changes `_toLinearMap` to `toLinearMap_`. --- Mathlib/Algebra/Category/ModuleCat/Basic.lean | 2 +- Mathlib/Algebra/Category/ModuleCat/Semi.lean | 2 +- Mathlib/Algebra/Colimit/Module.lean | 4 +- Mathlib/Algebra/Module/CharacterModule.lean | 4 +- Mathlib/Algebra/Module/Equiv/Basic.lean | 39 +++++++++++++------ .../Algebra/Module/Presentation/Basic.lean | 4 +- Mathlib/Algebra/Star/Module.lean | 2 +- .../Normed/Operator/LinearIsometry.lean | 2 +- Mathlib/LinearAlgebra/Contraction.lean | 4 +- .../DirectSum/TensorProduct.lean | 2 +- Mathlib/LinearAlgebra/Dual/Lemmas.lean | 2 +- .../LinearAlgebra/ExteriorPower/Basic.lean | 34 ++++++++-------- .../Finsupp/LinearCombination.lean | 2 +- .../Matrix/SpecialLinearGroup.lean | 2 +- .../LinearAlgebra/Multilinear/DFinsupp.lean | 2 +- Mathlib/LinearAlgebra/Pi.lean | 2 +- .../LinearAlgebra/PiTensorProduct/Basic.lean | 13 ++++--- .../PiTensorProduct/DFinsupp.lean | 2 +- .../LinearAlgebra/PiTensorProduct/Dual.lean | 2 +- Mathlib/LinearAlgebra/Projection.lean | 2 +- Mathlib/LinearAlgebra/Quotient/Basic.lean | 2 +- .../TensorProduct/Associator.lean | 11 ++++-- .../LinearAlgebra/TensorProduct/Basic.lean | 2 +- .../TensorProduct/DirectLimit.lean | 2 +- .../TensorProduct/Graded/External.lean | 4 +- Mathlib/LinearAlgebra/TensorProduct/Map.lean | 2 +- Mathlib/LinearAlgebra/TensorProduct/Pi.lean | 4 +- Mathlib/LinearAlgebra/TensorProduct/Prod.lean | 2 +- .../LinearAlgebra/TensorProduct/Quotient.lean | 2 +- .../TensorProduct/Subalgebra.lean | 2 +- .../TensorProduct/Submodule.lean | 4 +- .../LinearAlgebra/TensorProduct/Tower.lean | 10 ++--- Mathlib/LinearAlgebra/Trace.lean | 2 +- .../RepresentationTheory/Coinvariants.lean | 6 +-- Mathlib/RepresentationTheory/FiniteIndex.lean | 2 +- .../Homological/GroupHomology/LowDegree.lean | 2 +- .../AdicCompletion/AsTensorProduct.lean | 2 +- .../AdicCompletion/Functoriality.lean | 4 +- .../RingTheory/Extension/Cotangent/Basis.lean | 2 +- Mathlib/RingTheory/Flat/Equalizer.lean | 4 +- Mathlib/RingTheory/IsTensorProduct.lean | 2 +- Mathlib/RingTheory/Localization/Module.lean | 4 +- Mathlib/RingTheory/MatrixAlgebra.lean | 2 +- Mathlib/RingTheory/PicardGroup.lean | 4 +- 44 files changed, 114 insertions(+), 97 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index 9965a3a3fd..2688ce98df 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -287,7 +287,7 @@ variable {X Y : ModuleCat R} /-- Build a `LinearEquiv` from an isomorphism in the category `ModuleCat R`. -/ def toLinearEquiv (i : X ≅ Y) : X ≃ₗ[R] Y := - .ofLinear i.hom.hom i.inv.hom (by aesop) (by aesop) + .ofLinearMap i.hom.hom i.inv.hom (by aesop) (by aesop) @[simp] lemma toLinearEquiv_apply (i : X ≅ Y) (x : X) : i.toLinearEquiv x = i.hom x := rfl @[simp] lemma toLinearEquiv_symm (i : X ≅ Y) : i.toLinearEquiv.symm = i.symm.toLinearEquiv := rfl diff --git a/Mathlib/Algebra/Category/ModuleCat/Semi.lean b/Mathlib/Algebra/Category/ModuleCat/Semi.lean index 13ac4f283f..d2a9e36b3f 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Semi.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Semi.lean @@ -263,7 +263,7 @@ namespace CategoryTheory.Iso /-- Build a `LinearEquiv` from an isomorphism in the category `SemimoduleCat R`. -/ def toLinearEquivₛ {X Y : SemimoduleCat R} (i : X ≅ Y) : X ≃ₗ[R] Y := - LinearEquiv.ofLinear i.hom.hom i.inv.hom (by aesop) (by aesop) + LinearEquiv.ofLinearMap i.hom.hom i.inv.hom (by aesop) (by aesop) end CategoryTheory.Iso diff --git a/Mathlib/Algebra/Colimit/Module.lean b/Mathlib/Algebra/Colimit/Module.lean index 97586ab60c..9e4d148fa1 100644 --- a/Mathlib/Algebra/Colimit/Module.lean +++ b/Mathlib/Algebra/Colimit/Module.lean @@ -211,7 +211,7 @@ family of equivalences `eᵢ : Gᵢ ≅ G'ᵢ` such that `e ∘ f = f' ∘ e` in -/ def congr (e : (i : ι) → G i ≃ₗ[R] G' i) (he : ∀ i j h, e j ∘ₗ f i j h = f' i j h ∘ₗ e i) : DirectLimit G f ≃ₗ[R] DirectLimit G' f' := - LinearEquiv.ofLinear (map (e ·) he) + LinearEquiv.ofLinearMap (map (e ·) he) (map (fun i ↦ (e i).symm) fun i j h ↦ by rw [toLinearMap_symm_comp_eq, ← comp_assoc, he i, comp_assoc, comp_coe, symm_trans_self, refl_toLinearMap, comp_id]) @@ -242,7 +242,7 @@ open _root_.DirectLimit /-- The direct limit constructed as a quotient of the direct sum is isomorphic to the direct limit constructed as a quotient of the disjoint union. -/ def linearEquiv : DirectLimit G f ≃ₗ[R] _root_.DirectLimit G f := - .ofLinear + .ofLinearMap (lift _ _ _ _ (Module.of _ _ _ _) fun _ _ _ _ ↦ .symm <| eq_of_le ..) (Module.lift _ _ _ _ (of _ _ _ _) fun _ _ _ _ ↦ of_f ..) (by ext; simp) diff --git a/Mathlib/Algebra/Module/CharacterModule.lean b/Mathlib/Algebra/Module/CharacterModule.lean index 74223e75f9..2cf6f59f89 100644 --- a/Mathlib/Algebra/Module/CharacterModule.lean +++ b/Mathlib/Algebra/Module/CharacterModule.lean @@ -108,7 +108,7 @@ lemma dual_surjective_of_injective (f : A →ₗ[R] B) (hf : Function.Injective Two isomorphic modules have isomorphic character modules. -/ def congr (e : A ≃ₗ[R] B) : CharacterModule A ≃ₗ[R] CharacterModule B := - .ofLinear (dual e.symm) (dual e) + .ofLinearMap (dual e.symm) (dual e) (by ext c _; exact congr(c $(e.right_inv _))) (by ext c _; exact congr(c $(e.left_inv _))) @@ -144,7 +144,7 @@ Linear maps into a character module are exactly characters of the tensor product -/ @[simps!] noncomputable def homEquiv : (A →ₗ[R] CharacterModule B) ≃ₗ[R] CharacterModule (A ⊗[R] B) := - .ofLinear uncurry curry (by ext _ z; refine z.induction_on ?_ ?_ ?_ <;> aesop) (by aesop) + .ofLinearMap uncurry curry (by ext _ z; refine z.induction_on ?_ ?_ ?_ <;> aesop) (by aesop) theorem dual_rTensor_conj_homEquiv (f : A →ₗ[R] A') : homEquiv.symm.toLinearMap ∘ₗ dual (f.rTensor B) ∘ₗ homEquiv.toLinearMap = f.lcomp R _ := rfl diff --git a/Mathlib/Algebra/Module/Equiv/Basic.lean b/Mathlib/Algebra/Module/Equiv/Basic.lean index 566923c75a..93a26c2d2e 100644 --- a/Mathlib/Algebra/Module/Equiv/Basic.lean +++ b/Mathlib/Algebra/Module/Equiv/Basic.lean @@ -481,25 +481,40 @@ variable (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) /-- If a linear map has an inverse, it is a linear equivalence. -/ -def ofLinear (h₁ : f.comp g = LinearMap.id) (h₂ : g.comp f = LinearMap.id) : M ≃ₛₗ[σ₁₂] M₂ := - { f with - invFun := g - left_inv := LinearMap.ext_iff.1 h₂ - right_inv := LinearMap.ext_iff.1 h₁ } +def ofLinearMap (h₁ : f.comp g = .id) (h₂ : g.comp f = .id) : M ≃ₛₗ[σ₁₂] M₂ where + __ := f + invFun := g + left_inv := LinearMap.ext_iff.1 h₂ + right_inv := LinearMap.ext_iff.1 h₁ -@[simp] +@[simp low] +theorem coe_ofLinearMap (h₁ h₂) : ⇑(ofLinearMap f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) = f := rfl + +@[simp low] +theorem symm_ofLinearMap (h₁ h₂) : + (ofLinearMap f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm = (ofLinearMap g f h₂ h₁) := + rfl + +/-- If a linear map has an inverse, it is a linear equivalence. -/ +@[deprecated ofLinearMap (since := "2026-06-23")] +abbrev ofLinear (h₁ : f.comp g = .id) (h₂ : g.comp f = .id) : M ≃ₛₗ[σ₁₂] M₂ := ofLinearMap f g h₁ h₂ + +@[deprecated coe_ofLinearMap (since := "2026-06-23")] theorem ofLinear_apply {h₁ h₂} (x : M) : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) x = f x := rfl -@[simp] -theorem ofLinear_symm_apply {h₁ h₂} (x : M₂) : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm x = g x := +@[deprecated "Follows from simp lemmas `symm_ofLinearMap` and `coe_ofLinearMap`" + (since := "2026-06-23")] +theorem ofLinear_symm_apply {h₁ h₂} (x : M₂) : + (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm x = g x := rfl -@[simp] -theorem ofLinear_toLinearMap {h₁ h₂} : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) = f := rfl +@[deprecated "Follows from simp lemmas `symm_ofLinearMap` and `ofLinear_toLinearMap`" + (since := "2026-06-23")] +theorem ofLinear_symm_toLinearMap {h₁ h₂} : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm = g := rfl @[simp] -theorem ofLinear_symm_toLinearMap {h₁ h₂} : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm = g := rfl +theorem ofLinear_toLinearMap (h₁ h₂) : (ofLinearMap f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) = f := rfl end @@ -833,7 +848,7 @@ open LinearMap /-- Given an `R`-module `M` and an equivalence `m ≃ n` between arbitrary types, construct a linear equivalence `(n → M) ≃ₗ[R] (m → M)` -/ def funCongrLeft (e : m ≃ n) : (n → M) ≃ₗ[R] m → M := - LinearEquiv.ofLinear (funLeft R M e) (funLeft R M e.symm) + LinearEquiv.ofLinearMap (funLeft R M e) (funLeft R M e.symm) (LinearMap.ext fun x ↦ funext fun i ↦ by rw [id_apply, ← funLeft_comp, Equiv.symm_comp_self, LinearMap.funLeft_id]) (LinearMap.ext fun x ↦ diff --git a/Mathlib/Algebra/Module/Presentation/Basic.lean b/Mathlib/Algebra/Module/Presentation/Basic.lean index 4f372e7e6e..11b5b38e1e 100644 --- a/Mathlib/Algebra/Module/Presentation/Basic.lean +++ b/Mathlib/Algebra/Module/Presentation/Basic.lean @@ -364,7 +364,7 @@ variable {solution' : relations.Solution N} (h' : solution'.IsPresentation) /-- Uniqueness (up to a unique linear equivalence) of the module defined by generators and relations. -/ -def uniq : M ≃ₗ[A] N := LinearEquiv.ofLinear +def uniq : M ≃ₗ[A] N := LinearEquiv.ofLinearMap (h.desc solution') (h'.desc solution) (h'.postcomp_injective (by simp)) (h.postcomp_injective (by simp)) @@ -459,7 +459,7 @@ lemma isPresentation {solution : relations.Solution M} solution.IsPresentation where bijective := by let e : relations.Quotient ≃ₗ[A] M := - LinearEquiv.ofLinear solution.fromQuotient + LinearEquiv.ofLinearMap solution.fromQuotient ((down.{v} h).desc (ofQuotient relations)) ((down.{max u w₀} h).postcomp_injective (by aesop)) (by aesop) exact e.bijective diff --git a/Mathlib/Algebra/Star/Module.lean b/Mathlib/Algebra/Star/Module.lean index 3d5047d908..928ae94243 100644 --- a/Mathlib/Algebra/Star/Module.lean +++ b/Mathlib/Algebra/Star/Module.lean @@ -221,7 +221,7 @@ set_option backward.isDefEq.respectTransparency false in as a linear equivalence. -/ @[simps!] def StarModule.decomposeProdAdjoint : A ≃ₗ[R] selfAdjoint A × skewAdjoint A := by - refine LinearEquiv.ofLinear ((selfAdjointPart R).prod (skewAdjointPart R)) + refine LinearEquiv.ofLinearMap ((selfAdjointPart R).prod (skewAdjointPart R)) (LinearMap.coprod ((selfAdjoint.submodule R A).subtype) (skewAdjoint.submodule R A).subtype) ?_ (LinearMap.ext <| StarModule.selfAdjointPart_add_skewAdjointPart R) -- Note: with https://github.com/leanprover-community/mathlib4/pull/6965 `Submodule.coe_subtype` doesn't fire in `dsimp` or `simp` diff --git a/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean b/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean index fc839187ae..db0ab09034 100644 --- a/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean +++ b/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean @@ -962,7 +962,7 @@ theorem coe_ofSurjective (f : F →ₛₗᵢ[σ₁₂] E₂) (hfr : Function.Sur def ofLinearIsometry (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E) (h₁ : f.toLinearMap.comp g = LinearMap.id) (h₂ : g.comp f.toLinearMap = LinearMap.id) : E ≃ₛₗᵢ[σ₁₂] E₂ := - { toLinearEquiv := LinearEquiv.ofLinear f.toLinearMap g h₁ h₂ + { toLinearEquiv := LinearEquiv.ofLinearMap f.toLinearMap g h₁ h₂ norm_map' := fun x => f.norm_map x } @[simp] diff --git a/Mathlib/LinearAlgebra/Contraction.lean b/Mathlib/LinearAlgebra/Contraction.lean index 417f29cd82..d6a838fd4b 100644 --- a/Mathlib/LinearAlgebra/Contraction.lean +++ b/Mathlib/LinearAlgebra/Contraction.lean @@ -168,7 +168,7 @@ attribute [-ext] AlgebraTensorModule.curry_injective in provides this equivalence in return for a basis of `M`. -/ -- We manually create simp-lemmas because `@[simps]` generates a malformed lemma noncomputable def dualTensorHomEquivOfBasis : Module.Dual R M ⊗[R] N ≃ₗ[R] M →ₗ[R] N := - LinearEquiv.ofLinear (dualTensorHom R M N) + LinearEquiv.ofLinearMap (dualTensorHom R M N) (∑ i, TensorProduct.mk R _ N (b.dualBasis i) ∘ₗ (LinearMap.applyₗ (R := R) (b i))) (by ext f m @@ -446,7 +446,7 @@ isomorphism `R ⊗ R ≃ R`. @[simps!] noncomputable def dualDistribEquivOfBasis (b : Basis ι R M) (c : Basis κ R N) : Dual R M ⊗[R] Dual R N ≃ₗ[R] Dual R (M ⊗[R] N) := by - refine LinearEquiv.ofLinear (dualDistrib R M N) (dualDistribInvOfBasis b c) ?_ ?_ + refine LinearEquiv.ofLinearMap (dualDistrib R M N) (dualDistribInvOfBasis b c) ?_ ?_ · exact dualDistrib_dualDistribInvOfBasis_left_inverse _ _ · exact dualDistrib_dualDistribInvOfBasis_right_inverse _ _ diff --git a/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean b/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean index 10d530acea..374a08ed1f 100644 --- a/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean @@ -49,7 +49,7 @@ variable [Module S M₁'] [IsScalarTower R S M₁'] "tensor product distributes over direct sum". -/ protected def directSum : ((⨁ i₁, M₁ i₁) ⊗[R] ⨁ i₂, M₂ i₂) ≃ₗ[S] ⨁ i : ι₁ × ι₂, M₁ i.1 ⊗[R] M₂ i.2 := by - refine LinearEquiv.ofLinear ?toFun ?invFun ?left ?right + refine LinearEquiv.ofLinearMap ?toFun ?invFun ?left ?right · exact AlgebraTensorModule.lift <| toModule S _ _ fun i₁ => flip <| toModule R _ _ fun i₂ => flip <| AlgebraTensorModule.curry <| DirectSum.lof S (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂) diff --git a/Mathlib/LinearAlgebra/Dual/Lemmas.lean b/Mathlib/LinearAlgebra/Dual/Lemmas.lean index 0d17ea7dce..580046e923 100644 --- a/Mathlib/LinearAlgebra/Dual/Lemmas.lean +++ b/Mathlib/LinearAlgebra/Dual/Lemmas.lean @@ -620,7 +620,7 @@ vanish on `W`. The inverse of this is `Submodule.dualCopairing`. -/ def dualQuotEquivDualAnnihilator (W : Submodule R M) : Module.Dual R (M ⧸ W) ≃ₗ[R] W.dualAnnihilator := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap (W.mkQ.dualMap.codRestrict W.dualAnnihilator fun φ => W.range_dualMap_mkQ_eq ▸ LinearMap.mem_range_self W.mkQ.dualMap φ) W.dualCopairing (by ext; rfl) (by ext; rfl) diff --git a/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean b/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean index eacd609d23..d2a91ef943 100644 --- a/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean +++ b/Mathlib/LinearAlgebra/ExteriorPower/Basic.lean @@ -412,8 +412,7 @@ variable (R M) in /-- The linear equivalence ` ⋀[R]^0 M ≃ₗ[R] R`. -/ @[simps! -isSimp symm_apply] noncomputable def zeroEquiv : ⋀[R]^0 M ≃ₗ[R] R := - LinearEquiv.ofLinear - (alternatingMapLinearEquiv (AlternatingMap.constOfIsEmpty R _ _ 1)) + .ofLinearMap (alternatingMapLinearEquiv (AlternatingMap.constOfIsEmpty R _ _ 1)) { toFun := fun r ↦ r • (ιMulti _ _ (by rintro ⟨i, hi⟩; simp at hi)) map_add' := by intros; simp only [add_smul] map_smul' := by intros; simp only [smul_eq_mul, mul_smul, RingHom.id_apply] } @@ -431,22 +430,21 @@ variable (R M) in /-- The linear equivalence `M ≃ₗ[R] ⋀[R]^1 M`. -/ @[simps! -isSimp symm_apply] noncomputable def oneEquiv : ⋀[R]^1 M ≃ₗ[R] M := - LinearEquiv.ofLinear - (alternatingMapLinearEquiv (AlternatingMap.ofSubsingleton R M M (0 : Fin 1) .id)) (by - have h (m : M) : (fun (_ : Fin 1) ↦ m) = update (fun _ ↦ 0) 0 m := by - ext i - fin_cases i - rfl - exact - { toFun := fun m ↦ ιMulti _ _ (fun _ ↦ m) - map_add' := fun m₁ m₂ ↦ by - rw [h]; nth_rw 2 [h]; nth_rw 3 [h] - simp only [Fin.isValue, AlternatingMap.map_update_add] - map_smul' := fun r m ↦ by - dsimp - rw [h]; nth_rw 2 [h] - simp only [Fin.isValue, AlternatingMap.map_update_smul] }) - (by aesop) (by aesop) + .ofLinearMap (alternatingMapLinearEquiv (AlternatingMap.ofSubsingleton R M M (0 : Fin 1) .id)) (by + have h (m : M) : (fun (_ : Fin 1) ↦ m) = update (fun _ ↦ 0) 0 m := by + ext i + fin_cases i + rfl + exact + { toFun := fun m ↦ ιMulti _ _ (fun _ ↦ m) + map_add' := fun m₁ m₂ ↦ by + rw [h]; nth_rw 2 [h]; nth_rw 3 [h] + simp only [Fin.isValue, AlternatingMap.map_update_add] + map_smul' := fun r m ↦ by + dsimp + rw [h]; nth_rw 2 [h] + simp only [Fin.isValue, AlternatingMap.map_update_smul] }) + (by aesop) (by aesop) @[simp] lemma oneEquiv_ιMulti (f : Fin 1 → M) : diff --git a/Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean b/Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean index 9b3442cd41..0b39c12123 100644 --- a/Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean +++ b/Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean @@ -530,7 +530,7 @@ variable {R M ι : Type*} [Ring R] [AddCommGroup M] [Module R M] (i : ι) (c : the `j`-th standard basis vector to itself plus `c j` multiplied with the `i`-th standard basis vector (in particular, the `i`-th standard basis vector is kept invariant). -/ def Finsupp.addSingleEquiv : (ι →₀ R) ≃ₗ[R] (ι →₀ R) := by - refine .ofLinear (linearCombination _ fun j ↦ single j 1 + single i (c j)) + refine .ofLinearMap (linearCombination _ fun j ↦ single j 1 + single i (c j)) (linearCombination _ fun j ↦ single j 1 - single i (c j)) ?_ ?_ <;> ext j k <;> obtain rfl | hk := eq_or_ne i k · simp [h₀] diff --git a/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean b/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean index cbb6fad7f6..32864908ae 100644 --- a/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean +++ b/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean @@ -191,7 +191,7 @@ instance : Group (SpecialLinearGroup n R) := /-- A version of `Matrix.toLin' A` that produces linear equivalences. -/ def toLin' : SpecialLinearGroup n R →* (n → R) ≃ₗ[R] n → R where toFun A := - LinearEquiv.ofLinear (Matrix.toLin' ↑ₘA) (Matrix.toLin' ↑ₘA⁻¹) + LinearEquiv.ofLinearMap (Matrix.toLin' ↑ₘA) (Matrix.toLin' ↑ₘA⁻¹) (by rw [← toLin'_mul, ← coe_mul, mul_inv_cancel, coe_one, toLin'_one]) (by rw [← toLin'_mul, ← coe_mul, inv_mul_cancel, coe_one, toLin'_one]) map_one' := LinearEquiv.toLinearMap_injective Matrix.toLin'_one diff --git a/Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean b/Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean index c246005765..18309fef90 100644 --- a/Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean +++ b/Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean @@ -208,7 +208,7 @@ on the `fun i ↦ M i (p i)` and the space of multilinear map on `fun i ↦ Π def fromDFinsuppEquiv : ((p : Π i, κ i) → MultilinearMap R (fun i ↦ M i (p i)) N) ≃ₗ[R] MultilinearMap R (fun i ↦ Π₀ j : κ i, M i j) N := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap ((DFinsupp.lsum ℕ fun _ ↦ .id).compMultilinearMapₗ R ∘ₗ MultilinearMap.dfinsuppFamilyₗ) (LinearMap.pi fun p ↦ MultilinearMap.compLinearMapₗ fun i ↦ DFinsupp.lsingle (p i)) (by ext f x; simp) diff --git a/Mathlib/LinearAlgebra/Pi.lean b/Mathlib/LinearAlgebra/Pi.lean index 6d3599687b..cb62852d4d 100644 --- a/Mathlib/LinearAlgebra/Pi.lean +++ b/Mathlib/LinearAlgebra/Pi.lean @@ -303,7 +303,7 @@ def iInfKerProjEquiv {I J : Set ι} [DecidablePred fun i => i ∈ I] (hd : Disjo (⨅ i ∈ J, ker (proj i : ((i : ι) → φ i) →ₗ[R] φ i) : Submodule R ((i : ι) → φ i)) ≃ₗ[R] (i : I) → φ i := by refine - LinearEquiv.ofLinear (pi fun i => (proj (i : ι)).comp (Submodule.subtype _)) + LinearEquiv.ofLinearMap (pi fun i => (proj (i : ι)).comp (Submodule.subtype _)) (codRestrict _ (pi fun i => if h : i ∈ I then proj (⟨i, h⟩ : I) else 0) ?_) ?_ ?_ · intro b simp only [mem_iInf, mem_ker, proj_apply, pi_apply] diff --git a/Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean b/Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean index 30f274638e..b6900cd03e 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean @@ -599,7 +599,7 @@ This is the n-ary version of `TensorProduct.congr` -/ noncomputable def congr (f : Π i, s i ≃ₗ[R] t i) : (⨂[R] i, s i) ≃ₗ[R] ⨂[R] i, t i := - .ofLinear + .ofLinearMap (map (fun i ↦ f i)) (map (fun i ↦ (f i).symm)) (by ext; simp) @@ -608,12 +608,13 @@ noncomputable def congr (f : Π i, s i ≃ₗ[R] t i) : @[simp] theorem congr_tprod (f : Π i, s i ≃ₗ[R] t i) (m : Π i, s i) : congr f (tprod R m) = tprod R (fun (i : ι) ↦ (f i) (m i)) := by - simp only [congr, LinearEquiv.ofLinear_apply, map_tprod, LinearEquiv.coe_coe] + simp only [congr, LinearEquiv.coe_ofLinearMap, map_tprod, LinearEquiv.coe_coe] @[simp] theorem congr_symm_tprod (f : Π i, s i ≃ₗ[R] t i) (p : Π i, t i) : (congr f).symm (tprod R p) = tprod R (fun (i : ι) ↦ (f i).symm (p i)) := by - simp only [congr, LinearEquiv.ofLinear_symm_apply, map_tprod, LinearEquiv.coe_coe] + simp only [congr, LinearEquiv.symm_ofLinearMap, LinearEquiv.coe_ofLinearMap, map_tprod, + LinearEquiv.coe_coe] /-- Let `sᵢ`, `tᵢ` and `t'ᵢ` be families of `R`-modules, then `f : Πᵢ sᵢ → tᵢ → t'ᵢ` induces an @@ -680,7 +681,7 @@ variable (s) in def reindex (e : ι ≃ ι₂) : (⨂[R] i : ι, s i) ≃ₗ[R] ⨂[R] i : ι₂, s (e.symm i) := let f := domDomCongrLinearEquiv' R R s (⨂[R] (i : ι₂), s (e.symm i)) e let g := domDomCongrLinearEquiv' R R s (⨂[R] (i : ι), s i) e - LinearEquiv.ofLinear (lift <| f.symm <| tprod R) (lift <| g <| tprod R) (by aesop) (by aesop) + LinearEquiv.ofLinearMap (lift <| f.symm <| tprod R) (lift <| g <| tprod R) (by aesop) (by aesop) end @@ -805,7 +806,7 @@ variable [Subsingleton ι] (i₀ : ι) /-- Tensor product over a singleton type with element `i₀` is equivalent to `s i₀`. -/ def subsingletonEquiv : (⨂[R] i : ι, s i) ≃ₗ[R] s i₀ := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap (lift { toFun f := f i₀ map_update_add' m i := by rw [Subsingleton.elim i i₀]; simp @@ -845,7 +846,7 @@ set_option backward.isDefEq.respectTransparency false in modules, use the non-dependent version `PiTensorProduct.tmulEquiv` instead. -/ def tmulEquivDep : (⨂[R] i₁, N (.inl i₁)) ⊗[R] (⨂[R] i₂, N (.inr i₂)) ≃ₗ[R] ⨂[R] i, N i := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap (TensorProduct.lift { toFun a := PiTensorProduct.lift (PiTensorProduct.lift (MultilinearMap.currySumEquiv (tprod R)) a) diff --git a/Mathlib/LinearAlgebra/PiTensorProduct/DFinsupp.lean b/Mathlib/LinearAlgebra/PiTensorProduct/DFinsupp.lean index 88c01be991..a42f94413b 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct/DFinsupp.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct/DFinsupp.lean @@ -33,7 +33,7 @@ variable {R ι : Type*} {κ : ι → Type*} {M : (i : ι) → κ i → Type*} /-- The `ι`-ary tensor product distributes over `κ i`-ary finitely supported functions. -/ def ofDFinsuppEquiv : (⨂[R] i, (Π₀ j : κ i, M i j)) ≃ₗ[R] Π₀ p : Π i, κ i, ⨂[R] i, M i (p i) := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap (lift <| MultilinearMap.fromDFinsuppEquiv κ R fun p ↦ (DFinsupp.lsingle p).compMultilinearMap (tprod R)) (DFinsupp.lsum R fun p ↦ lift <| diff --git a/Mathlib/LinearAlgebra/PiTensorProduct/Dual.lean b/Mathlib/LinearAlgebra/PiTensorProduct/Dual.lean index eb6fc3f8c9..d94e560f27 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct/Dual.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct/Dual.lean @@ -104,7 +104,7 @@ isomorphism `⨂[R] i, R ≃ R` given by multiplication (`constantBaseRingEquiv` @[simps!] noncomputable def dualDistribEquivOfBasis [Finite ι] [∀ i, Finite (κ i)] (b : Π i, Basis (κ i) R (M i)) : (⨂[R] i, Dual R (M i)) ≃ₗ[R] Dual R (⨂[R] i, M i) := - LinearEquiv.ofLinear dualDistrib (dualDistribInvOfBasis b) + LinearEquiv.ofLinearMap dualDistrib (dualDistribInvOfBasis b) (dualDistrib_dualDistribInvOfBasis_left_inverse _) (dualDistrib_dualDistribInvOfBasis_right_inverse _) diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index ce2883ee8f..04b8f4e112 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -286,7 +286,7 @@ to its projection onto `q` along `p`; the backward direction sends an element of in `M ⧸ p`. -/ @[simps! symm_apply] def quotientEquivOfIsCompl (h : IsCompl p q) : (E ⧸ p) ≃ₗ[R] q := - .ofLinear + .ofLinearMap (p.liftQ (q.projectionOnto p h.symm) (by simp)) (p.mkQ ∘ₗ q.subtype) (by ext; simp) diff --git a/Mathlib/LinearAlgebra/Quotient/Basic.lean b/Mathlib/LinearAlgebra/Quotient/Basic.lean index 261bc284bc..d7616ee73d 100644 --- a/Mathlib/LinearAlgebra/Quotient/Basic.lean +++ b/Mathlib/LinearAlgebra/Quotient/Basic.lean @@ -404,7 +404,7 @@ variable (p p' : Submodule R M) /-- If `p = ⊥`, then `M / p ≃ₗ[R] M`. -/ def quotEquivOfEqBot (hp : p = ⊥) : (M ⧸ p) ≃ₗ[R] M := - LinearEquiv.ofLinear (p.liftQ id <| hp.symm ▸ bot_le) p.mkQ (liftQ_mkQ _ _ _) <| + LinearEquiv.ofLinearMap (p.liftQ id <| hp.symm ▸ bot_le) p.mkQ (liftQ_mkQ _ _ _) <| p.quot_hom_ext _ LinearMap.id fun _ => rfl @[simp] diff --git a/Mathlib/LinearAlgebra/TensorProduct/Associator.lean b/Mathlib/LinearAlgebra/TensorProduct/Associator.lean index 7bb8c73ec4..7f9e9738aa 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Associator.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Associator.lean @@ -39,7 +39,10 @@ variable (R M) /-- The base ring is a left identity for the tensor product of modules, up to linear equivalence. -/ protected def lid : R ⊗[R] M ≃ₗ[R] M := - LinearEquiv.ofLinear (lift <| LinearMap.lsmul R M) (mk R R M 1) (LinearMap.ext fun _ => by simp) + LinearEquiv.ofLinearMap + (lift <| LinearMap.lsmul R M) + (mk R R M 1) + (LinearMap.ext fun _ => by simp) (ext' fun r m => by simp [← tmul_smul, ← smul_tmul, smul_eq_mul, mul_one]) end @@ -69,7 +72,7 @@ variable (R M) /-- The base ring is a right identity for the tensor product of modules, up to linear equivalence. -/ protected def rid : M ⊗[R] R ≃ₗ[R] M := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap (lift <| .flip (LinearMap.lsmul R M)) (mk R M R |>.flip 1) (LinearMap.ext <| one_smul _) @@ -142,7 +145,7 @@ variable (R M N P) attribute [local ext high] ext in /-- The associator for tensor product of R-modules, as a linear equivalence. -/ protected def assoc : M ⊗[R] N ⊗[R] P ≃ₗ[R] M ⊗[R] (N ⊗[R] P) := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap (lift <| lift <| lcurry _ _ _ _ ∘ₗ mk _ _ _) (lift <| uncurry _ _ _ _ ∘ₗ curry (mk R _ _)) (by ext; rfl) @@ -245,7 +248,7 @@ variable (M N P) in attribute [local ext high] ext in /-- A tensor product analogue of `mul_right_comm`. -/ def rightComm : M ⊗[R] N ⊗[R] P ≃ₗ[R] M ⊗[R] P ⊗[R] N := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap (lift (lift (LinearMap.lflip.toLinearMap ∘ₗ (mk _ _ _).compr₂ (mk _ _ _)))) (lift (lift (LinearMap.lflip.toLinearMap ∘ₗ (mk _ _ _).compr₂ (mk _ _ _)))) (by ext; rfl) (by ext; rfl) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean index 132f843798..d88d19595a 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean @@ -263,7 +263,7 @@ variable (R M N) /-- The tensor product of modules is commutative, up to linear equivalence. -/ protected def comm : M ⊗[R] N ≃ₗ[R] N ⊗[R] M := - LinearEquiv.ofLinear (lift (mk R N M).flip) (lift (mk R M N).flip) (ext' fun _ _ => rfl) + LinearEquiv.ofLinearMap (lift (mk R N M).flip) (lift (mk R M N).flip) (ext' fun _ _ => rfl) (ext' fun _ _ => rfl) @[simp] diff --git a/Mathlib/LinearAlgebra/TensorProduct/DirectLimit.lean b/Mathlib/LinearAlgebra/TensorProduct/DirectLimit.lean index 5e43b9eb9e..9ba33ac844 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/DirectLimit.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/DirectLimit.lean @@ -77,7 +77,7 @@ attribute [local ext] TensorProduct.ext in -/ noncomputable def directLimitLeft : DirectLimit G f ⊗[R] M ≃ₗ[R] DirectLimit (G · ⊗[R] M) (f ▷ M) := - LinearEquiv.ofLinear (toDirectLimit f M) (fromDirectLimit f M) (by ext; simp) (by ext; simp) + LinearEquiv.ofLinearMap (toDirectLimit f M) (fromDirectLimit f M) (by ext; simp) (by ext; simp) @[simp] lemma directLimitLeft_tmul_of {i : ι} (g : G i) (m : M) : directLimitLeft f M (of _ _ _ _ _ g ⊗ₜ m) = of _ _ _ (f ▷ M) _ (g ⊗ₜ m) := diff --git a/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean b/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean index b26fafbc83..1b7efccfcc 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean @@ -103,7 +103,7 @@ This sends $a ⊗ b$ to $(-1)^{\deg a' \deg b} (b ⊗ a)$. -/ def gradedComm : (⨁ i, 𝒜 i) ⊗[R] (⨁ i, ℬ i) ≃ₗ[R] (⨁ i, ℬ i) ⊗[R] (⨁ i, 𝒜 i) := by refine TensorProduct.directSum R R 𝒜 ℬ ≪≫ₗ ?_ ≪≫ₗ (TensorProduct.directSum R R ℬ 𝒜).symm - exact LinearEquiv.ofLinear (gradedCommAux _ _ _) (gradedCommAux _ _ _) + exact LinearEquiv.ofLinearMap (gradedCommAux _ _ _) (gradedCommAux _ _ _) (gradedCommAux_comp_gradedCommAux _ _ _) (gradedCommAux_comp_gradedCommAux _ _ _) /-- The braiding is symmetric. -/ @@ -115,7 +115,7 @@ theorem gradedComm_of_tmul_of (i j : ι) (a : 𝒜 i) (b : ℬ j) : gradedComm R 𝒜 ℬ (lof R _ 𝒜 i a ⊗ₜ lof R _ ℬ j b) = (-1 : ℤˣ) ^ (j * i) • (lof R _ ℬ _ b ⊗ₜ lof R _ 𝒜 _ a) := by rw [gradedComm] - dsimp only [LinearEquiv.trans_apply, LinearEquiv.ofLinear_apply] + dsimp only [LinearEquiv.trans_apply, LinearEquiv.coe_ofLinearMap] rw [TensorProduct.directSum_lof_tmul_lof, gradedCommAux_lof_tmul, Units.smul_def, -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 specialized `map_smul` to `LinearEquiv.map_smul` to avoid timeouts. ← Int.cast_smul_eq_zsmul R, LinearEquiv.map_smul, TensorProduct.directSum_symm_lof_tmul, diff --git a/Mathlib/LinearAlgebra/TensorProduct/Map.lean b/Mathlib/LinearAlgebra/TensorProduct/Map.lean index ac9e7ae0a5..60b3091201 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Map.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Map.lean @@ -246,7 +246,7 @@ variable {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomIn /-- If `M` and `P` are semilinearly equivalent and `N` and `Q` are semilinearly equivalent then `M ⊗ N` and `P ⊗ Q` are semilinearly equivalent. -/ def congr (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂) : M ⊗[R] N ≃ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂ := - LinearEquiv.ofLinear (map f g) (map f.symm g.symm) + LinearEquiv.ofLinearMap (map f g) (map f.symm g.symm) (ext' fun m n => by simp) (ext' fun m n => by simp) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Pi.lean b/Mathlib/LinearAlgebra/TensorProduct/Pi.lean index 781eed9016..406b79e518 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Pi.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Pi.lean @@ -89,7 +89,7 @@ private lemma piRightInv_single (x : N) (i : ι) (m : M i) : /-- Tensor product commutes with finite products on the right. -/ def piRight : N ⊗[R] (∀ i, M i) ≃ₗ[S] ∀ i, N ⊗[R] M i := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap (piRightHom R S N M) (piRightInv R S N M) (by ext i x m j; simp [tmul_single]) @@ -161,7 +161,7 @@ private lemma piScalarRightInv_single (x : N) (i : ι) : /-- For any `R`-module `N` and finite index type `ι`, `N ⊗[R] (ι → R)` is canonically isomorphic to `ι → N`. -/ def piScalarRight : N ⊗[R] (ι → R) ≃ₗ[S] (ι → N) := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap (piScalarRightHom R S N ι) (piScalarRightInv R S N ι) (by ext i x j; simp [Pi.single_apply]) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Prod.lean b/Mathlib/LinearAlgebra/TensorProduct/Prod.lean index ef54c68077..1a2225ab23 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Prod.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Prod.lean @@ -39,7 +39,7 @@ attribute [ext] TensorProduct.ext set_option backward.isDefEq.respectTransparency false in /-- Tensor products distribute over a product on the right. -/ def prodRight : M₁ ⊗[R] (M₂ × M₃) ≃ₗ[S] (M₁ ⊗[R] M₂) × (M₁ ⊗[R] M₃) := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap (TensorProduct.AlgebraTensorModule.lift <| LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ LinearMap.prod (AlgebraTensorModule.mk R S M₁ M₂) (AlgebraTensorModule.mk R S M₁ M₃)) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean index d0595a460f..b604a7a236 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean @@ -58,7 +58,7 @@ noncomputable def quotientTensorQuotientEquiv (m : Submodule R M) (n : Submodule (M ⊗[R] N) ⧸ (LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)) := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap (lift <| Submodule.liftQ _ (LinearMap.flip <| Submodule.liftQ _ ((mk R (M := M) (N := N)).flip.compr₂ (Submodule.mkQ _)) fun x hx => by ext y diff --git a/Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean b/Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean index b4f1a8718e..81bd5f8865 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean @@ -135,7 +135,7 @@ set_option backward.isDefEq.respectTransparency false in This is promoted to an `R`-algebra isomorphism `Algebra.TensorProduct.algEquivIncludeRange`. -/ def linearEquivIncludeRange : S ⊗[R] T ≃ₗ[R] (includeLeft : S →ₐ[R] S ⊗[R] T).range ⊗[R] - (includeRight : T →ₐ[R] S ⊗[R] T).range := .ofLinear + (includeRight : T →ₐ[R] S ⊗[R] T).range := .ofLinearMap (_root_.TensorProduct.map includeLeft.toLinearMap.rangeRestrict includeRight.toLinearMap.rangeRestrict) (includeLeft.toLinearMap.range.mulMap includeRight.toLinearMap.range) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean b/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean index cb790fb68c..2a3973c205 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean @@ -163,7 +163,7 @@ there is the natural isomorphism of `R`-modules between `i(R) ⊗[R] N` and `N` induced by multiplication in `S`, here `i : R → S` is the structure map. This generalizes `TensorProduct.lid` as `i(R)` is not necessarily isomorphic to `R`. -/ def lTensorOne : (⊥ : Subalgebra R S) ⊗[R] N ≃ₗ[R] N := - LinearEquiv.ofLinear N.lTensorOne' (TensorProduct.mk R (⊥ : Subalgebra R S) N 1) + LinearEquiv.ofLinearMap N.lTensorOne' (TensorProduct.mk R (⊥ : Subalgebra R S) N 1) (by ext; simp) <| TensorProduct.ext' fun r n ↦ by change 1 ⊗ₜ[R] lTensorOne' N _ = r ⊗ₜ[R] n obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2 @@ -215,7 +215,7 @@ there is the natural isomorphism of `R`-modules between `M ⊗[R] i(R)` and `M` induced by multiplication in `S`, here `i : R → S` is the structure map. This generalizes `TensorProduct.rid` as `i(R)` is not necessarily isomorphic to `R`. -/ def rTensorOne : M ⊗[R] (⊥ : Subalgebra R S) ≃ₗ[R] M := - LinearEquiv.ofLinear M.rTensorOne' ((TensorProduct.comm R _ _).toLinearMap ∘ₗ + LinearEquiv.ofLinearMap M.rTensorOne' ((TensorProduct.comm R _ _).toLinearMap ∘ₗ TensorProduct.mk R (⊥ : Subalgebra R S) M 1) (by ext; simp) <| TensorProduct.ext' fun n r ↦ by change rTensorOne' M _ ⊗ₜ[R] 1 = n ⊗ₜ[R] r obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2 diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean index 1a388d0358..07943192bd 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean @@ -161,7 +161,7 @@ A linear equivalence constructing a linear map `M ⊗[R] N →[A] P` given a bilinear map `M →[A] N →[R] P` with the property that its composition with the canonical bilinear map `M →[A] N →[R] M ⊗[R] N` is the given bilinear map `M →[A] N →[R] P`. -/ def lift.equiv : (M →ₗ[A] N →ₗ[R] P) ≃ₗ[B] M ⊗[R] N →ₗ[A] P := - LinearEquiv.ofLinear (uncurry R A B M N P) (lcurry R A B M N P) + LinearEquiv.ofLinearMap (uncurry R A B M N P) (lcurry R A B M N P) (LinearMap.ext fun _ => ext fun x y => lift_tmul _ x y) (LinearMap.ext fun f => LinearMap.ext fun x => LinearMap.ext fun y => lift_tmul f x y) @@ -320,7 +320,7 @@ variable {R A B M N P Q} /-- Heterobasic version of `TensorProduct.congr` -/ def congr (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) : (M ⊗[R] N) ≃ₗ[A] (P ⊗[R] Q) := - LinearEquiv.ofLinear (map f g) (map f.symm g.symm) + LinearEquiv.ofLinearMap (map f g) (map f.symm g.symm) (ext fun _m _n => congr_arg₂ (· ⊗ₜ ·) (f.apply_symm_apply _) (g.apply_symm_apply _)) (ext fun _m _n => congr_arg₂ (· ⊗ₜ ·) (f.symm_apply_apply _) (g.symm_apply_apply _)) @@ -355,7 +355,7 @@ variable (R A M) /-- Heterobasic version of `TensorProduct.rid`. -/ protected def rid : M ⊗[R] R ≃ₗ[A] M := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap (lift <| Algebra.lsmul _ _ _ |>.toLinearMap |>.flip) (mk R A M R |>.flip 1) (LinearMap.ext <| one_smul _) @@ -400,7 +400,7 @@ variable [Algebra A B] [IsScalarTower A B M] Note this is especially useful with `A = R` (where it is a "more linear" version of `TensorProduct.assoc`), or with `B = A`. -/ def assoc : (M ⊗[A] P) ⊗[R] Q ≃ₗ[B] M ⊗[A] (P ⊗[R] Q) := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap (lift <| lift <| lcurry R A B P Q _ ∘ₗ mk A B M (P ⊗[R] Q)) (lift <| uncurry R A B P Q _ ∘ₗ curry (mk R B _ Q)) (by ext; rfl) @@ -532,7 +532,7 @@ and a `B`-module `M`, `S`-module `P`, `R`-module `Q`, then ``` -/ def rightComm : (M ⊗[S] P) ⊗[R] Q ≃ₗ[B] (M ⊗[R] Q) ⊗[S] P := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap (lift (lift (LinearMap.lflip.toLinearMap ∘ₗ (AlgebraTensorModule.mk _ _ _ _).compr₂ (AlgebraTensorModule.mk _ _ _ _)))) (lift (lift (LinearMap.lflip.toLinearMap ∘ₗ diff --git a/Mathlib/LinearAlgebra/Trace.lean b/Mathlib/LinearAlgebra/Trace.lean index 6c4239c9ef..2e916eca8f 100644 --- a/Mathlib/LinearAlgebra/Trace.lean +++ b/Mathlib/LinearAlgebra/Trace.lean @@ -402,6 +402,6 @@ lemma Module.Free.bijective_algebraMap_of_finrank_eq_one {R S : Type*} [CommRing have h2 : (f ∘ₗ Algebra.linearMap R S) ∘ₗ LinearMap.trace R S = LinearMap.id := b.ext fun i ↦ (basisUnique Unit h).ext fun j ↦ (by simp [f, b, Basis.tensorProduct]) - let eq : R ≃ₗ[R] End R S := .ofLinear (f ∘ₗ Algebra.linearMap R S) (.trace R S) h2 h1 + let eq : R ≃ₗ[R] End R S := .ofLinearMap (f ∘ₗ Algebra.linearMap R S) (.trace R S) h2 h1 have hf : Function.Bijective f := ⟨Algebra.lmul_injective, .of_comp eq.surjective⟩ exact (Function.Bijective.of_comp_iff' hf _).mp eq.bijective diff --git a/Mathlib/RepresentationTheory/Coinvariants.lean b/Mathlib/RepresentationTheory/Coinvariants.lean index 88834570e1..f4f63afbda 100644 --- a/Mathlib/RepresentationTheory/Coinvariants.lean +++ b/Mathlib/RepresentationTheory/Coinvariants.lean @@ -237,7 +237,7 @@ variable (ρ α) in @[simps! symm_apply] noncomputable def coinvariantsFinsuppLEquiv : Coinvariants (ρ.finsupp α) ≃ₗ[k] α →₀ Coinvariants ρ := - LinearEquiv.ofLinear (coinvariantsToFinsupp ρ α) (finsuppToCoinvariants ρ α) + LinearEquiv.ofLinearMap (coinvariantsToFinsupp ρ α) (finsuppToCoinvariants ρ α) (by ext; simp) (by ext; simp) @[simp] @@ -283,7 +283,7 @@ lemma ofCoinvariantsTprodLeftRegular_mk_tmul_single (x : V) (g : G) (r : k) : @[simps! symm_apply] noncomputable def coinvariantsTprodLeftRegularLEquiv : Coinvariants (ρ.tprod (leftRegular k G)) ≃ₗ[k] V := - LinearEquiv.ofLinear (ofCoinvariantsTprodLeftRegular ρ) + LinearEquiv.ofLinearMap (ofCoinvariantsTprodLeftRegular ρ) (Coinvariants.mk _ ∘ₗ (TensorProduct.mk k V k[G]).flip (.single 1 1)) (by ext; simp) (by ext; simp) @@ -502,7 +502,7 @@ variable (A α) @[simps! symm_apply] noncomputable abbrev coinvariantsTensorFreeLEquiv : Coinvariants (A ⊗ free k G α).ρ ≃ₗ[k] (α →₀ A) := - LinearEquiv.ofLinear (coinvariantsTensorFreeToFinsupp A α) (finsuppToCoinvariantsTensorFree A α) + .ofLinearMap (coinvariantsTensorFreeToFinsupp A α) (finsuppToCoinvariantsTensorFree A α) (lhom_ext fun i x => by simp [finsuppToCoinvariantsTensorFree_single, coinvariantsTensorFreeToFinsupp_mk_tmul_single]) <| diff --git a/Mathlib/RepresentationTheory/FiniteIndex.lean b/Mathlib/RepresentationTheory/FiniteIndex.lean index 3d7fc7f106..e97c51615f 100644 --- a/Mathlib/RepresentationTheory/FiniteIndex.lean +++ b/Mathlib/RepresentationTheory/FiniteIndex.lean @@ -177,7 +177,7 @@ The forward map sends `(⟦g ⊗ₜ[k] a⟧, sg) ↦ ρ(s)(a)`, and the inverse @[simps! hom_hom_toLinearMap inv_hom_toLinearMap] noncomputable def indCoindIso (A : Rep.{max w u} k S) : ind S.subtype A ≅ coind S.subtype A := - mkIso (.mk (.ofLinear (indToCoind A) (coindToInd A) + mkIso (.mk (.ofLinearMap (indToCoind A) (coindToInd A) (coindToInd_indToCoind A) (indToCoind_coindToInd A)) <| fun g ↦ by ext; simp) variable (k S) diff --git a/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean b/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean index 5fda00c63b..8041e0c715 100644 --- a/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean +++ b/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean @@ -1022,7 +1022,7 @@ set_option backward.isDefEq.respectTransparency false in @[simps! -isSimp] def H1AddEquivOfIsTrivial : H1 A ≃+ (Additive <| Abelianization G) ⊗[ℤ] A := - LinearEquiv.toAddEquiv <| LinearEquiv.ofLinear + LinearEquiv.toAddEquiv <| LinearEquiv.ofLinearMap (H1ToTensorOfIsTrivial A) (lift <| mkH1OfIsTrivial A) (ext <| LinearMap.toAddMonoidHom_injective <| by ext g a diff --git a/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean b/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean index ff051e3127..5c3185b279 100644 --- a/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean +++ b/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean @@ -179,7 +179,7 @@ lemma ofTensorProduct_comp_ofTensorProductInvOfPiFintype : /-- `ofTensorProduct` as an equiv in the case of `M = R^ι` where `ι` is finite. -/ def ofTensorProductEquivOfPiFintype : AdicCompletion I R ⊗[R] (ι → R) ≃ₗ[AdicCompletion I R] AdicCompletion I (ι → R) := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap (ofTensorProduct I (ι → R)) (ofTensorProductInvOfPiFintype I ι) (ofTensorProduct_comp_ofTensorProductInvOfPiFintype I ι) diff --git a/Mathlib/RingTheory/AdicCompletion/Functoriality.lean b/Mathlib/RingTheory/AdicCompletion/Functoriality.lean index fa6e85c521..b71da44356 100644 --- a/Mathlib/RingTheory/AdicCompletion/Functoriality.lean +++ b/Mathlib/RingTheory/AdicCompletion/Functoriality.lean @@ -178,7 +178,7 @@ theorem map_of (f : M →ₗ[R] N) (x : M) : map I f (of I M x) = of I N (f x) : /-- A linear equiv induces a linear equiv on adic completions. -/ def congr (f : M ≃ₗ[R] N) : AdicCompletion I M ≃ₗ[AdicCompletion I R] AdicCompletion I N := - LinearEquiv.ofLinear (map I f) + LinearEquiv.ofLinearMap (map I f) (map I f.symm) (by simp [map_comp]) (by simp [map_comp]) @[simp] @@ -292,7 +292,7 @@ theorem sum_comp_sumInv : sum I M ∘ₗ sumInv I M = LinearMap.id := by /-- If `ι` is finite, `sum` has `sumInv` as inverse. -/ def sumEquivOfFintype : (⨁ j, (AdicCompletion I (M j))) ≃ₗ[AdicCompletion I R] AdicCompletion I (⨁ j, M j) := - LinearEquiv.ofLinear (sum I M) (sumInv I M) (sum_comp_sumInv I M) (sumInv_comp_sum I M) + LinearEquiv.ofLinearMap (sum I M) (sumInv I M) (sum_comp_sumInv I M) (sumInv_comp_sum I M) @[simp] theorem sumEquivOfFintype_apply (x : ⨁ j, (AdicCompletion I (M j))) : diff --git a/Mathlib/RingTheory/Extension/Cotangent/Basis.lean b/Mathlib/RingTheory/Extension/Cotangent/Basis.lean index 6a4cc4ce7b..43b653c5d8 100644 --- a/Mathlib/RingTheory/Extension/Cotangent/Basis.lean +++ b/Mathlib/RingTheory/Extension/Cotangent/Basis.lean @@ -168,7 +168,7 @@ set_option backward.isDefEq.respectTransparency false in /-- The linear isomorphism `S ⊗[T] J/J² ≃ₗ[S] I/I²`. -/ def tensorCotangentEquiv : S ⊗[D.T] D.presLeft.toExtension.Cotangent ≃ₗ[S] P.toExtension.Cotangent := by - refine LinearEquiv.ofLinear D.tensorCotangentHom D.tensorCotangentInv ?_ ?_ + refine LinearEquiv.ofLinearMap D.tensorCotangentHom D.tensorCotangentInv ?_ ?_ · refine b.ext fun i ↦ ?_ simpa only [LinearMap.coe_comp, Function.comp_apply, tensorCotangentInv_apply, tensorCotangentHom_tmul] using! D.hf (b i) diff --git a/Mathlib/RingTheory/Flat/Equalizer.lean b/Mathlib/RingTheory/Flat/Equalizer.lean index 766fec0bfe..25ac663715 100644 --- a/Mathlib/RingTheory/Flat/Equalizer.lean +++ b/Mathlib/RingTheory/Flat/Equalizer.lean @@ -139,7 +139,7 @@ private lemma LinearMap.lTensor_eqLocus_subtype_tensorEqLocusInv [Module.Flat R /-- If `M` is `R`-flat, the canonical map `M ⊗[R] ker f →ₗ[R] ker (𝟙 ⊗ f)` is an isomorphism. -/ def LinearMap.tensorKerEquiv [Module.Flat R M] : M ⊗[R] LinearMap.ker f ≃ₗ[S] LinearMap.ker (AlgebraTensorModule.lTensor S M f) := - LinearEquiv.ofLinear (LinearMap.tensorKer S M f) (LinearMap.tensorKerInv S M f) + LinearEquiv.ofLinearMap (LinearMap.tensorKer S M f) (LinearMap.tensorKerInv S M f) (by ext x; simp) (by ext m x @@ -164,7 +164,7 @@ def LinearMap.tensorEqLocusEquiv [Module.Flat R M] : M ⊗[R] eqLocus f g ≃ₗ[S] eqLocus (AlgebraTensorModule.lTensor S M f) (AlgebraTensorModule.lTensor S M g) := - LinearEquiv.ofLinear (LinearMap.tensorEqLocus S M f g) (LinearMap.tensorEqLocusInv S M f g) + LinearEquiv.ofLinearMap (LinearMap.tensorEqLocus S M f g) (LinearMap.tensorEqLocusInv S M f g) (by ext; simp) (by ext m x diff --git a/Mathlib/RingTheory/IsTensorProduct.lean b/Mathlib/RingTheory/IsTensorProduct.lean index 6d880f1416..108f9bb12a 100644 --- a/Mathlib/RingTheory/IsTensorProduct.lean +++ b/Mathlib/RingTheory/IsTensorProduct.lean @@ -496,7 +496,7 @@ theorem IsBaseChange.of_lift_unique · dsimp at *; rw [smul_add, map_add, map_add, smul_add, hx, hy] simp_rw [DFunLike.ext_iff, LinearMap.comp_apply, LinearMap.restrictScalars_apply] at hg let fe : S ⊗[R] M ≃ₗ[S] N := - LinearEquiv.ofLinear f'' (ULift.moduleEquiv.toLinearMap.comp g) ?_ ?_ + LinearEquiv.ofLinearMap f'' (ULift.moduleEquiv.toLinearMap.comp g) ?_ ?_ · exact fe.bijective · rw [← LinearMap.cancel_left (ULift.moduleEquiv : ULift.{max v₁ v₃} N ≃ₗ[S] N).symm.injective] refine (h (ULift.{max v₁ v₃} N) <| ULift.moduleEquiv.symm.toLinearMap.comp f).unique ?_ rfl diff --git a/Mathlib/RingTheory/Localization/Module.lean b/Mathlib/RingTheory/Localization/Module.lean index 05e0c8bd54..a7ae587f65 100644 --- a/Mathlib/RingTheory/Localization/Module.lean +++ b/Mathlib/RingTheory/Localization/Module.lean @@ -239,7 +239,7 @@ def LinearMap.extendScalarsOfIsLocalizationEquiv : (M →ₗ[R] N) ≃ₗ[A] (M /-- An `R`-linear isomorphism between `S⁻¹R`-modules is actually `S⁻¹R`-linear. -/ @[simps!] def LinearEquiv.extendScalarsOfIsLocalization (f : M ≃ₗ[R] N) : M ≃ₗ[A] N := - .ofLinear (LinearMap.extendScalarsOfIsLocalization S A f) + .ofLinearMap (LinearMap.extendScalarsOfIsLocalization S A f) (LinearMap.extendScalarsOfIsLocalization S A f.symm) (by ext; simp) (by ext; simp) @@ -277,7 +277,7 @@ def mapExtendScalars : (M →ₗ[R] N) →ₗ[R] (M' →ₗ[Rₛ] N') := @[simps!] noncomputable def mapEquiv (e : M ≃ₗ[R] N) : M' ≃ₗ[Rₛ] N' := - LinearEquiv.ofLinear + LinearEquiv.ofLinearMap (IsLocalizedModule.mapExtendScalars S f g Rₛ e) (IsLocalizedModule.mapExtendScalars S g f Rₛ e.symm) (by diff --git a/Mathlib/RingTheory/MatrixAlgebra.lean b/Mathlib/RingTheory/MatrixAlgebra.lean index 6b41a99a0d..73830fa293 100644 --- a/Mathlib/RingTheory/MatrixAlgebra.lean +++ b/Mathlib/RingTheory/MatrixAlgebra.lean @@ -44,7 +44,7 @@ attribute [local ext] ext_linearMap /-- `Matrix.kroneckerTMul` as a linear equivalence, when the two arguments are tensored. -/ def kroneckerTMulLinearEquiv : Matrix l m M ⊗[R] Matrix n p N ≃ₗ[S] Matrix (l × n) (m × p) (M ⊗[R] N) := - .ofLinear + .ofLinearMap (AlgebraTensorModule.lift <| kroneckerTMulBilinear R S) (Matrix.liftLinear R fun ii jj => AlgebraTensorModule.map (singleLinearMap S ii.1 jj.1) (singleLinearMap R ii.2 jj.2)) diff --git a/Mathlib/RingTheory/PicardGroup.lean b/Mathlib/RingTheory/PicardGroup.lean index 6b62b5e7dd..3c5c3e0905 100644 --- a/Mathlib/RingTheory/PicardGroup.lean +++ b/Mathlib/RingTheory/PicardGroup.lean @@ -301,7 +301,7 @@ theorem leftInverse_iff_rightInverse : a left inverse of `g`, then in fact `f` is also the right inverse of `g`, and we promote this to an `R`-module isomorphism. -/ def linearEquivOfLeftInverse (hfg : Function.LeftInverse f g) : M ≃ₗ[R] N := - .ofLinear f g (LinearMap.ext hfg) (LinearMap.ext <| rightInverse_of_leftInverse hfg) + .ofLinearMap f g (LinearMap.ext hfg) (LinearMap.ext <| rightInverse_of_leftInverse hfg) @[simp] lemma linearEquivOfLeftInverse_apply (hfg : Function.LeftInverse f g) (x : M) : linearEquivOfLeftInverse hfg x = f x := rfl @@ -313,7 +313,7 @@ def linearEquivOfLeftInverse (hfg : Function.LeftInverse f g) : M ≃ₗ[R] N := a right inverse of `g`, then in fact `f` is also the left inverse of `g`, and we promote this to an `R`-module isomorphism. -/ def linearEquivOfRightInverse (hfg : Function.RightInverse f g) : M ≃ₗ[R] N := - .ofLinear f g (LinearMap.ext <| leftInverse_of_rightInverse hfg) (LinearMap.ext hfg) + .ofLinearMap f g (LinearMap.ext <| leftInverse_of_rightInverse hfg) (LinearMap.ext hfg) @[simp] lemma linearEquivOfRightInverse_apply (hfg : Function.RightInverse f g) (x : M) : linearEquivOfRightInverse hfg x = f x := rfl From 0232cac95945a83b27da8b5785bfd152d9b5faec Mon Sep 17 00:00:00 2001 From: Alex Korbonits <5281694+korbonits@users.noreply.github.com> Date: Mon, 3 Aug 2026 21:26:53 +0000 Subject: [PATCH 14/16] feat(Topology/Connected): local (path-)connectedness of products and pi types (#41663) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add product and pi instances for `LocallyConnectedSpace` and `LocallyPathConnectedSpace`, together with a full characterization of local (path-)connectedness of pi types: - `Prod.locallyConnectedSpace` / `Prod.locallyPathConnectedSpace`: binary products. - `Pi.locallyConnectedSpace_of_finite_not_preconnectedSpace` / `Pi.locallyPathConnectedSpace_of_finite_not_pathConnectedSpace`: a product of locally (path-)connected spaces is locally (path-)connected provided all but finitely many factors are preconnected (resp. path-connected). The `Finite ι` and all-factors-preconnected (resp. path-connected) instances are corollaries. - `Pi.locallyConnectedSpace_iff` / `Pi.locallyPathConnectedSpace_iff`: a product is locally (path-)connected iff it is empty or the above conditions hold. - Topology.IsCoinducing.locallyConnectedSpace: a topology coinduced by a locally connected topology is locally connected (used for the forward direction via the projections). Since IsQuotientMap is by definition IsCoinducing, this covers quotient maps; the analogous IsQuotientMap.locallyPathConnectedSpace already existed. Supporting API in Topology/Connected/Basic.lean: - ContinuousOn.image_connectedComponentIn_subset, ContinuousOn.mapsTo_connectedComponentIn, ContinuousOn.preimage_connectedComponentIn: ContinuousOn generalizations of the existing Continuous lemmas. - Continuous.preimage_connectedComponent: the connectedComponent form of the preimage lemma. - Deprecates Continuous.image_connectedComponentIn_subset and Continuous.mapsTo_connectedComponentIn in favor of the ContinuousOn versions. Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> --- Mathlib/Topology/Connected/Basic.lean | 40 ++++++++- .../Topology/Connected/LocallyConnected.lean | 83 ++++++++++++++++++ .../Connected/LocallyPathConnected.lean | 84 +++++++++++++++++++ Mathlib/Topology/Homeomorph/Lemmas.lean | 4 +- 4 files changed, 205 insertions(+), 6 deletions(-) diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean index 445fa61e0e..131d9f3b85 100644 --- a/Mathlib/Topology/Connected/Basic.lean +++ b/Mathlib/Topology/Connected/Basic.lean @@ -613,21 +613,33 @@ theorem Continuous.image_connectedComponent_subset [TopologicalSpace β] {f : α (isConnected_connectedComponent.image f h.continuousOn).subset_connectedComponent ((mem_image f (connectedComponent a) (f a)).2 ⟨a, mem_connectedComponent, rfl⟩) +theorem ContinuousOn.image_connectedComponentIn_subset [TopologicalSpace β] {f : α → β} {s : Set α} + {a : α} (hf : ContinuousOn f s) (hx : a ∈ s) : + f '' connectedComponentIn s a ⊆ connectedComponentIn (f '' s) (f a) := + (isPreconnected_connectedComponentIn.image _ <| hf.mono <| connectedComponentIn_subset _ _) + |>.subset_connectedComponentIn (mem_image_of_mem _ <| mem_connectedComponentIn hx) + (image_mono <| connectedComponentIn_subset _ _) + +@[deprecated ContinuousOn.image_connectedComponentIn_subset (since := "2026-07-27")] theorem Continuous.image_connectedComponentIn_subset [TopologicalSpace β] {f : α → β} {s : Set α} {a : α} (hf : Continuous f) (hx : a ∈ s) : f '' connectedComponentIn s a ⊆ connectedComponentIn (f '' s) (f a) := - (isPreconnected_connectedComponentIn.image _ hf.continuousOn).subset_connectedComponentIn - (mem_image_of_mem _ <| mem_connectedComponentIn hx) - (image_mono <| connectedComponentIn_subset _ _) + hf.continuousOn.image_connectedComponentIn_subset hx theorem Continuous.mapsTo_connectedComponent [TopologicalSpace β] {f : α → β} (h : Continuous f) (a : α) : MapsTo f (connectedComponent a) (connectedComponent (f a)) := mapsTo_iff_image_subset.2 <| h.image_connectedComponent_subset a +theorem ContinuousOn.mapsTo_connectedComponentIn [TopologicalSpace β] {f : α → β} {s : Set α} + (h : ContinuousOn f s) {a : α} (hx : a ∈ s) : + MapsTo f (connectedComponentIn s a) (connectedComponentIn (f '' s) (f a)) := + mapsTo_iff_image_subset.2 <| h.image_connectedComponentIn_subset hx + +@[deprecated ContinuousOn.mapsTo_connectedComponentIn (since := "2026-07-27")] theorem Continuous.mapsTo_connectedComponentIn [TopologicalSpace β] {f : α → β} {s : Set α} (h : Continuous f) {a : α} (hx : a ∈ s) : MapsTo f (connectedComponentIn s a) (connectedComponentIn (f '' s) (f a)) := - mapsTo_iff_image_subset.2 <| image_connectedComponentIn_subset h hx + h.continuousOn.mapsTo_connectedComponentIn hx theorem irreducibleComponent_subset_connectedComponent {x : α} : irreducibleComponent x ⊆ connectedComponent x := @@ -643,6 +655,26 @@ theorem connectedComponentIn_mono (x : α) {F G : Set α} (h : F ⊆ G) : · rw [connectedComponentIn_eq_empty hx] exact Set.empty_subset _ +/-- The preimage of a connected component of `F` is the union of the connected components of +`f ⁻¹' F` at the points of that preimage. -/ +theorem ContinuousOn.preimage_connectedComponentIn [TopologicalSpace β] {f : α → β} {F : Set β} + (hf : ContinuousOn f (f ⁻¹' F)) (y : β) : + f ⁻¹' connectedComponentIn F y = + ⋃ x ∈ f ⁻¹' connectedComponentIn F y, connectedComponentIn (f ⁻¹' F) x := by + refine subset_antisymm (fun z hz ↦ ?_) (iUnion₂_subset fun x hx z hz ↦ ?_) + · exact mem_biUnion hz (mem_connectedComponentIn (connectedComponentIn_subset F y hz)) + · rw [mem_preimage, connectedComponentIn_eq hx] + exact connectedComponentIn_mono _ (image_preimage_subset f F) + (hf.mapsTo_connectedComponentIn (connectedComponentIn_subset F y hx) hz) + +/-- The preimage of a connected component is the union of the connected components at the points +of that preimage. -/ +theorem Continuous.preimage_connectedComponent [TopologicalSpace β] {f : α → β} + (hf : Continuous f) (y : β) : + f ⁻¹' connectedComponent y = ⋃ x ∈ f ⁻¹' connectedComponent y, connectedComponent x := by + simpa [connectedComponentIn_univ] using + hf.continuousOn.preimage_connectedComponentIn (F := univ) y + /-- A preconnected space is one where there is no non-trivial open partition. -/ class PreconnectedSpace (α : Type u) [TopologicalSpace α] : Prop where /-- The universal set `Set.univ` in a preconnected space is a preconnected set. -/ diff --git a/Mathlib/Topology/Connected/LocallyConnected.lean b/Mathlib/Topology/Connected/LocallyConnected.lean index b634ba83b6..9b57ca543b 100644 --- a/Mathlib/Topology/Connected/LocallyConnected.lean +++ b/Mathlib/Topology/Connected/LocallyConnected.lean @@ -151,6 +151,13 @@ theorem IsOpen.locallyConnectedSpace [LocallyConnectedSpace α] {U : Set α} (hU LocallyConnectedSpace U := hU.isOpenEmbedding_subtypeVal.locallyConnectedSpace +/-- Any topology coinduced by a locally connected topology is locally connected. -/ +theorem Topology.IsCoinducing.locallyConnectedSpace [LocallyConnectedSpace α] + [TopologicalSpace β] {f : α → β} (hf : IsCoinducing f) : LocallyConnectedSpace β := by + refine locallyConnectedSpace_iff_connectedComponentIn_open.2 fun F hF y _ ↦ ?_ + rw [← hf.isOpen_preimage, hf.continuous.continuousOn.preimage_connectedComponentIn] + exact isOpen_biUnion fun x _ ↦ (hF.preimage hf.continuous).connectedComponentIn + /-- If a space is locally connected, the topology of its connected components is discrete. -/ instance [LocallyConnectedSpace α] : DiscreteTopology <| ConnectedComponents α := by refine discreteTopology_iff_isOpen_singleton.mpr fun c ↦ ?_ @@ -162,4 +169,80 @@ instance [LocallyConnectedSpace α] : DiscreteTopology <| ConnectedComponents α instance [LocallyConnectedSpace α] [CompactSpace α] : Finite <| ConnectedComponents α := finite_of_compact_of_discrete +/-- The product of two locally connected spaces is locally connected. -/ +instance Prod.locallyConnectedSpace [TopologicalSpace β] [LocallyConnectedSpace α] + [LocallyConnectedSpace β] : LocallyConnectedSpace (α × β) := by + rw [locallyConnectedSpace_iff_connected_subsets] + rintro ⟨x, y⟩ U hU + obtain ⟨u, hu, v, hv, huv⟩ := mem_nhds_prod_iff.mp hU + exact ⟨connectedComponentIn u x ×ˢ connectedComponentIn v y, + prod_mem_nhds (connectedComponentIn_mem_nhds hu) (connectedComponentIn_mem_nhds hv), + isPreconnected_connectedComponentIn.prod isPreconnected_connectedComponentIn, + (prod_mono (connectedComponentIn_subset _ _) (connectedComponentIn_subset _ _)).trans huv⟩ + +/-- If each `X i` is locally connected and all but finitely many are preconnected, then +`∀ i, X i` is locally connected. -/ +theorem Pi.locallyConnectedSpace_of_finite_not_preconnectedSpace [∀ i, TopologicalSpace (X i)] + [∀ i, LocallyConnectedSpace (X i)] (hfinite : {i | ¬PreconnectedSpace (X i)}.Finite) : + LocallyConnectedSpace (∀ i, X i) := by + refine locallyConnectedSpace_iff_connected_subsets.2 fun x U hU ↦ ?_ + rw [nhds_pi, Filter.mem_pi] at hU + obtain ⟨J, hJ, t, ht, htU⟩ := hU + let K := J ∪ {i | ¬PreconnectedSpace (X i)} + refine ⟨K.pi fun i ↦ connectedComponentIn (t i) (x i), + set_pi_mem_nhds (hJ.union hfinite) fun i _ ↦ connectedComponentIn_mem_nhds (ht i), ?_, + fun f hf ↦ htU fun i hiJ ↦ connectedComponentIn_subset _ _ (hf i (mem_union_left _ hiJ))⟩ + classical + rw [← univ_pi_piecewise_univ] + refine isPreconnected_univ_pi fun i ↦ ?_ + by_cases hi : i ∈ K + · rw [piecewise_eq_of_mem _ _ _ hi] + exact isPreconnected_connectedComponentIn + · rw [piecewise_eq_of_notMem _ _ _ hi] + have : PreconnectedSpace (X i) := not_not.mp (not_or.1 hi).2 + exact isPreconnected_univ + +/-- A finite product of locally connected spaces is locally connected. -/ +instance Pi.locallyConnectedSpace_of_finite [Finite ι] [∀ i, TopologicalSpace (X i)] + [∀ i, LocallyConnectedSpace (X i)] : LocallyConnectedSpace (∀ i, X i) := + locallyConnectedSpace_of_finite_not_preconnectedSpace (toFinite _) + +/-- A product of preconnected, locally connected spaces is locally connected. Note that an +arbitrary product of locally connected spaces need not be locally connected, so the +preconnectedness assumption cannot be dropped entirely (though it can be dropped for finitely +many factors, see `Pi.locallyConnectedSpace_of_finite_not_preconnectedSpace`). -/ +instance Pi.locallyConnectedSpace [∀ i, TopologicalSpace (X i)] + [∀ i, LocallyConnectedSpace (X i)] [∀ i, PreconnectedSpace (X i)] : + LocallyConnectedSpace (∀ i, X i) := + locallyConnectedSpace_of_finite_not_preconnectedSpace + (finite_empty.subset fun _ hi ↦ hi inferInstance) + +/-- A product of spaces is locally connected iff it is empty, or every factor is locally +connected and all but finitely many factors are preconnected. -/ +theorem Pi.locallyConnectedSpace_iff [∀ i, TopologicalSpace (X i)] : + LocallyConnectedSpace (∀ i, X i) ↔ + IsEmpty (∀ i, X i) ∨ + (∀ i, LocallyConnectedSpace (X i)) ∧ {i | ¬PreconnectedSpace (X i)}.Finite := by + refine ⟨fun h ↦ ?_, ?_⟩ + · rcases isEmpty_or_nonempty (∀ i, X i) with he | hne + · exact .inl he + obtain ⟨x⟩ := hne + classical + have : ∀ i, Nonempty (X i) := Classical.nonempty_pi.mp ⟨x⟩ + refine .inr ⟨fun i ↦ ((isOpenMap_eval i).isQuotientMap (continuous_apply i) + (Function.surjective_eval i)).locallyConnectedSpace, ?_⟩ + have hVn : connectedComponent x ∈ 𝓝 x := + isOpen_connectedComponent.mem_nhds mem_connectedComponent + rw [nhds_pi, Filter.mem_pi] at hVn + obtain ⟨J, hJ, t, ht, htV⟩ := hVn + refine hJ.subset fun i hi ↦ by_contra fun hiJ ↦ hi ?_ + suffices himg : Function.eval i '' connectedComponent x = univ from + ⟨himg ▸ isPreconnected_connectedComponent.image _ (continuous_apply i).continuousOn⟩ + refine (subset_univ _).antisymm fun z _ ↦ ⟨Function.update x i z, htV fun j hj ↦ ?_, by simp⟩ + rw [Function.update_of_ne (ne_of_mem_of_not_mem hj hiJ)] + exact mem_of_mem_nhds (ht j) + · rintro (he | ⟨hloc, hfin⟩) + · exact ⟨he.elim⟩ + · exact locallyConnectedSpace_of_finite_not_preconnectedSpace hfin + end LocallyConnectedSpace diff --git a/Mathlib/Topology/Connected/LocallyPathConnected.lean b/Mathlib/Topology/Connected/LocallyPathConnected.lean index b5ff93d853..14d2f01fbd 100644 --- a/Mathlib/Topology/Connected/LocallyPathConnected.lean +++ b/Mathlib/Topology/Connected/LocallyPathConnected.lean @@ -29,6 +29,12 @@ path-connected, in that each point has a basis of path-connected neighborhoods. path-connected spaces are locally path-connected. * `Sum.locallyPathConnectedSpace` / `Sigma.locallyPathConnectedSpace`: disjoint unions of locally path-connected spaces are locally path-connected. +* `Prod.locallyPathConnectedSpace` / `Pi.locallyPathConnectedSpace`: binary products of locally + path-connected spaces are locally path-connected; likewise for pi types when the index type is + finite or all factors are path-connected. +* `Pi.locallyPathConnectedSpace_iff`: a product of spaces is locally path-connected iff it is + empty, or every factor is locally path-connected and all but finitely many factors are + path-connected. Abstractly, this also shows that locally path-connected spaces form a coreflective subcategory of the category of topological spaces, although we do not prove that in this form here. @@ -299,6 +305,84 @@ instance Sigma.locallyPathConnectedSpace {X : ι → Type*} @[deprecated (since := "2026-06-21")] alias Sigma.locPathConnectedSpace := Sigma.locallyPathConnectedSpace +/-- The product of two locally path-connected spaces is locally path-connected. -/ +instance Prod.locallyPathConnectedSpace [LocallyPathConnectedSpace Y] : + LocallyPathConnectedSpace (X × Y) where + path_connected_basis := fun (x, y) ↦ hasBasis_self.mpr fun U hU ↦ by + obtain ⟨u, hu, v, hv, huv⟩ := mem_nhds_prod_iff.mp hU + exact ⟨pathComponentIn u x ×ˢ pathComponentIn v y, + prod_mem_nhds (pathComponentIn_mem_nhds hu) (pathComponentIn_mem_nhds hv), + (isPathConnected_pathComponentIn (mem_of_mem_nhds hu)).prod + (isPathConnected_pathComponentIn (mem_of_mem_nhds hv)), + (Set.prod_mono pathComponentIn_subset pathComponentIn_subset).trans huv⟩ + +/-- If each `Z i` is locally path-connected and all but finitely many are path-connected, then +`∀ i, Z i` is locally path-connected. -/ +theorem Pi.locallyPathConnectedSpace_of_finite_not_pathConnectedSpace {Z : ι → Type*} + [∀ i, TopologicalSpace (Z i)] [∀ i, LocallyPathConnectedSpace (Z i)] + (hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite) : + LocallyPathConnectedSpace (∀ i, Z i) where + path_connected_basis x := hasBasis_self.mpr fun U hU ↦ by + rw [nhds_pi, Filter.mem_pi] at hU + obtain ⟨J, hJ, t, ht, htU⟩ := hU + let K := J ∪ {i | ¬PathConnectedSpace (Z i)} + refine ⟨K.pi fun i ↦ pathComponentIn (t i) (x i), + set_pi_mem_nhds (hJ.union hfinite) fun i _ ↦ pathComponentIn_mem_nhds (ht i), ?_, + fun f hf ↦ htU fun i hiJ ↦ pathComponentIn_subset (hf i (mem_union_left _ hiJ))⟩ + classical + rw [← univ_pi_piecewise_univ] + refine .pi fun i ↦ ?_ + by_cases hi : i ∈ K + · rw [piecewise_eq_of_mem _ _ _ hi] + exact isPathConnected_pathComponentIn (mem_of_mem_nhds (ht i)) + · rw [piecewise_eq_of_notMem _ _ _ hi] + have : PathConnectedSpace (Z i) := not_not.mp (not_or.1 hi).2 + exact isPathConnected_univ + +/-- A finite product of locally path-connected spaces is locally path-connected. -/ +instance Pi.locallyPathConnectedSpace_of_finite [Finite ι] {Z : ι → Type*} + [∀ i, TopologicalSpace (Z i)] [∀ i, LocallyPathConnectedSpace (Z i)] : + LocallyPathConnectedSpace (∀ i, Z i) := + locallyPathConnectedSpace_of_finite_not_pathConnectedSpace (toFinite _) + +/-- A product of path-connected, locally path-connected spaces is locally path-connected. Note +that an arbitrary product of locally path-connected spaces need not be locally path-connected, so +the path-connectedness assumption cannot be dropped entirely (though it can be dropped for +finitely many factors, see `Pi.locallyPathConnectedSpace_of_finite_not_pathConnectedSpace`). -/ +instance Pi.locallyPathConnectedSpace {Z : ι → Type*} [∀ i, TopologicalSpace (Z i)] + [∀ i, LocallyPathConnectedSpace (Z i)] [∀ i, PathConnectedSpace (Z i)] : + LocallyPathConnectedSpace (∀ i, Z i) := + locallyPathConnectedSpace_of_finite_not_pathConnectedSpace + (finite_empty.subset fun _ hi ↦ hi inferInstance) + +/-- A product of spaces is locally path-connected iff it is empty, or every factor is locally +path-connected and all but finitely many factors are path-connected. -/ +theorem Pi.locallyPathConnectedSpace_iff {Z : ι → Type*} [∀ i, TopologicalSpace (Z i)] : + LocallyPathConnectedSpace (∀ i, Z i) ↔ + IsEmpty (∀ i, Z i) ∨ + (∀ i, LocallyPathConnectedSpace (Z i)) ∧ {i | ¬PathConnectedSpace (Z i)}.Finite := by + refine ⟨fun h ↦ ?_, ?_⟩ + · rcases isEmpty_or_nonempty (∀ i, Z i) with he | hne + · exact .inl he + obtain ⟨x⟩ := hne + classical + have : ∀ i, Nonempty (Z i) := Classical.nonempty_pi.mp ⟨x⟩ + refine .inr ⟨fun i ↦ ((isOpenMap_eval i).isQuotientMap (continuous_apply i) + (surjective_eval i)).locallyPathConnectedSpace, ?_⟩ + have hVn : pathComponent x ∈ 𝓝 x := + (IsOpen.pathComponent x).mem_nhds (mem_pathComponent_self x) + rw [nhds_pi, Filter.mem_pi] at hVn + obtain ⟨J, hJ, t, ht, htV⟩ := hVn + refine hJ.subset fun i hi ↦ by_contra fun hiJ ↦ hi ?_ + suffices himg : eval i '' pathComponent x = univ from pathConnectedSpace_iff_univ.mpr + (himg ▸ isPathConnected_pathComponent.image (continuous_apply i)) + refine (subset_univ _).antisymm fun z _ ↦ ⟨update x i z, htV fun j hj ↦ ?_, by simp⟩ + rw [update_of_ne (ne_of_mem_of_not_mem hj hiJ)] + exact mem_of_mem_nhds (ht j) + · rintro (he | ⟨hloc, hfin⟩) + · exact ⟨he.elim⟩ + · exact locallyPathConnectedSpace_of_finite_not_pathConnectedSpace hfin + instance AlexandrovDiscrete.locallyPathConnectedSpace [AlexandrovDiscrete X] : LocallyPathConnectedSpace X := by apply LocallyPathConnectedSpace.of_bases nhds_basis_nhdsKer_singleton diff --git a/Mathlib/Topology/Homeomorph/Lemmas.lean b/Mathlib/Topology/Homeomorph/Lemmas.lean index 4257d91ebb..37889e18b3 100644 --- a/Mathlib/Topology/Homeomorph/Lemmas.lean +++ b/Mathlib/Topology/Homeomorph/Lemmas.lean @@ -87,8 +87,8 @@ theorem isConnected_preimage {s : Set Y} (h : X ≃ₜ Y) : theorem image_connectedComponentIn {s : Set X} (h : X ≃ₜ Y) {x : X} (hx : x ∈ s) : h '' connectedComponentIn s x = connectedComponentIn (h '' s) (h x) := by - refine (h.continuous.image_connectedComponentIn_subset hx).antisymm ?_ - have := h.symm.continuous.image_connectedComponentIn_subset (mem_image_of_mem h hx) + refine (h.continuous.continuousOn.image_connectedComponentIn_subset hx).antisymm ?_ + have := h.symm.continuous.continuousOn.image_connectedComponentIn_subset (mem_image_of_mem h hx) rwa [image_subset_iff, h.preimage_symm, h.image_symm, h.preimage_image, h.symm_apply_apply] at this From 899f7e5fd0f3d35015ae969135f529db8878a920 Mon Sep 17 00:00:00 2001 From: mpacholski <227430665+mpacholski@users.noreply.github.com> Date: Mon, 3 Aug 2026 21:26:56 +0000 Subject: [PATCH 15/16] =?UTF-8?q?feat(Topology/Algebra/Module/Spaces/Conti?= =?UTF-8?q?nuousLinearMap):=20convert=20`toLinearMap=E2=82=81=E2=82=82`=20?= =?UTF-8?q?to=20a=20linear=20map=20(#41731)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Convert the projection `toLinearMap₁₂` (which strips the topology from a continuous semibilinear map) to a linear map, by showing that it preserves addition and scalar multiplication. We also rename `toLinearMap₁₂_apply` to `toLinearMap₁₂_apply_apply_apply` without deprecation so that we can have `_apply` be a different lemma. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> Co-authored-by: JX-Mo <296066944+JX-Mo@users.noreply.github.com> Co-authored-by: mathlib-splicebot[bot] <261196803+mathlib-splicebot[bot]@users.noreply.github.com> Co-authored-by: Felix Pernegger <188575194+felixpernegger@users.noreply.github.com> Co-authored-by: Rémy Degenne <4094732+RemyDegenne@users.noreply.github.com> Co-authored-by: David Loeffler Co-authored-by: Yi.Yuan Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Thomas Browning <13339017+tb65536@users.noreply.github.com> Co-authored-by: mitchell-horner <29882987+mitchell-horner@users.noreply.github.com> Co-authored-by: Seewoo Lee <49933279+seewoo5@users.noreply.github.com> Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> Co-authored-by: Yaël Dillies Co-authored-by: Jz Pan <3397779+acmepjz@users.noreply.github.com> Co-authored-by: Kevin Buzzard Co-authored-by: Michał Pacholski Co-authored-by: Bhavik Mehta <29959226+b-mehta@users.noreply.github.com> Co-authored-by: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Co-authored-by: Richard Osborn Co-authored-by: Brian Nugent --- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean | 4 ++-- .../CharacteristicFunction/TaylorExpansion.lean | 5 ++--- .../Algebra/Module/Spaces/ContinuousLinearMap.lean | 11 +++++++---- 3 files changed, 11 insertions(+), 9 deletions(-) diff --git a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean index 01d43a1b8b..0a07d00935 100644 --- a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean +++ b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean @@ -263,8 +263,8 @@ theorem fourierIntegral_fderiv [MeasurableSpace V] [BorelSpace V] [FiniteDimensi /- First rewrite things in a simplified form, without any real change. -/ suffices ∫ x, g x • fderiv ℝ f x y ∂μ = ∫ x, (2 * ↑π * I * L y w * g x) • f x ∂μ by rw [fourierIntegral_continuousLinearMap_apply' hf'] - simpa only [fourierIntegral, ContinuousLinearMap.toLinearMap₁₂_apply, fourierSMulRight_apply, - neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul, + simpa only [fourierIntegral, ContinuousLinearMap.toLinearMap₁₂_apply_apply_apply, + fourierSMulRight_apply, neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul, smul_neg, ← smul_smul, coe_smul, neg_neg] -- Key step: integrate by parts with respect to `y` to switch the derivative from `f` to `g`. have A x : fderiv ℝ g x y = - 2 * ↑π * I * L y w * g x := diff --git a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean index 2c5f7e64be..e11fe18fba 100644 --- a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean +++ b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean @@ -66,7 +66,6 @@ lemma continuous_charFun : Continuous (charFun μ) := by refine contDiff_zero.1 (contDiff_charFun ?_) simpa using by fun_prop -set_option backward.isDefEq.respectTransparency false in theorem iteratedFDeriv_charFun {n : ℕ} {t : E} (hint : MemLp id n μ) (x : Fin n → E) : iteratedFDeriv ℝ n (charFun μ) t x = I ^ n * ∫ y, (∏ i, ⟪y, x i⟫) * exp (⟪y, t⟫ * I) ∂μ := by have h : innerₗ E = (innerSL ℝ).toLinearMap₁₂ := rfl @@ -85,8 +84,8 @@ theorem iteratedFDeriv_charFun {n : ℕ} {t : E} (hint : MemLp id n μ) (x : Fin rw [fourierIntegral_continuousMultilinearMap_apply Real.continuous_fourierChar] swap; · exact integrable_fourierPowSMulRight _ (by simpa using hint.integrable_norm_pow') (by fun_prop) - simp only [fourierIntegral, Real.fourierChar, Circle.exp, ContinuousMap.coe_mk, ofReal_mul, - ofReal_ofNat, innerSL, map_neg, map_smul, ContinuousLinearMap.toLinearMap₁₂_apply, + simp only [fourierIntegral, Real.fourierChar, Circle.coe_exp, ofReal_mul, + ofReal_ofNat, innerSL, map_neg, map_smul, ContinuousLinearMap.toLinearMap₁₂_apply_apply_apply, LinearMap.mkContinuous₂_apply, innerₛₗ_apply_apply, smul_eq_mul, neg_neg, AddChar.coe_mk, ofReal_inv, fourierPowSMulRight_apply, Pi.ofNat_apply, real_smul, ofReal_prod, mul_one, Circle.smul_def] diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean index f0a3681fab..a59c263854 100644 --- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean +++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean @@ -299,14 +299,17 @@ theorem map_smulₛₗ₂ (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (c : R) (x f (c • x) y = σ₁₃ c • f x y := by rw [f.map_smulₛₗ, smul_apply] /-- Send a continuous sesquilinear map to an abstract sesquilinear map (forgetting continuity). -/ -def toLinearMap₁₂ (L : E →SL[σ₁₃] F →SL[σ₂₃] G) : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G := - (coeLMₛₗ σ₂₃).comp L.toLinearMap +@[simps -isSimp apply] +def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G where + toFun L := (coeLMₛₗ σ₂₃).comp L.toLinearMap + map_add' _ _ := rfl + map_smul' _ _ := rfl -@[simp] lemma toLinearMap₁₂_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) : +@[simp] lemma toLinearMap₁₂_apply_apply_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) : L.toLinearMap₁₂ v w = L v w := rfl lemma toLinearMap₁₂_injective : - (toLinearMap₁₂ (E := E) (F := F) (G := G) (σ₁₃ := σ₁₃) (σ₂₃ := σ₂₃)).Injective := by + (toLinearMap₁₂ (E := E) (F := F) (G := G) (σ₁₃ := σ₁₃) (σ₂₃ := σ₂₃) : _ → _).Injective := by simp [Function.Injective, LinearMap.ext_iff, ← ContinuousLinearMap.ext_iff] lemma toLinearMap₁₂_inj (L₁ L₂ : E →SL[σ₁₃] F →SL[σ₂₃] G) : From 9fb10993c11c9e7abfa291e86fb499b6e1f4da82 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 3 Aug 2026 21:26:58 +0000 Subject: [PATCH 16/16] feat(Topology/Order): the bornology of an unbounded order is non-trivial (#42030) Also generalise the fact that cobounded sets tend to top/bot from linear orders to preorders (without a max/min element). --- Mathlib/Order/Filter/Basic.lean | 4 ++++ Mathlib/Topology/Order/Bornology.lean | 33 ++++++++++++++++++--------- 2 files changed, 26 insertions(+), 11 deletions(-) diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean index 1fb22e6f63..98f4c29e9b 100644 --- a/Mathlib/Order/Filter/Basic.lean +++ b/Mathlib/Order/Filter/Basic.lean @@ -260,6 +260,7 @@ theorem NeBot.ne {f : Filter α} (hf : NeBot f) : f ≠ ⊥ := hf.ne' @[simp, push] theorem not_neBot {f : Filter α} : ¬f.NeBot ↔ f = ⊥ := neBot_iff.not_left +@[gcongr] theorem NeBot.mono {f g : Filter α} (hf : NeBot f) (hg : f ≤ g) : NeBot g := ⟨ne_bot_of_le_ne_bot hf.1 hg⟩ @@ -269,6 +270,9 @@ theorem neBot_of_le {f g : Filter α} [hf : NeBot f] (hg : f ≤ g) : NeBot g := @[simp] theorem sup_neBot {f g : Filter α} : NeBot (f ⊔ g) ↔ NeBot f ∨ NeBot g := by simp only [neBot_iff, not_and_or, Ne, sup_eq_bot_iff] +instance neBot_sup_of_left {f g : Filter α} [f.NeBot] : NeBot (f ⊔ g) := by simp [*] +instance neBot_sup_of_right {f g : Filter α} [g.NeBot] : NeBot (f ⊔ g) := by simp [*] + theorem not_disjoint_self_iff : ¬Disjoint f f ↔ f.NeBot := by rw [disjoint_self, neBot_iff] theorem bot_sets_eq : (⊥ : Filter α).sets = univ := rfl diff --git a/Mathlib/Topology/Order/Bornology.lean b/Mathlib/Topology/Order/Bornology.lean index bcb58e3988..f7abb517fa 100644 --- a/Mathlib/Topology/Order/Bornology.lean +++ b/Mathlib/Topology/Order/Bornology.lean @@ -99,27 +99,37 @@ instance Pi.instIsOrderBornology {ι : Type*} {α : ι → Type*} [∀ i, Preord simp_rw [← forall_isBounded_image_eval_iff, bddBelow_pi, bddAbove_pi, ← forall_and, isBounded_iff_bddBelow_bddAbove] -end Preorder +variable (α) in +lemma Nonempty.of_isOrderBornology : Nonempty α := Bornology.isBounded_empty.bddBelow.nonempty -section LinearOrder +instance IsOrderBornology.neBot_cobounded_of_noBotOrder [NoBotOrder α] : (cobounded α).NeBot := by + simp [Filter.neBot_iff, cobounded_eq_bot_iff, ← isBounded_univ, isBounded_iff_bddBelow_bddAbove] -variable [Nonempty α] [LinearOrder α] [IsOrderBornology α] +instance IsOrderBornology.neBot_cobounded_of_noTopOrder [NoTopOrder α] : (cobounded α).NeBot := + neBot_cobounded_of_noBotOrder (α := αᵒᵈ) lemma IsOrderBornology.atTop_le_cobounded [NoMaxOrder α] : .atTop ≤ Bornology.cobounded α := by - intro s - rw [← compl_compl s, ← isBounded_def, isBounded_iff_bddBelow_bddAbove, compl_compl s, - Filter.atTop_basis_Ioi.mem_iff] - intro ⟨_, b, hb⟩ - rw [mem_upperBounds_iff_subset_Iic, ← compl_compl (Iic b), compl_subset_compl, compl_Iic] at hb - use b + intro s hs + rw [← compl_compl s, ← isBounded_def, isBounded_iff_bddBelow_bddAbove] at hs + obtain ⟨b, hb⟩ := hs.2 + obtain ⟨c, hbc⟩ := exists_gt b + refine Filter.mem_of_superset (Filter.mem_atTop c) fun x hx ↦ ?_ + by_contra hx' + exact hbc.not_ge <| hx.trans <| hb <| mem_compl hx' -- TODO (khw): Generate this in the future with `to_dual` -- See https://github.com/leanprover-community/mathlib4/pull/37738 lemma IsOrderBornology.atBot_le_cobounded [NoMinOrder α] : .atBot ≤ Bornology.cobounded α := atTop_le_cobounded (α := αᵒᵈ) -lemma IsOrderBornology.cobounded_le_atBot_sup_atTop : - cobounded α ≤ .atBot ⊔ .atTop := by +end Preorder + +section LinearOrder + +variable [LinearOrder α] [IsOrderBornology α] + +lemma IsOrderBornology.cobounded_le_atBot_sup_atTop : cobounded α ≤ .atBot ⊔ .atTop := by + have := Nonempty.of_isOrderBornology α intro s rw [Filter.mem_sup, Filter.atTop_basis.mem_iff, Filter.atBot_basis.mem_iff, ← compl_compl s, ← isBounded_def, isBounded_iff_bddBelow_bddAbove, compl_compl s] @@ -145,6 +155,7 @@ lemma IsOrderBornology.cobounded_eq_atTop [NoMaxOrder α] [OrderBot α] : -- TODO (khw): Generate this in the future with `to_dual` -- See https://github.com/leanprover-community/mathlib4/pull/37738 +@[to_dual existing] lemma IsOrderBornology.cobounded_eq_atBot [NoMinOrder α] [OrderTop α] : Bornology.cobounded α = .atBot := cobounded_eq_atTop (α := αᵒᵈ)