Merge branch 'master' into mans0954/hull-kernel-topology

Mathlib.lean

@@ -183,8 +183,10 @@ import Mathlib.Algebra.CharZero.Infinite
 import Mathlib.Algebra.CharZero.Lemmas
 import Mathlib.Algebra.CharZero.Quotient
 import Mathlib.Algebra.Colimit.DirectLimit
+import Mathlib.Algebra.Colimit.Finiteness
 import Mathlib.Algebra.Colimit.Module
 import Mathlib.Algebra.Colimit.Ring
+import Mathlib.Algebra.Colimit.TensorProduct
 import Mathlib.Algebra.ContinuedFractions.Basic
 import Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
 import Mathlib.Algebra.ContinuedFractions.Computation.Approximations
@@ -303,6 +305,7 @@ import Mathlib.Algebra.Group.Opposite
 import Mathlib.Algebra.Group.PNatPowAssoc
 import Mathlib.Algebra.Group.Pi.Basic
 import Mathlib.Algebra.Group.Pi.Lemmas
+import Mathlib.Algebra.Group.Pi.Units
 import Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import Mathlib.Algebra.Group.Pointwise.Finset.Interval
 import Mathlib.Algebra.Group.Pointwise.Set.Basic
@@ -317,6 +320,7 @@ import Mathlib.Algebra.Group.Semiconj.Units
 import Mathlib.Algebra.Group.Subgroup.Actions
 import Mathlib.Algebra.Group.Subgroup.Basic
 import Mathlib.Algebra.Group.Subgroup.Defs
+import Mathlib.Algebra.Group.Subgroup.Even
 import Mathlib.Algebra.Group.Subgroup.Finite
 import Mathlib.Algebra.Group.Subgroup.Finsupp
 import Mathlib.Algebra.Group.Subgroup.Ker
@@ -626,7 +630,9 @@ import Mathlib.Algebra.NoZeroSMulDivisors.Pi
 import Mathlib.Algebra.NoZeroSMulDivisors.Prod
 import Mathlib.Algebra.Notation
 import Mathlib.Algebra.Opposites
-import Mathlib.Algebra.Order.AbsoluteValue
+import Mathlib.Algebra.Order.AbsoluteValue.Basic
+import Mathlib.Algebra.Order.AbsoluteValue.Equivalence
+import Mathlib.Algebra.Order.AbsoluteValue.Euclidean
 import Mathlib.Algebra.Order.AddGroupWithTop
 import Mathlib.Algebra.Order.AddTorsor
 import Mathlib.Algebra.Order.Algebra
@@ -652,7 +658,6 @@ import Mathlib.Algebra.Order.CauSeq.BigOperators
 import Mathlib.Algebra.Order.CauSeq.Completion
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Algebra.Order.CompleteField
-import Mathlib.Algebra.Order.EuclideanAbsoluteValue
 import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Algebra.Order.Field.Canonical.Basic
 import Mathlib.Algebra.Order.Field.Canonical.Defs
@@ -4265,6 +4270,7 @@ import Mathlib.Probability.Kernel.Disintegration.Unique
 import Mathlib.Probability.Kernel.Integral
 import Mathlib.Probability.Kernel.Invariance
 import Mathlib.Probability.Kernel.MeasurableIntegral
+import Mathlib.Probability.Kernel.Proper
 import Mathlib.Probability.Kernel.RadonNikodym
 import Mathlib.Probability.Kernel.WithDensity
 import Mathlib.Probability.Martingale.Basic

