笔记

如果有矩阵A（m n a），矩阵B(m n b)
且有f是a到b的映射
且若有像f a1=f a2的话，可以推出原像，a1=a2
若有A映射到A2（m n b）,B映射到B2（m,n,b）， 且A2=B2。 具体映射过程是A，B每一项通过f作用

？则可推出A=B


看到哪里：
行列式定义
Determinant：
1.def detRowAlternating : AlternatingMap R (n → R) R n :=
  MultilinearMap.alternatization ((MultilinearMap.mkPiAlgebra R n R).compLinearMap LinearMap.proj)
1.1 AlternatingMap：



下面这个是zulip上回答我的问题，如何展开一个定义
import Mathlib
open BigOperators Matrix
variable (l m n α : Type)
theorem mul_apply [Fintype m] [Mul α] [AddCommMonoid α] {M : Matrix l m α} {N : Matrix m n α} {i k} :
    (M * N) i k = ∑ j, M i j * N j k := by
  unfold HMul.hMul
  -- ⊢ instHMulMatrixMatrixMatrix ...
  unfold instHMulMatrixMatrixMatrix
  simp only
  -- possibly what you want?
  rfl
也能用unfold_projs


Perm n 从哪来：import Mathlib
#eval @Finset.univ (Equiv.Perm (Fin 4)) _

正则找符号：
找乘号：
instance.*:.*\n.* HMul.*Matrix
开启大小写，和.*
找逆：
instance.*:.* Inv .*Matrix

看到哪里：
矩阵乘法之逆mul_inv_rev （lake-packages/mathlib/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean）
1. inv_def 是什么？涉及两个未知名词Ring.inverse，adjugate
    1.1 inv_def 是什么：inv_def: A⁻¹ = Ring.inverse (det A) • adjugate A
    1.2 inv_def证明rfl太简洁，找到相关invOf_eq: ⅟ A = ⅟ A.det • A.adjugate
    1.3 invOf_eq中有未知名词invertibleOfDetInvertible [Invertible A.det] : Invertible A ， 还有convert
        1.3.1 invertibleOfDetInvertible中定义了逆的表达式invOf，并且给出了这个表达式的合理性（即证明）
        1.3.2 mul_invOf_self := by
                rw [mul_smul_comm, mul_adjugate, smul_smul, invOf_mul_self, one_smul]
              invOf_mul_self := by
                rw [smul_mul_assoc, adjugate_mul, smul_smul, invOf_mul_self, one_smul]
        1.3.3 convert是什么？是一种策略,转换目标，比如将已有假设的参数对比目标的参数，将参数相同变成新的目标，未详!!!
    1.4 Ring.inverse定义:gpt3.5帮忙理解：这个函数的作用是判断传入的参数 x 是否是一个单位元。如果是单位元，返回其逆元；如果不是，则返回0。
        noncomputable def inverse : M₀ → M₀ := fun x => if h : IsUnit x then ((h.unit⁻¹ : M₀ˣ) : M₀) else 0
        其中有未知名词IsUnit，h.unit⁻¹，M₀ˣ
        1.4.1 IsUnit: def IsUnit [Monoid M] (a : M) : Prop := ∃ u : Mˣ, (u : M) = a
              1.4.1.1 Monoid就是Semigroup与一个元素1这样1 * a = a * 1 = a
        1.4.2 h.unit⁻¹？
        1.4.3 M₀ˣ？
    1.5 adjugate定义：
        def adjugate (A : Matrix n n α) : Matrix n n α := of fun i => cramer Aᵀ (Pi.single i 1)
        其中有未知名词 cramer，Pi.single
        1.5.1 cramer : def cramer (A : Matrix n n α) : (n → α) →ₗ[α] (n → α) := IsLinearMap.mk' (cramerMap A) (cramer_is_linear A)
              这段代码定义了一个函数 cramer，它接受一个矩阵 A，并返回一个从类型 (n → α) 到 (n → α) 的线性映射。
              该函数的定义采用了 IsLinearMap.mk' 函数，该函数接受两个参数：cramerMap A 和 cramer_is_linear A。
              cramerMap A 是一个函数，用于实现给定矩阵 A 的克莱姆（Cramer）映射。克莱姆映射的作用是对给定的向量进行变换，利用克莱姆法则计算解的向量。这个函数将输入的向量转换为输出的向量。
              cramer_is_linear A 是一个关于矩阵 A 的证明，它说明了 cramerMap A 是一个线性映射。即，它满足线性映射的性质，例如加法和数乘的保持。
              通过使用 IsLinearMap.mk' 函数，我们可以生成一个 cramer 函数的线性映射，并且它是通过 cramerMap 函数和 cramer_is_linear 证明得到的。
              因此，整个定义的结果是一个将矩阵 A 转换为线性映射的函数 cramer。这个线性映射可以将一个类型为 (n → α) 的向量映射到另一个类型为 (n → α) 的向量。
              其中未知名词  →ₗ , IsLinearMap.mk' , cramerMap A , cramer_is_linear
            1.5.1.1 →ₗ : `M →ₗ[R] N` 是从 `M` 到 `N` 的 `R` 线性映射类型 , 即LinearMap (RingHom.id R) M M₂
                        其中有未知名词LinearMap，RingHom.id
                        1.5.1.1.1 : LinearMap即线性图，里面涉及到底层的群论大量预设，未详!!!
            1.5.1.2+ :  IsLinearMap.mk' ? , cramerMap A ?, cramer_is_linear?
