Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
…regular into erd1/changeA
  • Loading branch information
erdOne committed Nov 30, 2023
2 parents 6c9696a + 6fea061 commit 65a4ed2
Showing 1 changed file with 55 additions and 41 deletions.
96 changes: 55 additions & 41 deletions FltRegular/NumberTheory/SystemOfUnits.lean
Original file line number Diff line number Diff line change
Expand Up @@ -61,49 +61,63 @@ lemma spanA_eq_spanA [Module A G] {R : ℕ} (f : Fin R → G) :
apply Submodule.subset_span (R := A)
use a

lemma mem_spanZ [Module A G] {R : ℕ} (n : Fin R) (m : Fin (p - 1)) (f : Fin R → G) :
(zeta p) ^ m.1 • f n ∈ Submodule.span ℤ
(Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p)^e.2.1 • f e.1)) := by
exact Submodule.subset_span ⟨⟨n, m⟩, rfl⟩
-- have hσmon : ∀ x, x ∈ Submonoid.powers σ := fun τ ↦ by
-- have : τ ∈ Subgroup.zpowers σ := by simp []
-- exact mem_powers_iff_mem_zpowers.2 this
-- obtain ⟨k, hk⟩ := (Submonoid.mem_powers_iff _ _).1 (hσmon h)
-- rw [← hk, map_pow, map_pow (Ideal.Quotient.mk (Ideal.span
-- {∑ i in Finset.range p, (MonoidAlgebra.of ℤ H σ) ^ i})), smul_smul (M := A),
-- ← pow_add]
-- rw [← Ideal.Quotient.mk_eq_mk, ← Submodule.Quotient.quot_mk_eq_mk]
-- sorry

-- #exit

set_option synthInstance.maxHeartbeats 0 in
lemma mem_spanS [Module A G] {R : ℕ} {g : G} (a : A) (f : Fin R → G)
(hg : g ∈ Submodule.span ℤ
(Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p) ^ e.2.1 • f e.1))) :
a • g ∈ Submodule.span ℤ
(Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p) ^ e.2.1 • f e.1)) := by
rcases a with ⟨x⟩
revert hg
sorry
-- apply MonoidAlgebra.induction_on x
-- · intro h hg
-- refine Submodule.span_induction hg ?_ ?_ ?_ ?_
-- · intro g₁ ⟨⟨n, m⟩, key⟩
-- simp only at key


-- sorry
-- · rw [smul_zero]
-- apply Submodule.zero_mem
-- · intro g₁ g₂ hg₁ hg₂
-- rw [smul_add]
-- exact Submodule.add_mem _ hg₁ hg₂
-- · intro n g hg
-- rw [smul_algebra_smul_comm]
-- apply Submodule.smul_mem
-- exact hg
-- · intro f₁ f₂ hf₁ hf₂ hg
-- simp only [MonoidAlgebra.of_apply, Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk,
-- map_add]
-- rw [add_smul (R := A)]
-- exact Submodule.add_mem _ (hf₁ hg) (hf₂ hg)
-- · intro n f₁ hf₁ hg
-- rw [Submodule.Quotient.quot_mk_eq_mk, ← intCast_smul (k := MonoidAlgebra ℤ H),
-- Submodule.Quotient.mk_smul, intCast_smul, smul_assoc]
-- apply Submodule.smul_mem
-- specialize hf₁ hg
-- rwa [Submodule.Quotient.quot_mk_eq_mk] at hf₁
-- · intro h hg
-- have : h ∈ Subgroup.zpowers σ := by simp []
-- rw [Subgroup.mem_zpowers_iff] at this
-- obtain ⟨n, hn⟩ := this
-- rw [← hn]
-- refine ⟨?_, ?_
(hg : g ∈ Submodule.span ℤ
(Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p)^e.2.1 • f e.1))) :
a • g ∈ Submodule.span ℤ
(Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p)^e.2.1 • f e.1)) := by
rcases a with ⟨x⟩
revert hg
sorry
-- apply MonoidAlgebra.induction_on x
-- · intro h hg
-- refine Submodule.span_induction hg ?_ ?_ ?_ ?_
-- · intro g₁ ⟨⟨n, m⟩, key⟩
-- simp only at key
-- rw [← key]
-- apply mem_spanZ
-- --have : h ∈ Subgroup.zpowers σ := by simp []
-- --rw [Subgroup.mem_zpowers_iff] at this
-- --obtain ⟨k, hk⟩ := this
-- --rw [← key, ← hk]
-- --refine ⟨⟨?_, m⟩, ?_
-- · rw [smul_zero]
-- apply Submodule.zero_mem
-- · intro g₁ g₂ hg₁ hg₂
-- rw [smul_add]
-- exact Submodule.add_mem _ hg₁ hg₂
-- · intro n g hg
-- rw [smul_algebra_smul_comm]
-- apply Submodule.smul_mem
-- exact hg
-- · intro f₁ f₂ hf₁ hf₂ hg
-- simp only [MonoidAlgebra.of_apply, Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk,
-- map_add]
-- rw [add_smul (R := A)]
-- exact Submodule.add_mem _ (hf₁ hg) (hf₂ hg)
-- · intro n f₁ hf₁ hg
-- rw [Submodule.Quotient.quot_mk_eq_mk, ← intCast_smul (k := MonoidAlgebra ℤ H),
-- Submodule.Quotient.mk_smul, intCast_smul, smul_assoc]
-- apply Submodule.smul_mem
-- specialize hf₁ hg
-- rwa [Submodule.Quotient.quot_mk_eq_mk] at hf₁

lemma spanA_eq_spanZ [Module A G] {R : ℕ} (f : Fin R → G) :
(Submodule.span A (Set.range f) : Set G) =
Expand Down

0 comments on commit 65a4ed2

Please sign in to comment.