staging

Author: pink10000

LeanCommAlg/Exterior.lean

@@ -23,9 +23,12 @@ open Classical
 
 infixr:20 "<∘ₗ>" => LinearMap.comp
 
+universe u
+
 variable {A : Type*} [Semiring A]
 variable {R : Type*} [CommRing R] [Algebra R A]
 variable {M : Type*} [AddCommGroup M] [Module R M]
+variable {ι : Type u}
 
 open ExteriorAlgebra CategoryTheory
 
@@ -76,7 +79,7 @@ end TensorPower
 #check exteriorPower.alternatingMapToDual
 noncomputable def linearFormOfFamily {n : ℕ} (f : (_ : Fin n) → (Module.Dual R M)) :
     Module.Dual R (⋀[R]^n M) :=
-  (TensorPower.multilinearMapToDual R M n f) ∘ₗ (exteriorPower.toTensorPower R M n)
+  TensorPower.linearFormOfFamily f ∘ₗ (exteriorPower.toTensorPower R M) n
 
 @[simp]
 lemma linearFormOfFamily_apply (f : (_ : Fin n) → (M →ₗ[R] R)) (x : ⋀[R]^n M) :
@@ -112,40 +115,125 @@ lemma linearFormOfBasis_apply_ιMulti {I : Type*} [LinearOrder I] (b : Basis I R
   refine Finset.sum_congr rfl fun σ _ => ?_
   rw [LinearMap.map_smul_of_tower, TensorPower.linearFormOfFamily_apply_tprod]
 
+/-- If `v : ι → M` is a family of vectors and there exists a family of linear forms
+`dv : ι → (M →ₗ[R] R)` such that `dv i (v j)` is `1` for `i = j` and `0` for `i ≠ j`, then
+`v` is linearly independent. -/
+theorem linearIndependent_of_dualFamily
+    (v : ι → M) (dv : ι → (M →ₗ[R] R))
+    (h1 : ∀ (a : ι) (b : ι), a ≠ b → (dv a) (v b) = 0) (h2 : ∀ (a : ι), (dv a) (v a) = 1) :
+    LinearIndependent R v := by
+  rw [linearIndependent_iff']
+  intro s g hrel i hi
+  apply_fun (fun x => dv i x) at hrel
+  simp only [map_sum, map_smul, smul_eq_mul, _root_.map_zero] at hrel
+  rw [Finset.sum_eq_single i (fun j _ hj ↦ by rw [h1 i j (Ne.symm hj), mul_zero])
+    (fun hi' ↦ False.elim (hi' hi)), h2 i, mul_one] at hrel
+  exact hrel
+
+/-- Let `b` be a basis of `M` indexed by a linearly ordered type `I` and `s` be a finset of `I`
+of cardinality `n`. If we apply the linear form on `⋀[R]^n M` defined by `b` and `s`
+to the exterior product of the `b i` for `i ∈ s`, then we get `1`. -/
+lemma linearFormOfBasis_apply_diag {I : Type*} [LinearOrder I] (b : Basis I R M)
+    {s : Finset I} (hs : Finset.card s = n) :
+    linearFormOfBasis b hs (ιMulti_family R n b (Subtype.mk s hs)) = 1 := by
+  trans ∑ σ : Fin n ≃ Fin n,
+    TensorPower.linearFormOfFamily R n (fun i ↦ b.coord (Finset.orderIsoOfFin s hs i))
+      (Equiv.Perm.sign σ • ⨂ₜ[R] i : Fin n, b (Finset.orderIsoOfFin s hs (σ i)))
+  · rw [ιMulti_family, linearFormOfBasis_apply_ιMulti]
+    congr
+    ext σ
+    rw [LinearMap.map_smul_of_tower, TensorPower.linearFormOfFamily_apply_tprod]
+  · have hzero : ∀ σ ∈ Finset.univ, σ ≠ Equiv.refl (Fin n) →
+        (TensorPower.linearFormOfFamily R n fun i ↦ b.coord (Finset.orderIsoOfFin s hs i))
+          (Equiv.Perm.sign σ • ⨂ₜ[R] i, b (Finset.orderIsoOfFin s hs (σ i))) = 0 := by
+      rintro σ - hσ
+      rw [ne_eq, Equiv.ext_iff.not, not_forall] at hσ
+      obtain ⟨i, hi⟩ := hσ
+      rw [LinearMap.map_smul_of_tower, smul_eq_zero_iff_eq,
+        TensorPower.linearFormOfFamily_apply_tprod]
+      apply Finset.prod_eq_zero (Finset.mem_univ _) (a := i)
+      rw [Finset.coe_orderIsoOfFin_apply, Basis.coord_apply, Basis.repr_self_apply,
+        Finset.coe_orderIsoOfFin_apply, ite_eq_right_iff, OrderEmbedding.eq_iff_eq]
+      exact fun a ↦ absurd a hi
+    rw [Finset.sum_eq_single_of_mem (Equiv.refl (Fin n)) (Finset.mem_univ _) hzero,
+     Equiv.Perm.sign_refl, one_smul, TensorPower.linearFormOfFamily_apply_tprod]
+    apply Finset.prod_eq_one
+    rintro i -
+    rw [Basis.coord_apply, Basis.repr_self, Equiv.refl_apply, Finsupp.single_eq_same]
+
+lemma linearFormOfBasis_apply_nondiag_aux {I : Type*} [LinearOrder I] {s t : Finset I}
+    (hs : Finset.card s = n) (ht : Finset.card t = n) (hst : s ≠ t) (σ : Equiv.Perm (Fin n)) :
+    ∃ (i : Fin n), (Finset.orderIsoOfFin s hs i).1 ≠ (Finset.orderIsoOfFin t ht (σ i)).1 := by
+  by_contra! habs
+  apply hst
+  apply Finset.eq_of_subset_of_card_le
+  · intro a has
+    let b := Finset.orderIsoOfFin t ht (σ ((Finset.orderIsoOfFin s hs).symm ⟨a, has⟩))
+    have heq : a = b.1 := by
+      rw [← habs]
+      simp only [OrderIso.apply_symm_apply]
+    rw [heq]
+    exact b.2
+  · rw [hs, ht]
+
+/-- Let `b` be a basis of `M` indexed by a linearly ordered type `I` and `s` be a finset of `I`
+of cardinality `n`. Let `t` be a finset of `I` of cardinality `n` such that `s ≠ t`. If we apply
+the linear form on `⋀[R]^n M` defined by `b` and `s` to the exterior product of the
+`b i` for `i ∈ t`, then we get `0`. -/
+lemma linearFormOfBasis_apply_nondiag {I : Type*} [LinearOrder I] (b : Basis I R M)
+    {s t : Finset I} (hs : Finset.card s = n) (ht : Finset.card t = n) (hst : s ≠ t) :
+    linearFormOfBasis b hs (ιMulti_family R n b ⟨t, ht⟩) = 0 := by
+  simp only [ιMulti_family]
+  rw [linearFormOfBasis_apply_ιMulti]
+  apply Finset.sum_eq_zero
+  intro σ _
+  have ⟨i, hi⟩ := linearFormOfBasis_apply_nondiag_aux n hs ht hst σ
+  apply smul_eq_zero_of_right
+  apply Finset.prod_eq_zero (Finset.mem_univ i)
+  rw [Basis.coord_apply, Basis.repr_self_apply, if_neg (ne_comm.mp hi)]
 
 /-! ### Freeness and dimension of `⋀[R]^n M. -/
 
 lemma ιMulti_family_linearIndependent_ofBasis {I : Type*} [LinearOrder I] (b : Basis I R M) :
-    LinearIndependent R (ιMulti_family R n b) := by
-  -- linearIndependent_of_dualFamily _ (fun s ↦ linearFormOfBasis R n b s.2)
-  -- (fun ⟨_, _⟩ ⟨_, _⟩ hst ↦ by
-  --   rw [ne_eq, Subtype.mk.injEq] at hst
-  --   exact linearFormOfBasis_apply_nondiag _ _ _ _ _ hst)
-  -- (fun ⟨_, _⟩ ↦ linearFormOfBasis_apply_diag _ _ _ _)
-  sorry
+    LinearIndependent R (ιMulti_family R n b) :=
+  linearIndependent_of_dualFamily _ (fun st ↦ linearFormOfBasis b st.2)
+  (fun ⟨_, _⟩ ⟨_, _⟩ hst ↦ by
+    rw [ne_eq, Subtype.mk.injEq] at hst
+    exact linearFormOfBasis_apply_nondiag _ _ _ _ _ hst)
+  (fun ⟨_, _⟩ ↦ linearFormOfBasis_apply_diag _ _ _ _)
+
 
 noncomputable def basisExteriorPower {I : Type*} [LinearOrder I] (b : Basis I R M) :
     Basis {s : Finset I // Finset.card s = n} R (⋀[R]^n M) := by
+  -- by
+  -- letI : LinearOrder {s : Finset I // Finset.card s = n} := IsWellFounded.wellOrderExtension emptyWf.rel
+  -- apply Basis.mk
+  -- . case hli =>
+  --   apply ιMulti_family_linearIndependent_ofBasis R
+
+  --   #check exteriorPower.toTensorPower R M n
+
+  --   sorry
+  -- . case hsp =>
+
+  --   sorry
+  -- . case v =>
+  --   -- use linearFormOfBasis
+
 
-  -- Basis.mk (ιMulti_family_linearIndependent_ofBasis _ _ _)
-    -- (eq_top_iff.mp <| span_top_of_span_top' R n (Basis.span_eq b))
+  --   sorry
+  apply Basis.mk (ιMulti_family_linearIndependent_ofBasis _ _ _)
+    (eq_top_iff.mp <| span_top_of_span_top' R n (Basis.span_eq b))
   sorry
 
 -- variable
 
 /-- If `M` is a free module, then so is its `n`th exterior power. -/
 instance instFree [hfree : Module.Free R M] : Module.Free R (⋀[R]^n M) := by
   have ⟨I, b⟩ := hfree.exists_basis
-  -- letI : LinearOrder I := IsWellFounded.wellOrderExtension (@WellFoundedRelation.emptyWf I)
-
-  letI : LinearOrder I := by
-    apply IsWellFounded.wellOrderExtension emptyWf.rel
-
-
+  letI : LinearOrder I := IsWellFounded.wellOrderExtension emptyWf.rel
   apply Module.Free.of_basis (basisExteriorPower b)
 
-
-
 variable [StrongRankCondition R]
 
 set_option linter.unusedTactic false
@@ -155,28 +243,10 @@ set_option linter.unusedTactic false
 the `n`th exterior power of `M` is of finrank `Nat.choose r n`. -/
 lemma finrank_eq [hfree : Module.Free R M] [Module.Finite R M] :
     Module.finrank R (⋀[R]^n M) = Nat.choose (Module.finrank R M) n := by
-  -- have : IsWellFounded ((Module.Free.ChooseBasisIndex R M)) (@emptyWf.wf (Module.Free.ChooseBasisIndex R M)) := by
-
-  -- letI : LinearOrder hfree.ChooseBasisIndex := by
-    -- apply IsWellFounded.wellOrderExtension (@emptyWf.wf (Module.Free.ChooseBasisIndex R M))
-
-
-
-
-  have ⟨I, b⟩ := hfree.exists_basis
-  letI lin : LinearOrder I := by sorry
-  let B := @basisExteriorPower R _ M _ _ n I lin b
-  rw [Module.finrank_eq_card_basis hfree.chooseBasis]
-
-
-  haveI : Fintype {s : Finset I // s.card = n} := sorry
-  rw [Module.finrank_eq_card_basis B]
-  rw [← Fintype.card_finset_len]
-
-
-  sorry
-
-
+  letI : LinearOrder hfree.ChooseBasisIndex := IsWellFounded.wellOrderExtension emptyWf.rel
+  let B := @basisExteriorPower R _ M _ _ n hfree.ChooseBasisIndex _ hfree.chooseBasis
+  rw [Module.finrank_eq_card_basis hfree.chooseBasis,
+    Module.finrank_eq_card_basis B, Fintype.card_finset_len]
 
 instance ExteriorAlgebraFinite [E_finite : Module.Finite R E] :
     Module.Finite R (ExteriorAlgebra R E) := by

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fc7ec703b36bc6ddf510ff84b58265318091f439",
+   "rev": "507dd92b9ed9cfd43bd29d1438a458da6705d8a0",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8cee626a680fe217814c4bd444b94ceb31efd6b6",
+   "rev": "61c44bec841faabd47d11c2eda15f57ec2ffe9d5",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "25078369972d295301f5a1e53c3e5850cf6d9d4c",
+   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c20832d6f0b3186a97ea9361cec0a5b87dd152a3",
+   "rev": "140dc642f4f29944abcdcd3096e8ea9b4469c873",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ea953247aac573c9b5adea60bacd3e085f58aca4",
+   "rev": "96c67159f161fb6bf6ce91a2587232034ac33d7e",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.56",
+   "inputRev": "v0.0.67",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "323e9f0b9bd41161ba116fe3bff86fc464d454f2",
+   "rev": "a62ecd0343a2dcfbcac6d1e8243f5821879c0244",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "aa4c87abed970d9dfad2506000d99d30b02f476b",
+   "rev": "867d9dc77534341321179c9aa40fceda675c50d4",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f523fcb75db2b472cda7d94d6caa5d745b1a0c26",
+   "rev": "3cabaef23886b82ba46f07018f2786d9496477d6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "aff4176e5c41737a0d73be74ad9feb6a889bfa98",
+   "rev": "e22ed0883c7d7f9a7e294782b6b137b783715386",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.19.0-rc3
+leanprover/lean4:v4.22.0-rc3