2. Matrix.smul_mul结论很明显，但证明也可以简单看一下--
    2.1 对smul_mul的学习路径有点不同，先看了底层的smul_dotProduct定义,然后挖掘出了矩阵和点乘之间还有一个很需要展示的关系mul_apply'，也加进去了smul_mul的证明里面，
        矩阵乘法说到底就是两个映射的点乘!!!
3. det_mul 矩阵乘的行列式=分开行列式的数乘，这个需要回顾一下，很值得一看。
    3.1 det的定义，detRowAlternating，引出未知名词AlternatingMap，MultilinearMap.alternatization，MultilinearMap.mkPiAlgebra
        compLinearMap，LinearMap.proj -- 真的很难理解，里面太多内容了，要分开解释。
        3.1.1 太多？
    3.2 所以直接进入det_mul的证明过程：用gpt3.5教会我自己：逐步解释（gpt使用技巧：1.如何理解以下定理（定理尽量短），2.举个例子解释一下）
        第一步：det (M * N) = ∑ p : n → n, ∑ σ : Perm n, ε σ * ∏ i, M (σ i) (p i) * N (p i) i := by
        simp only [det_apply', mul_apply, prod_univ_sum, mul_sum, Fintype.piFinset_univ]
        rw [Finset.sum_comm]
        这里意外学会了如何单独分析定理，只需要导入那个包，比如import Mathlib.LinearAlgebra.Matrix.Determinant，如有报错则在该文件里找到需要的定义或符号，如local notation "ε " σ:arg => ((sign σ : ℤ) : R)
        3.2.1 simp only里面对嵌套求和符号有很好的学习帮助
            3.2.1 从det_apply'的证明，找到det_apply，即行列式的定义
                  theorem det_apply (M : Matrix n n R) : M.det = ∑ σ : Perm n, Equiv.Perm.sign σ • ∏ i, M (σ i) i :=
                  MultilinearMap.alternatization_apply _ M
                  但还是需要理解det原始的定义：
                  def detRowAlternating : AlternatingMap R (n → R) R n :=
                  MultilinearMap.alternatization ((MultilinearMap.mkPiAlgebra R n R).compLinearMap LinearMap.proj)

4. adjugate_mul_distrib 是什么？涉及伴随矩阵adjugate的运算律：adjugate (A * B) = adjugate B * adjugate A
    4.1 adjugate定义：
        def adjugate (A : Matrix n n α) : Matrix n n α :=
        of fun i => cramer Aᵀ (Pi.single i 1)
        其中Pi.single i 1 ：表示创建一个函数，它在索引 i 处的取值为 1，而其他索引处的取值为默认值（通常为 0）

5. Ring.mul_inverse_rev 是什么？涉及Ring.mul_inverse_rev的运算律



明天从类型+gpt问参数出发研究，各种映射，符号什么的琐碎知识也要补充。最重要的还是“类型理论”，“映射类型理论”


下一个视频，介绍线性代数里面的，证明矩阵的逆表达式的合理性
/Users/chenjulang/Desktop/数学/LeanCourse_Learning/lake-packages/mathlib/Mathlib/LinearAlgebra/Matrix/Adjugate.lean：
关键定理：theorem mul_adjugate (A : Matrix n n α) : A * adjugate A = A.det • (1 : Matrix n n α) := by sorry
  -- 四个领域 1.adjugate 2.cramer 3.det 4.Pi.single


下一个视频，介绍线性代数里面的，证明先矩阵乘积再行列式 等于 先行列式再乘积
Semiring： 半环（Semiring）是一个代数结构，它是一个非空集合，定义了两个二元运算（加法和乘法），并满足一些特性，如封闭性、结合律、分配律和幺元等
Module： 模块（Module）。模块在抽象代数中是一种代数结构，它具有以下特性：
    环（Ring）：用 R 表示，是一个满足一组代数运算（加法和乘法）的集合，具有特定的性质，如封闭性、结合律、分配律等。
    交换加法群（Additive Commutative Monoid）：用 M 表示，是一个满足加法运算的集合，具有封闭性、结合律、交换律和单位元等属性。
    右分配乘法（Right Distributive Multiplication）：用 • 表示，表示标量乘法作用于向量的运算。右分配乘法意味着对于任意的标量 r，s 和向量 x，(r + s) • x 等于 r • x + s • x。
    零标量乘法（Zero Scalar Multiplication）：用 0 表示，表示零元标量与任何向量的乘法结果总是零向量。即对于任意的向量 x，(0 : R) • x 等于零向量。

 -- 1.分析MultilinearMap.mkPiAlgebra R n R传参数，\\\即在语境mkPiAlgebra里面，可以直接这样替代理解 R=>R,ι=>n,A=>R
    1.1 分析所属类MultilinearMap R (fun _ : ι => A) A，\\\MultilinearMap语境里面， R=>R,ι=>ι,M₂=>A
    1.2 所以分析MultilinearMap里面的toFun类型就是 n→R→R !!bingo!!对了
    *1.3 目前只知道对于整体(MultilinearMap.mkPiAlgebra R n R)的toFun的类型是(ι → A) → A替换外层就是(n → R) → R
        具体写的是m → ∏ i, m i，替换成最外层表示就是(n->R) → ((∏ n, (n->R) n) : 就是一个R)
-- 2. 分析compLinearMap的参数MultilinearMap R (fun x ↦ R) R
    根据(MultilinearMap.mkPiAlgebra R n R)的类型为MultilinearMap R (fun x ↦ R) R，可以推断出下面
    \\\在compLinearMap语境里面  R=>R,M₁'=>(fun x ↦ R),M₂=>R
    2.1 第二个参数需要(f : ∀ i, M₁ i →ₗ[R] M₁' i)，代入上面外层的参数后是 (f : ∀ i, (fun x ↦ R) i →ₗ[R] (fun x ↦ R) i)
    ，而传入的是LinearMap.proj 属于 ((i : ι) → φ i) →ₗ[R] φ i ，

需要的是MultilinearMap R (fun ι ↦ M) N'
实际传入MultilinearMap R (fun x ↦ n → R) R
\\\所以alternatization的语境里面 R=>R,
M=>R还是M=>(n → R),??
N'=>R

试着直接分析alternatization里面的AlternatingMap R M N' ι
需要的是R (fun _ : ι => M) N ，
\\\所以AlternatingMap语境下是R=>R,ι=>M,M=>N',N=>ι
进入MultilinearMap，需要的是(R : Type uR)(M₁ : ι → Type v₁) (M₂ : Type v₂);实际传入的是R (fun _ : M=> N') ι
\\\所以MultilinearMap语境下R=>R, M₁=>(M→N') 其中ι=>M,Type v₁=>N',M₂=>ι
最后得到最终类型为(∀ i, M₁ i) → M₂  代入外层就是ι→(M→N')→M 最外层如果要对应(?m.33147 → ?m.33147 → ?m.33149) → ?m.33149的话
具体成n→n→R→R的话
则需要就需要R M N' ι分别是n n R R
反推就知道MultilinearMap R (fun _ : ι => M) N'的四个参数分别R传入n，M传入n，N'传入R，ι传入R
MultilinearMap n (fun _ : R => n) R

怎么得到？
(?m.33147 → ?m.33147 → ?m.33149) → ?m.33149

 -- 参考：
  -- def foo1 := MultilinearMap.alternatization (
  --   (MultilinearMap.mkPiAlgebra R n R).compLinearMap
  --     LinearMap.proj
  --   )
  -- #check foo1.toFun -- : (?m.59411 → ?m.59411 → ?m.59413) → ?m.59413
  -- def foo2 := (
  --   (MultilinearMap.mkPiAlgebra R n R).compLinearMap
  --     LinearMap.proj)
  -- #check foo2 -- :MultilinearMap R (fun i ↦ n → R) R
  -- #check foo2.toFun -- :(?m.62638 → ?m.62638 → ?m.62640) → ?m.62640
  -- def foo3 := (MultilinearMap.mkPiAlgebra R n R)
  -- #check foo3 -- MultilinearMap R (fun x ↦ R) R 或者 MultilinearMap R (n ↦ R) R
  -- #check foo3.toFun -- (?m.31250 → ?m.31252) → ?m.31252 或 (n ↦ R) ↦ R
have :sorry:=sorry



线性独立视频：
-- 假设我们有一个向量空间 V，它是由实数组成，记作 {v0, v1, v2, ...}。接下来，
    -- 让我们考虑一个具体的例子，其中有限支撑函数 f 从整数集合到这个向量空间 V 上的向量。假设 f 是这样一个函数：
    -- f(0) = 2
    -- f(1) = -3
    -- f(3) = 5
    -- 现在，我们可以使用 Finsupp.total 函数将这些特殊的函数组合起来，得到一个 V 中的向量，
    -- 即把所有函数 f 的值加在一起得到的结果。在这个例子中，我们可以计算如下：
    -- Finsupp.total ι V R (λ i, f i)
    -- 根据上述定义的函数 f，我们可以计算出：
    -- Finsupp.total ι V R (λ i, f i) = 2 * v0 + (-3) * v1 + 5 * v3
    -- 这里，v0, v1 和 v3 是 V 中的基向量。因此，Finsupp.total ι V R (λ i, f i) 将是向量 2v0 - 3v1 + 5v3。
    -- 希望这个例子能够帮助你更好地理解 Finsupp.total ι M R v 的意义。

    -- smulRight:
    -- M₁ = ℝ²
    -- M = ℝ³
    -- S = ℝ
    -- f: M₁ →ₗ[ℝ] S
    -- f b = b₁ + 2b₂
    -- x: M
    -- x = [1, 2, 3]
    -- 在这个例子中，M₁ 是二维实数向量空间，M 是三维实数向量空间，S 是实数域。
    -- f 是一个线性映射，将 M₁ 中的向量 [b₁, b₂] 映射到实数域 S 上，根据定义，f b = b₁ + 2b₂。
    -- x 是一个三维实数向量 [1, 2, 3]。
    -- 现在我们可以应用 smulRight 方法，并提供上述定义中的参数值f 和 x：
    -- result = smulRight(f, x)
    -- 计算结果如下：
    -- 对于给定的输入 b，result 的线性映射将 b 应用到 f 上，然后乘以向量 x。
    -- 假设我们选择 b = [2, 3]，那么根据 f 的定义，f [2, 3] = 2 + 2 * 3 = 8。
    -- 将 f [2, 3] 与向量 x = [1, 2, 3] 相乘得到 [8, 16, 24]。
    -- 因此，对于这个例子，result 的线性映射将输入向量 [2, 3] 映射为 [8, 16, 24]。

    -- lsum:
    -- 假设你有三个朋友：Alice、Bob 和 Charlie。你想创建一个函数，
    -- 将每个人的名字映射到他们的年龄。你可以使用以下映射函数来实现：
    -- F: str → int
    -- F "Alice" = 25
    -- F "Bob" = 30
    -- F "Charlie" = 28
    -- 这里，F 是一个从字符串到整数的函数，它将每个名字映射到相应的年龄。
    -- 现在，假设你有一个名字列表，其中包含 Alice、Bob 和 Charlie：
    -- d: str →₀ int
    -- d = {"Alice" → 2, "Bob" → 1, "Charlie" → 3}
    -- 在这个例子中，我们有三个名字及其对应的数量。Alice 的数量是 2，Bob 的数量是 1，Charlie 的数量是 3。
    -- 现在，我们可以使用 lsum 方法将映射函数 F 和名字函数 d 组合起来：
    -- lsumResult = lsum F d
    -- lsumResult 是一个从 (str →₀ int) 到 int 的线性映射。
    -- 具体的计算步骤如下：
    -- 对于给定的输入 {"Alice" → 2, "Bob" → 1, "Charlie" → 3}，toFun 方法将遍历每个名字，
    -- 并根据映射函数 F 将每个名字映射到相应的年龄。
    -- 根据我们之前定义的 F 函数，我们得到 Alice 的年龄是 25，Bob 的年龄是 30，Charlie 的年龄是 28。
    -- 根据 toFun 方法的定义，我们将对输入 {"Alice" → 2, "Bob" → 1, "Charlie" → 3} 中的每个名字进行遍历。
    -- 对于 "Alice"，我们将应用 F "Alice"，对于 "Bob"，我们将应用 F "Bob"，
    -- 对于 "Charlie"，我们将应用 F "Charlie"。然后，我们将所有结果进行求和，并得到最终的结果。

    -- lsum：
    -- 让我们通过一个具体的例子来说明这个同构关系：
    -- 假设我们有一个线性映射 f: ℝ² → ℝ，它将二维实数向量v映射到实数。这个映射可以表示为：
    -- f (v) = f((x, y)) = 2x + 3y
    -- 其中 x 和 y 是实数。
    -- 现在，我们希望找到一个同构关系，将这个线性映射 f 表示为一个有限支持函数经过另一个线性映射的组合。
    -- 首先，我们定义一个特殊的有限支持函数 g: {1, 2} →₀ ℝ²，它对应着一个从索引集合 {1, 2} 到 ℝ² 的映射，
    -- 并且只在索引集合中的有限个位置取非零值。我们可以定义 g 如下：
    -- g1 = (v.1, 0) = (x, 0)
    -- g2 = (0, v.2) = (0, y)
    -- 接下来，根据同构关系 (α → M →ₗ[R] N) ≃ₗ[S] (α →₀ M) →ₗ[R] N，我们可以找到一个线性同构，
    -- 将 f 转换为另一种表达形式。
    -- 我们可以定义一个线性映射 L: (α →₀ M) →ₗ[R] N，它将有限支持函数映射到实数。
    -- 我们可以选择 L(g) = 2g1.x + 3g2.y = 2x + 3y = f (v)
    -- 其中 g(i)_j 表示 g(i) 中第 j 个分量。
    -- 通过这样的构造，我们可以将原始的线性映射 f 表示为一个有限支持函数 g 经过另一个线性映射 L 的组合。
    -- 这展示了 (α → M →ₗ[R] N) 和 (α →₀ M) →ₗ[R] N 之间的同构关系。