Skip to content

Commit

Permalink
Update graded.lean
Browse files Browse the repository at this point in the history
  • Loading branch information
yuanyi-350 committed Oct 26, 2024
1 parent ec4986f commit 6153ef2
Showing 1 changed file with 20 additions and 19 deletions.
39 changes: 20 additions & 19 deletions FilteredRing/graded.lean
Original file line number Diff line number Diff line change
Expand Up @@ -87,28 +87,29 @@ instance : FilteredAlgebra (induced_fil' π’œ) where
carrier := {z | z * y ∈ induced_fil' π’œ (i + j)}
add_mem' := fun ha hb ↦ by simp only [Set.mem_setOf_eq, add_mul, add_mem ha.out hb.out]
zero_mem' := by simp only [Set.mem_setOf_eq, zero_mul, zero_mem]
smul_mem' := sorry
-- intro r a ha
-- simp only [Set.mem_setOf_eq, Algebra.smul_mul_assoc]
-- let P : Submodule R A := {
-- carrier := {o | r β€’ o ∈ induced_fil' π’œ (i + j)}
-- add_mem' := fun ha hb ↦ by simp only [Set.mem_setOf_eq, smul_add, add_mem ha.out hb.out]
-- zero_mem' := by simp only [Set.mem_setOf_eq, smul_zero, Submodule.zero_mem]
-- smul_mem' := sorry}
-- have : induced_fil' π’œ (i + j) ≀ P := by
-- simp only [induced_fil', F_le', iSup_le_iff]
-- intro l hl
-- intro q hq
-- simp only [Submodule.mem_mk, AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk,
-- Set.mem_setOf_eq, P]
-- have t1 : r β€’ q ∈ π’œ l := by exact Submodule.smul_mem (π’œ l) r hq
-- have t2 : π’œ l ≀ ⨆ k, ⨆ (_ : k ≀ i + j), π’œ k := by
-- apply le_biSup
-- exact hl
-- exact t2 t1
smul_mem' := by--sorry
intro r a ha
simp only [Set.mem_setOf_eq, Algebra.smul_mul_assoc]
let P : Submodule R A := {
carrier := {o | r β€’ o ∈ induced_fil' π’œ (i + j)}
add_mem' := fun ha hb ↦ by simp only [Set.mem_setOf_eq, smul_add, add_mem ha.out hb.out]
zero_mem' := by simp only [Set.mem_setOf_eq, smul_zero, Submodule.zero_mem]
smul_mem' := sorry}
have : induced_fil' π’œ (i + j) ≀ P := by
simp only [induced_fil', F_le', iSup_le_iff]
intro l hl
intro q hq
simp only [Submodule.mem_mk, AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk,
Set.mem_setOf_eq, P]
have t1 : r β€’ q ∈ π’œ l := by exact Submodule.smul_mem (π’œ l) r hq
have t2 : π’œ l ≀ ⨆ k, ⨆ (_ : k ≀ i + j), π’œ k := by
apply le_biSup
exact hl
exact t2 t1
-- #check this (a * y) ha.out
-- have : r β€’ (a * y) = (r β€’ a) * y := by exact Eq.symm (smul_mul_assoc r a y)
-- rw[ this]
sorry--**else is easy**
}
have : induced_fil' π’œ i ≀ S := by
simp only [induced_fil', F_le', iSup_le_iff]
Expand Down

0 comments on commit 6153ef2

Please sign in to comment.