Mathlib/Algebra/Colimit/Finiteness.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2024 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu
+-/
+import Mathlib.Algebra.Colimit.Module
+import Mathlib.RingTheory.Finiteness.Basic
+
+/-!
+# Modules as direct limits of finitely generated submodules
+
+We show that every module is the direct limit of its finitely generated submodules.
+
+## Main definitions
+
+* `Module.fgSystem`: the directed system of finitely generated submodules of a module.
+
+* `Module.fgSystem.equiv`: the isomorphism between a module and the direct limit of its
+finitely generated submodules.
+-/
+
+namespace Module
+
+variable (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M]
+
+/-- The directed system of finitely generated submodules of a module. -/
+def fgSystem (N₁ N₂ : {N : Submodule R M // N.FG}) (le : N₁ ≤ N₂) : N₁ →ₗ[R] N₂ :=
+  Submodule.inclusion le
+
+open DirectLimit
+
+namespace fgSystem
+
+instance : IsDirected {N : Submodule R M // N.FG} (· ≤ ·) where
+  directed N₁ N₂ :=
+    ⟨⟨_, N₁.2.sup N₂.2⟩, Subtype.coe_le_coe.mp le_sup_left, Subtype.coe_le_coe.mp le_sup_right⟩
+
+instance : DirectedSystem _ (fgSystem R M · · · ·) where
+  map_self _ _ := rfl
+  map_map _ _ _ _ _ _ := rfl
+
+variable [DecidableEq (Submodule R M)]
+
+open Submodule in
+/-- Every module is the direct limit of its finitely generated submodules. -/
+noncomputable def equiv : DirectLimit _ (fgSystem R M) ≃ₗ[R] M :=
+  .ofBijective (lift _ _ _ _ (fun _ ↦ Submodule.subtype _) fun _ _ _ _ ↦ rfl)
+    ⟨lift_injective _ _ fun _ ↦ Subtype.val_injective, fun x ↦
+      ⟨of _ _ _ _ ⟨_, fg_span_singleton x⟩ ⟨x, subset_span <| by rfl⟩, lift_of ..⟩⟩
+
+variable {R M}
+
+lemma equiv_comp_of (N : {N : Submodule R M // N.FG}) :
+    (equiv R M).toLinearMap ∘ₗ of _ _ _ _ N = N.1.subtype := by
+  ext; simp [equiv]
+
+end fgSystem
+
+end Module

Mathlib/Algebra/Colimit/Module.lean

@@ -247,16 +247,22 @@ theorem linearEquiv_symm_mk {g} : (linearEquiv _ _).symm ⟦g⟧ = of _ _ G f g.
 
 end equiv
 
-variable {G f}
+variable {G f} [DirectedSystem G (f · · ·)] [IsDirected ι (· ≤ ·)]
+
+theorem exists_eq_of_of_eq {i x y} (h : of R ι G f i x = of R ι G f i y) :
+    ∃ j hij, f i j hij x = f i j hij y := by
+  have := Nonempty.intro i
+  apply_fun linearEquiv _ _ at h
+  simp_rw [linearEquiv_of] at h
+  have ⟨j, h⟩ := Quotient.exact h
+  exact ⟨j, h.1, h.2.2⟩
 
 /-- A component that corresponds to zero in the direct limit is already zero in some
 bigger module in the directed system. -/
-theorem of.zero_exact [DirectedSystem G (f · · ·)] [IsDirected ι (· ≤ ·)]
-    {i x} (H : of R ι G f i x = 0) :
+theorem of.zero_exact {i x} (H : of R ι G f i x = 0) :
     ∃ j hij, f i j hij x = (0 : G j) := by
-  haveI : Nonempty ι := ⟨i⟩
-  apply_fun linearEquiv _ _ at H
-  rwa [map_zero, linearEquiv_of, DirectLimit.exists_eq_zero] at H
+  convert exists_eq_of_of_eq (H.trans (map_zero <| _).symm)
+  rw [map_zero]
 
 end DirectLimit
 

Mathlib/Algebra/Colimit/Ring.lean

@@ -158,7 +158,7 @@ theorem lift_unique (F : DirectLimit G f →+* P) (x) :
     F x = lift G f P (fun i ↦ F.comp <| of G f i) (fun i j hij x ↦ by simp) x := by
   obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
   exact x.induction_on (by simp) (fun _ ↦ .symm <| lift_of ..)
-    (by simp +contextual) (by simp+contextual)
+    (by simp+contextual) (by simp+contextual)
 
 lemma lift_injective [Nonempty ι] [IsDirected ι (· ≤ ·)]
     (injective : ∀ i, Function.Injective <| g i) :
@@ -193,7 +193,7 @@ variable {G f'}
 bigger module in the directed system. -/
 theorem of.zero_exact {i x} (hix : of G (f' · · ·) i x = 0) :
     ∃ (j : _) (hij : i ≤ j), f' i j hij x = 0 := by
-  haveI := Nonempty.intro i
+  have := Nonempty.intro i
   apply_fun ringEquiv _ _ at hix
   rwa [map_zero, ringEquiv_of, DirectLimit.exists_eq_zero] at hix
 
@@ -206,7 +206,7 @@ from the components to the direct limits are injective. -/
 theorem of_injective [IsDirected ι (· ≤ ·)] [DirectedSystem G fun i j h ↦ f' i j h]
     (hf : ∀ i j hij, Function.Injective (f' i j hij)) (i) :
     Function.Injective (of G (fun i j h ↦ f' i j h) i) :=
-  haveI := Nonempty.intro i
+  have := Nonempty.intro i
   ((ringEquiv _ _).comp_injective _).mp
     fun _ _ eq ↦  DirectLimit.mk_injective f' hf _ (by simpa only [← ringEquiv_of])
 

Mathlib/Algebra/Colimit/TensorProduct.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2025 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu
+-/
+import Mathlib.Algebra.Colimit.Finiteness
+import Mathlib.LinearAlgebra.TensorProduct.DirectLimit
+
+/-!
+# Tensor product with direct limit of finitely generated submodules
+
+we show that if `M` and `P` are arbitrary modules and `N` is a finitely generated submodule
+of a module `P`, then two elements of `N ⊗ M` have the same image in `P ⊗ M` if and only if
+they already have the same image in `N' ⊗ M` for some finitely generated submodule `N' ≥ N`.
+This is the theorem `Submodule.FG.exists_rTensor_fg_inclusion_eq`. The key facts used are
+that every module is the direct limit of its finitely generated submodules and that tensor
+product preserves colimits.
+-/
+
+open TensorProduct
+
+variable {R M P : Type*} [CommSemiring R]
+variable [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P]
+
+theorem Submodule.FG.exists_rTensor_fg_inclusion_eq {N : Submodule R P} (hN : N.FG)
+    {x y : N ⊗[R] M} (eq : N.subtype.rTensor M x = N.subtype.rTensor M y) :
+    ∃ N', N'.FG ∧ ∃ h : N ≤ N', (N.inclusion h).rTensor M x = (N.inclusion h).rTensor M y := by
+  classical
+  lift N to {N : Submodule R P // N.FG} using hN
+  apply_fun (Module.fgSystem.equiv R P).symm.toLinearMap.rTensor M at eq
+  apply_fun directLimitLeft _ _ at eq
+  simp_rw [← LinearMap.rTensor_comp_apply, ← (LinearEquiv.eq_toLinearMap_symm_comp _ _).mpr
+    (Module.fgSystem.equiv_comp_of N), directLimitLeft_rTensor_of] at eq
+  have ⟨N', le, eq⟩ := Module.DirectLimit.exists_eq_of_of_eq eq
+  exact ⟨_, N'.2, le, eq⟩

Mathlib/Algebra/EuclideanDomain/Defs.lean

@@ -159,11 +159,8 @@ section
 theorem GCD.induction {P : R → R → Prop} (a b : R) (H0 : ∀ x, P 0 x)
     (H1 : ∀ a b, a ≠ 0 → P (b % a) a → P a b) : P a b := by
   classical
-  exact if a0 : a = 0 then by
-    -- Porting note: required for hygiene, the equation compiler introduces a dummy variable `x`
-    -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unnecessarily.20tombstoned.20argument/near/314573315
-    change P a b
-    exact a0.symm ▸ H0 b
+  exact if a0 : a = 0 then
+    a0.symm ▸ H0 b
   else
     have _ := mod_lt b a0
     H1 _ _ a0 (GCD.induction (b % a) a H0 H1)

Mathlib/Algebra/Group/Pi/Units.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2024 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.Algebra.Group.Pi.Basic
+import Mathlib.Algebra.Group.Units.Defs
+import Mathlib.Algebra.Group.Equiv.Basic
+import Mathlib.Util.Delaborators
+
+/-! # Units in pi types -/
+
+variable {ι : Type*} {M : ι → Type*} [∀ i, Monoid (M i)] {x : Π i, M i}
+
+open Units in
+/-- The monoid equivalence between units of a product,
+and the product of the units of each monoid. -/
+@[to_additive (attr := simps)
+  "The additive-monoid equivalence between (additive) units of a product,
+  and the product of the (additive) units of each monoid."]
+def MulEquiv.piUnits : (Π i, M i)ˣ ≃* Π i, (M i)ˣ where
+  toFun f i := ⟨f.val i, f.inv i, congr_fun f.val_inv i, congr_fun f.inv_val i⟩
+  invFun f := ⟨(val <| f ·), (inv <| f ·), funext (val_inv <| f ·), funext (inv_val <| f ·)⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+  map_mul' _ _ := rfl
+
+@[to_additive]
+lemma Pi.isUnit_iff :
+    IsUnit x ↔ ∀ i, IsUnit (x i) := by
+  simp_rw [isUnit_iff_exists, funext_iff, ← forall_and]
+  exact Classical.skolem (p := fun i y ↦ x i * y = 1 ∧ y * x i = 1).symm
+
+@[to_additive]
+alias ⟨IsUnit.apply, _⟩ := Pi.isUnit_iff
+
+@[to_additive]
+lemma IsUnit.val_inv_apply (hx : IsUnit x) (i : ι) : (hx.unit⁻¹).1 i = (hx.apply i).unit⁻¹ := by
+  rw [← Units.inv_eq_val_inv, ← MulEquiv.val_inv_piUnits_apply]; congr; ext; rfl

Mathlib/Algebra/Group/Prod.lean

@@ -671,6 +671,11 @@ def prodUnits : (M × N)ˣ ≃* Mˣ × Nˣ where
     exact ⟨rfl, rfl⟩
   map_mul' := MonoidHom.map_mul _
 
+@[to_additive]
+lemma _root_.Prod.isUnit_iff {x : M × N} : IsUnit x ↔ IsUnit x.1 ∧ IsUnit x.2 where
+  mp h := ⟨(prodUnits h.unit).1.isUnit, (prodUnits h.unit).2.isUnit⟩
+  mpr h := (prodUnits.symm (h.1.unit, h.2.unit)).isUnit
+
 end
 
 end MulEquiv

Mathlib/Algebra/Group/Subgroup/Even.lean

@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2024 Artie Khovanov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Artie Khovanov
+-/
+import Mathlib.Algebra.Group.Even
+import Mathlib.Algebra.Group.Subgroup.Defs
+
+/-!
+# Squares and even elements
+
+This file defines the subgroup of squares / even elements in an abelian group.
+-/
+
+namespace Subsemigroup
+variable {S : Type*} [CommSemigroup S] {a : S}
+
+variable (S) in
+/--
+In a commutative semigroup `S`, `Subsemigroup.squareIn S` is the subsemigroup of squares in `S`.
+-/
+@[to_additive
+"In a commutative additive semigroup `S`, the type `AddSubsemigroup.evenIn S`
+is the subsemigroup of even elements of `S`."]
+def squareIn : Subsemigroup S where
+  carrier := {s : S | IsSquare s}
+  mul_mem' := IsSquare.mul
+
+@[to_additive (attr := simp)]
+theorem mem_squareIn : a ∈ squareIn S ↔ IsSquare a := Iff.rfl
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_squareIn : squareIn S = {s : S | IsSquare s} := rfl
+
+end Subsemigroup
+
+namespace Submonoid
+variable {M : Type*} [CommMonoid M] {a : M}
+
+variable (M) in
+/--
+In a commutative monoid `M`, `Submonoid.squareIn M` is the submonoid of squares in `M`.
+-/
+@[to_additive
+"In a commutative additive monoid `M`, the type `AddSubmonoid.evenIn M`
+is the submonoid of even elements of `M`."]
+def squareIn : Submonoid M where
+  __ := Subsemigroup.squareIn M
+  one_mem' := IsSquare.one
+
+@[to_additive (attr := simp)]
+theorem squareIn_toSubsemigroup : (squareIn M).toSubsemigroup = .squareIn M := rfl
+
+@[to_additive (attr := simp)]
+theorem mem_squareIn : a ∈ squareIn M ↔ IsSquare a := Iff.rfl
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_squareIn : squareIn M = {s : M | IsSquare s} := rfl
+
+end Submonoid
+
+namespace Subgroup
+variable {G : Type*} [CommGroup G] {a : G}
+
+variable (G) in
+/--
+In an abelian group `G`, `Subgroup.squareIn G` is the subgroup of squares in `G`.
+-/
+@[to_additive
+"In an abelian additive group `G`, the type `AddSubgroup.evenIn G` is
+the subgroup of even elements in `G`."]
+def squareIn : Subgroup G where
+  __ := Submonoid.squareIn G
+  inv_mem' := IsSquare.inv
+
+@[to_additive (attr := simp)]
+theorem squareIn_toSubmonoid : (squareIn G).toSubmonoid = .squareIn G := rfl
+
+@[to_additive (attr := simp)]
+theorem mem_squareIn : a ∈ squareIn G ↔ IsSquare a := Iff.rfl
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_squareIn : squareIn G = {s : G | IsSquare s} := rfl
+
+end Subgroup