|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Joël Riou. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Joël Riou |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Mathlib.Data.SubtypeNeLift |
| 9 | +public import Mathlib.Data.Set.Card |
| 10 | +public import Mathlib.LinearAlgebra.PiTensorProduct.Basic |
| 11 | +public import Mathlib.LinearAlgebra.Quotient.Basic |
| 12 | +public import Mathlib.LinearAlgebra.TensorProduct.Map |
| 13 | +public import Mathlib.SetTheory.Cardinal.Finite |
| 14 | + |
| 15 | +/-! |
| 16 | +# Generators of multiple tensor products |
| 17 | +
|
| 18 | +Given a finite family of `R`-modules `M i`, if we have, for each `i`, |
| 19 | +a family of generators of the module `M i`, then the tensor products |
| 20 | +of these elements generate `⨂[R] i, M i`. |
| 21 | +
|
| 22 | +In `LinearAlgebra.PiTensorProduct.Finite`, we deduce that if the modules `M i` |
| 23 | +are finitely generated, then so is `⨂[R] i, M i`. |
| 24 | +
|
| 25 | +-/ |
| 26 | + |
| 27 | +@[expose] public section |
| 28 | + |
| 29 | +open TensorProduct |
| 30 | + |
| 31 | +namespace PiTensorProduct |
| 32 | + |
| 33 | +variable (R : Type*) |
| 34 | + |
| 35 | +section equivPiTensorComplSingletonTensor |
| 36 | + |
| 37 | +variable {ι : Type*} [DecidableEq ι] (M : ι → Type*) |
| 38 | + [CommSemiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)] |
| 39 | + |
| 40 | +/-- The linear equivalence between `⨂[R] i, M i` and the tensor product of |
| 41 | +the pi tensor product indexed by the complement of `{i₀}` and `M i₀`. -/ |
| 42 | +noncomputable def equivPiTensorComplSingletonTensor (i₀ : ι) : |
| 43 | + (⨂[R] i, M i) ≃ₗ[R] ((⨂[R] (i : ({i₀}ᶜ : Set ι)), M i) ⊗[R] M i₀) := |
| 44 | + (reindex R (s := M) (Equiv.subtypeNeSumPUnit.{0} i₀).symm).trans |
| 45 | + ((tmulEquivDep R (fun i ↦ M (Equiv.subtypeNeSumPUnit i₀ i))).symm.trans |
| 46 | + (LinearEquiv.lTensor _ (subsingletonEquiv Unit.unit))) |
| 47 | + |
| 48 | +variable (i₀ : ι) |
| 49 | + |
| 50 | +set_option backward.isDefEq.respectTransparency false in |
| 51 | +@[simp] |
| 52 | +lemma equivPiTensorComplSingletonTensor_tprod (i₀ : ι) (m : ∀ i, M i) : |
| 53 | + equivPiTensorComplSingletonTensor R M i₀ (⨂ₜ[R] i, m i) = |
| 54 | + (⨂ₜ[R] (j : ((Set.singleton i₀)ᶜ : Set ι)), m j) ⊗ₜ m i₀:= by |
| 55 | + dsimp [equivPiTensorComplSingletonTensor] |
| 56 | + have : (reindex R M (Equiv.subtypeNeSumPUnit.{0} i₀).symm) (⨂ₜ[R] (i : ι), m i) = |
| 57 | + ⨂ₜ[R] j, m ((Equiv.subtypeNeSumPUnit.{0} i₀) j) := by |
| 58 | + simp_rw [reindex_tprod (R := R) (s := M), Equiv.symm_symm] |
| 59 | + rw [dsimp% this, dsimp% tmulEquivDep_symm_apply R |
| 60 | + (fun i ↦ M ((Equiv.subtypeNeSumPUnit.{0} i₀) i))] |
| 61 | + exact (LinearEquiv.lTensor_tmul _ _ _ _).trans (by congr; simp) |
| 62 | + |
| 63 | +@[simp] |
| 64 | +lemma equivPiTensorComplSingletonTensor_symm_tmul (i₀ : ι) |
| 65 | + (m : ∀ (i : ((Set.singleton i₀)ᶜ : Set ι)), M i) (x : M i₀) : |
| 66 | + (equivPiTensorComplSingletonTensor R M i₀).symm |
| 67 | + ((⨂ₜ[R] (j : ((Set.singleton i₀)ᶜ : Set ι)), m j) ⊗ₜ x) = |
| 68 | + (⨂ₜ[R] i, Function.subtypeNeLift i₀ m x i) := by |
| 69 | + apply (equivPiTensorComplSingletonTensor R M i₀).injective |
| 70 | + simp only [LinearEquiv.apply_symm_apply, equivPiTensorComplSingletonTensor_tprod, |
| 71 | + Function.subtypeNeLift_self] |
| 72 | + congr |
| 73 | + ext ⟨i, hi⟩ |
| 74 | + rw [Function.subtypeNeLift_of_neq _ _ _ _ hi] |
| 75 | + rfl |
| 76 | + |
| 77 | +end equivPiTensorComplSingletonTensor |
| 78 | + |
| 79 | +variable {R} {ι : Type*} [Finite ι] {M : ι → Type*} {N : Type*} {γ : ι → Type*} |
| 80 | + |
| 81 | +section AddCommMonoid |
| 82 | + |
| 83 | +variable [CommSemiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)] |
| 84 | + [AddCommMonoid N] [Module R N] {g : ⦃i : ι⦄ → (j : γ i) → M i} |
| 85 | + |
| 86 | +lemma ext_of_span_eq_top |
| 87 | + (hg : ∀ i, Submodule.span R (Set.range (@g i)) = ⊤) |
| 88 | + {φ φ' : (⨂[R] i, M i) →ₗ[R] N} |
| 89 | + (h : ∀ (j : (i : ι) → γ i), |
| 90 | + φ (tprod _ (fun i ↦ g (j i))) = φ' (tprod _ (fun i ↦ g (j i)))) : |
| 91 | + φ = φ' := by |
| 92 | + obtain ⟨n, hι⟩ : ∃ (n : ℕ), Nat.card ι = n := ⟨_, rfl⟩ |
| 93 | + induction n generalizing ι with |
| 94 | + | zero => |
| 95 | + ext x |
| 96 | + have : IsEmpty ι := (Nat.card_eq_zero.1 hι).resolve_right <| Finite.not_infinite ‹_› |
| 97 | + obtain rfl : x = fun i ↦ @g i (isEmptyElim i) := Subsingleton.elim _ _ |
| 98 | + apply h |
| 99 | + | succ n hn => |
| 100 | + classical |
| 101 | + have : Nonempty ι := ((Nat.card_pos_iff (α := ι)).1 (by omega)).1 |
| 102 | + have i₀ : ι := Classical.arbitrary _ |
| 103 | + let e := (equivPiTensorComplSingletonTensor R M i₀).trans (TensorProduct.comm _ _ _) |
| 104 | + obtain ⟨ψ, rfl⟩ : ∃ ψ, φ = LinearMap.comp ψ e.toLinearMap := |
| 105 | + ⟨φ.comp e.symm.toLinearMap, by ext; simp⟩ |
| 106 | + obtain ⟨ψ', rfl⟩ : ∃ ψ', φ' = LinearMap.comp ψ' e.toLinearMap := |
| 107 | + ⟨φ'.comp e.symm.toLinearMap, by ext; simp⟩ |
| 108 | + dsimp [e] at h |
| 109 | + congr 1 |
| 110 | + apply (TensorProduct.lift.equiv _ _ _ _).symm.injective |
| 111 | + rw [Submodule.linearMap_eq_iff_of_span_eq_top _ _ (hg i₀)] |
| 112 | + rintro ⟨_, ⟨g₀, rfl⟩⟩ |
| 113 | + apply hn (g := fun i (j : γ i.1) ↦ by exact g j) |
| 114 | + · intro |
| 115 | + exact hg _ |
| 116 | + · intro j |
| 117 | + have : (g g₀ ⊗ₜ[R] (tprod R) fun i ↦ g (j i)) = |
| 118 | + TensorProduct.comm R _ _ ((equivPiTensorComplSingletonTensor R M i₀) |
| 119 | + (⨂ₜ[R] (i : ι), g (Function.subtypeNeLift i₀ j g₀ i))) := by |
| 120 | + simp only [equivPiTensorComplSingletonTensor_tprod, Function.subtypeNeLift_self] |
| 121 | + congr |
| 122 | + ext ⟨x, hx⟩ |
| 123 | + congr |
| 124 | + rw [Function.subtypeNeLift_of_neq _ _ _ _ (by assumption)] |
| 125 | + rfl |
| 126 | + simpa only [lift.equiv_symm_apply, this] using h (Function.subtypeNeLift i₀ j g₀) |
| 127 | + · exact Set.ncard_compl_of_ncard_eq_add _ (by simpa) |
| 128 | + |
| 129 | +lemma _root_.MultilinearMap.ext_of_span_eq_top |
| 130 | + (hg : ∀ i, Submodule.span R (Set.range (@g i)) = ⊤) |
| 131 | + {φ φ' : MultilinearMap R M N} |
| 132 | + (h : ∀ (j : (i : ι) → γ i), φ (fun i ↦ g (j i)) = φ' (fun i ↦ g (j i))) : |
| 133 | + φ = φ' := by |
| 134 | + suffices lift φ = lift φ' by |
| 135 | + ext m |
| 136 | + simpa using DFunLike.congr_fun this (tprod _ m) |
| 137 | + exact PiTensorProduct.ext_of_span_eq_top hg (fun j ↦ by simpa using h j) |
| 138 | + |
| 139 | +end AddCommMonoid |
| 140 | + |
| 141 | +variable [CommRing R] [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)] |
| 142 | + [AddCommMonoid N] [Module R N] {g : ⦃i : ι⦄ → (j : γ i) → M i} |
| 143 | + |
| 144 | +lemma submodule_span_eq_top |
| 145 | + (hg : ∀ i, Submodule.span R (Set.range (@g i)) = ⊤) : |
| 146 | + Submodule.span R (Set.range (fun j : ((i : ι) → γ i) ↦ |
| 147 | + ⨂ₜ[R] (i : ι), g (j i))) = ⊤ := by |
| 148 | + rw [← (Submodule.span R _).ker_mkQ, LinearMap.ker_eq_top] |
| 149 | + refine ext_of_span_eq_top hg (fun j ↦ ?_) |
| 150 | + simp only [Submodule.mkQ_apply, LinearMap.zero_apply, Submodule.Quotient.mk_eq_zero] |
| 151 | + exact Submodule.subset_span ⟨j, rfl⟩ |
| 152 | + |
| 153 | +end PiTensorProduct |
0 commit comments