Changes
5 changed files (+54/-29)
-
-
@@ -4,7 +4,6 @@ import Mathlib.LinearAlgebra.Charpoly.Basicimport MIL.Common variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V] example (U : Submodule K V) {x y : V} (hx : x ∈ U) (hy : y ∈ U) :
-
@@ -35,11 +34,16 @@ def preimage {W : Type*} [AddCommGroup W] [Module K W] (φ : V →ₗ[K] W) (H : Submodule K W) :Submodule K V where carrier := φ ⁻¹' H zero_mem' := by sorry simp add_mem' := by sorry intro a b ha hb simp exact H.add_mem_iff_right ha |>.mpr hb smul_mem' := by sorry intro c x hx simp exact H.smul_mem c hx example (U : Submodule K V) : Module K U := inferInstance
-
@@ -79,7 +83,7 @@ {i j : ι} (hij : i ≠ j) : U i ⊓ U j = ⊥ :=(h.submodule_iSupIndep.pairwiseDisjoint hij).eq_bot -- Those conditions characterize direct sums. #check DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top #check DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top -- The relation with external direct sums: if a family of subspaces is -- in internal direct sum then the map from their external direct sum into `V`
-
@@ -96,17 +100,28 @@ example : GaloisInsertion (Submodule.span K) ((↑) : Submodule K V → Set V) :=Submodule.gi K V example {S T : Submodule K V} {x : V} (h : x ∈ S ⊔ T) : ∃ s ∈ S, ∃ t ∈ T, x = s + t := by ∃ s ∈ S, ∃ t ∈ T, x = s + t := by rw [← S.span_eq, ← T.span_eq, ← Submodule.span_union] at h induction h using Submodule.span_induction with | mem y h => sorry have h' : y ∈ Submodule.span K (S ∪ T) := Submodule.mem_span_of_mem h simp [Submodule.span_union] at h' obtain ⟨s, hs, t, ht, hy⟩ := Submodule.mem_sup.mp h' use s, hs, t, ht simp [hy] | zero => sorry use 0, by simp, 0, by simp simp | add x y hx hy hx' hy' => sorry obtain ⟨xs, hxs, xt, hxt, hx'⟩ := hx' obtain ⟨ys, hys, yt, hyt, hy'⟩ := hy' use xs + ys, S.add_mem hxs hys, xt + yt, T.add_mem hxt hyt simp [hx', hy'] module | smul a x hx hx' => sorry obtain ⟨s, hs, t, ht, h⟩ := hx' use a • s, S.smul_mem a hs, a • t, T.smul_mem a ht simp [h] section
-
@@ -136,7 +151,13 @@ #check Submodule.mem_comapexample (E : Submodule K V) (F : Submodule K W) : Submodule.map φ E ≤ F ↔ E ≤ Submodule.comap φ F := by sorry constructor · intro h x hx exact h <| Submodule.mem_map_of_mem hx · intro h x hx obtain ⟨y, hy, hy₂⟩ := Submodule.mem_map.mp hx rw [← hy₂] exact Submodule.mem_comap.mp <| h hy variable (E : Submodule K V)
-
@@ -161,7 +182,11 @@ #check Submodule.map_comap_eq#check Submodule.comap_map_eq example : Submodule K (V ⧸ E) ≃ { F : Submodule K V // E ≤ F } where toFun := sorry invFun := sorry toFun := by intro h invFun := by intro h left_inv := sorry right_inv := sorry
-
-
-
@@ -1,10 +1,10 @@import Mathlib.LinearAlgebra.Matrix.Determinant.Basic import Mathlib.LinearAlgebra.Eigenspace.Minpoly import Mathlib.LinearAlgebra.Charpoly.Basic import Mathlib.Data.Complex.FiniteDimensional import MIL.Common open Module section matrices
-
-
-
@@ -5,17 +5,17 @@ [{"url": "https://github.com/leanprover-community/mathlib4","type": "git", "subDir": null, "scope": "", "rev": "37df177aaa770670452312393d4e84aaad56e7b6", "rev": "eed770a434957369c6262aa3fb1d6426419016d4", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "v4.23.0", "inputRev": "v4.24.0-rc1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", "rev": "a22e7c1fa7707fb7ea75f2f9fd6b14de2b7b87a9", "rev": "c205f530395b57b520d3d78d975293f0c69b65ce", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main",
-
@@ -35,37 +35,37 @@ {"url": "https://github.com/leanprover-community/import-graph","type": "git", "subDir": null, "scope": "leanprover-community", "rev": "7fca1d4a190761bac0028848f73dc9a59fcb4957", "rev": "a564b9c2252afef6e0d40613d4ec086b54ffe7df", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", "rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8", "rev": "557f2069977de1c95e68de09e693bc4d1eee7842", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "v0.0.71", "inputRev": "v0.0.72-pre", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", "rev": "247ff80701c76760523b5d7c180b27b7708faf38", "rev": "fc97e592e3e150370f17a12e3613e96252c4d3d0", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", "rev": "9b703a545097978aef0e7e243ab8b71c32a9ff65", "rev": "345a958916d27982d4ecb4500fba0ebb21096651", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master",
-
@@ -75,17 +75,17 @@ {"url": "https://github.com/leanprover-community/batteries","type": "git", "subDir": null, "scope": "leanprover-community", "rev": "d117e2c28cba42e974bc22568ac999492a34e812", "rev": "b3a8bc5f8b72102ebbe4da3302432b196e215522", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", "rev": "41c5d0b8814dec559e2e1441171db434fe2281cc", "rev": "e22ed0883c7d7f9a7e294782b6b137b783715386", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main",
-
-
-
@@ -9,7 +9,7 @@[[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" rev = "v4.23.0" rev = "v4.24.0-rc1" [[lean_lib]] name = "MIL"
-
-
-
@@ -1,1 +1,1 @@leanprover/lean4:v4.23.0 leanprover/lean4:v4.24.0-rc1
-