|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Oliver Nash. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Oliver Nash |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Mathlib.Algebra.Algebra.Bilinear |
| 9 | +public import Mathlib.LinearAlgebra.TensorProduct.Tower |
| 10 | +public import Mathlib.RingTheory.Localization.FractionRing |
| 11 | +public import Mathlib.RingTheory.TensorProduct.Finite |
| 12 | + |
| 13 | +/-! |
| 14 | +# Algebras which are commutative ring epimorphisms |
| 15 | +-/ |
| 16 | + |
| 17 | +@[expose] public section |
| 18 | + |
| 19 | +noncomputable section |
| 20 | +open Function TensorProduct |
| 21 | + |
| 22 | +namespace Algebra |
| 23 | + |
| 24 | +section Semiring |
| 25 | + |
| 26 | +variable (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] |
| 27 | + |
| 28 | +/-- A commutative `R`-algebra `A` is epi, if the multiplication map `A ⊗[R] A → A` is injective. -/ |
| 29 | +protected class IsEpi : Prop where |
| 30 | + injective_lift_mul : Injective <| lift <| LinearMap.mul R A |
| 31 | + |
| 32 | +/-- See also `CommRingCat.epi_iff_epi`. -/ |
| 33 | +lemma isEpi_iff_forall_one_tmul_eq : |
| 34 | + Algebra.IsEpi R A ↔ ∀ a : A, 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1 := by |
| 35 | + refine ⟨fun h a ↦ IsEpi.injective_lift_mul <| by simp, fun h ↦ ⟨fun x y hxy ↦ ?_⟩⟩ |
| 36 | + have h' (x : A ⊗[R] A) : ∃ a : A, x = a ⊗ₜ 1 := by |
| 37 | + induction x using TensorProduct.induction_on with |
| 38 | + | zero => exact ⟨0, by simp⟩ |
| 39 | + | tmul u v => |
| 40 | + use u * v |
| 41 | + calc u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v := by simp |
| 42 | + _ = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 := by rw [h] |
| 43 | + _ = (u * v) ⊗ₜ[R] 1 := by simp |
| 44 | + | add u v hu hv => |
| 45 | + obtain ⟨u, rfl⟩ := hu |
| 46 | + obtain ⟨v, rfl⟩ := hv |
| 47 | + exact ⟨u + v, by simp [add_tmul]⟩ |
| 48 | + obtain ⟨a, rfl⟩ := h' x |
| 49 | + obtain ⟨b, rfl⟩ := h' y |
| 50 | + aesop |
| 51 | + |
| 52 | +/-- See also `Algebra.isEpi_iff_surjective_algebraMap_of_finite`. -/ |
| 53 | +lemma isEpi_of_surjective_algebraMap (h : Surjective (algebraMap R A)) : |
| 54 | + Algebra.IsEpi R A := by |
| 55 | + refine (isEpi_iff_forall_one_tmul_eq R A).mpr fun a ↦ ?_ |
| 56 | + obtain ⟨r, rfl⟩ := h a |
| 57 | + rw [algebraMap_eq_smul_one, smul_tmul] |
| 58 | + |
| 59 | +end Semiring |
| 60 | + |
| 61 | +-- TODO Generalise to any localization |
| 62 | +instance (R A : Type*) [CommRing R] [IsDomain R] [Field A] [Algebra R A] [IsFractionRing R A] : |
| 63 | + Algebra.IsEpi R A := by |
| 64 | + refine (isEpi_iff_forall_one_tmul_eq R A).mpr fun x ↦ ?_ |
| 65 | + obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective (A := R) x |
| 66 | + set f := algebraMap R A with hf |
| 67 | + replace hb : f b ≠ 0 := by aesop |
| 68 | + calc 1 ⊗ₜ[R] (f a / f b) |
| 69 | + = 1 ⊗ₜ[R] (a • (1 / f b)) := by rw [← smul_div_assoc, algebraMap_eq_smul_one a] |
| 70 | + _ = f a ⊗ₜ[R] (1 / f b) := by rw [← smul_tmul, algebraMap_eq_smul_one a] |
| 71 | + _ = (b • (f a / f b)) ⊗ₜ[R] (1 / f b) := by rw [smul_def, mul_div_cancel₀ _ hb] |
| 72 | + _ = (f a / f b) ⊗ₜ[R] (b • (1 / f b)) := by rw [smul_tmul] |
| 73 | + _ = (f a / f b) ⊗ₜ[R] 1 := by rw [smul_def, mul_div_cancel₀ _ hb] |
| 74 | + |
| 75 | +section Ring |
| 76 | + |
| 77 | +variable {R A : Type*} [CommRing R] [Ring A] [Algebra R A] |
| 78 | + |
| 79 | +lemma isEpi_iff_surjective_algebraMap_of_finite [Module.Finite R A] : |
| 80 | + Algebra.IsEpi R A ↔ Surjective (algebraMap R A) := by |
| 81 | + refine ⟨fun h ↦ ?_, isEpi_of_surjective_algebraMap R A⟩ |
| 82 | + let R' := (Algebra.linearMap R A).range |
| 83 | + rcases subsingleton_or_nontrivial (A ⧸ R') with h | _ |
| 84 | + · rwa [Submodule.Quotient.subsingleton_iff, LinearMap.range_eq_top] at h |
| 85 | + have : Subsingleton ((A ⧸ R') ⊗[R] (A ⧸ R')) := by |
| 86 | + refine subsingleton_of_forall_eq 0 fun y ↦ ?_ |
| 87 | + induction y with |
| 88 | + | zero => rfl |
| 89 | + | add a b e₁ e₂ => rwa [e₁, zero_add] |
| 90 | + | tmul x y => |
| 91 | + obtain ⟨x, rfl⟩ := R'.mkQ_surjective x |
| 92 | + obtain ⟨y, rfl⟩ := R'.mkQ_surjective y |
| 93 | + obtain ⟨s, hs⟩ : ∃ s, 1 ⊗ₜ[R] s = x ⊗ₜ[R] y := by |
| 94 | + use x * y |
| 95 | + trans x ⊗ₜ 1 * 1 ⊗ₜ y |
| 96 | + · simp [(isEpi_iff_forall_one_tmul_eq R A).mp] |
| 97 | + · simp |
| 98 | + have : R'.mkQ 1 = 0 := (Submodule.Quotient.mk_eq_zero R').mpr ⟨1, map_one (algebraMap R A)⟩ |
| 99 | + rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul] |
| 100 | + cases false_of_nontrivial_of_subsingleton ((A ⧸ R') ⊗[R] (A ⧸ R')) |
| 101 | + |
| 102 | +@[deprecated (since := "2026-01-13")] |
| 103 | +alias _root_.RingHom.surjective_of_tmul_eq_tmul_of_finite := |
| 104 | + isEpi_iff_surjective_algebraMap_of_finite |
| 105 | + |
| 106 | +end Ring |
| 107 | + |
| 108 | +section CommSemiring |
| 109 | + |
| 110 | +variable (R A : Type*) [CommSemiring R] [CommSemiring A] [Algebra R A] [Algebra.IsEpi R A] |
| 111 | + |
| 112 | +variable {A} in |
| 113 | +lemma tmul_comm (a b : A) : |
| 114 | + a ⊗ₜ[R] b = b ⊗ₜ[R] a := by |
| 115 | + have (a b : A) := calc a ⊗ₜ[R] b |
| 116 | + = a • (1 ⊗ₜ[R] b) := by rw [tmul_eq_smul_one_tmul] |
| 117 | + _ = a • (b ⊗ₜ[R] 1) := by rw [(isEpi_iff_forall_one_tmul_eq R A).mp inferInstance b] |
| 118 | + _ = a • (b • (1 ⊗ₜ[R] 1)) := by rw [tmul_eq_smul_one_tmul] |
| 119 | + rw [this a b, this b a, smul_comm] |
| 120 | + |
| 121 | +section Module |
| 122 | + |
| 123 | +variable (M : Type*) [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] |
| 124 | + |
| 125 | +/-- If an `R`-algebra `A` is epi, then the scalar multiplication `A ⊗[R] M → M` is injective, for |
| 126 | +any `A`-module `M`. -/ |
| 127 | +lemma injective_lift_lsmul : |
| 128 | + Injective (lift <| LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)) := by |
| 129 | + /- Morally the proof is to recognise that we can construct the map `A ⊗[R] M → M` as a |
| 130 | + composition of (`A`-linear) equivalences: |
| 131 | + ``` |
| 132 | + A ⊗[R] M ≃ A ⊗[R] (A ⊗[A] M) |
| 133 | + ≃ (A ⊗[R] A) ⊗[A] M |
| 134 | + ≃ A ⊗[A] M |
| 135 | + ≃ M |
| 136 | + ``` |
| 137 | + However the second equivalence above requires a version of heterogeneous tensor product |
| 138 | + associativity which is problematic in Mathlib because `TensorProduct.leftModule` prioritises the |
| 139 | + left factor in any tensor product. We therefore formalise a slightly lower level proof below. -/ |
| 140 | + suffices ∀ (a : A) (m : M), 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m by |
| 141 | + let f : M →ₗ[R] A ⊗[R] M := |
| 142 | + { toFun m := 1 ⊗ₜ m |
| 143 | + map_add' m n := tmul_add _ _ _ |
| 144 | + map_smul' r m := tmul_smul _ _ _ } |
| 145 | + have aux : f ∘ₗ (lift <| LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)) = .id := by |
| 146 | + ext a m; simpa using this a m |
| 147 | + exact HasLeftInverse.injective ⟨f, fun x ↦ congr($aux x)⟩ |
| 148 | + intro a m |
| 149 | + let f : A ⊗[R] A →ₗ[R] A ⊗[R] M := lift |
| 150 | + { toFun x := |
| 151 | + { toFun y := x ⊗ₜ (y • m) |
| 152 | + map_add' := by simp [add_smul, tmul_add] |
| 153 | + map_smul' := by simp } |
| 154 | + map_add' := by intros; ext; simp [add_tmul] |
| 155 | + map_smul' := by intros; ext; simp [smul_tmul'] } |
| 156 | + simpa [f] using congr_arg f (tmul_comm R 1 a) |
| 157 | + |
| 158 | +/-- A heterogeneous variant of `TensorProduct.lid` when `R → A` is epi. -/ |
| 159 | +def _root_.TensorProduct.lid' : A ⊗[R] M ≃ₗ[A] M := |
| 160 | + .ofBijective |
| 161 | + (AlgebraTensorModule.lift <| LinearMap.restrictScalarsₗ R A M M A ∘ₗ LinearMap.lsmul A M) |
| 162 | + ⟨injective_lift_lsmul R A M, fun m ↦ ⟨1 ⊗ₜ m, by simp⟩⟩ |
| 163 | + |
| 164 | +@[simp] lemma _root_.TensorProduct.lid'_apply_tmul (a : A) (m : M) : |
| 165 | + TensorProduct.lid' R A M (a ⊗ₜ m) = a • m := |
| 166 | + rfl |
| 167 | + |
| 168 | +@[simp] lemma _root_.TensorProduct.lid'_symm_apply (m : M) : |
| 169 | + (TensorProduct.lid' R A M).symm m = 1 ⊗ₜ m := |
| 170 | + (TensorProduct.lid' R A M).injective <| by simp |
| 171 | + |
| 172 | +end Module |
| 173 | + |
| 174 | +end CommSemiring |
| 175 | + |
| 176 | +end Algebra |
0 commit comments