English
A meta-result showing how prototype_perm can transform IsWeaklyRegular under a permutation rs' of rs with a corresponding sub-permutation compatibility condition.
Русский
Мета-результат, показывающий как prototype_perm может преобразовать IsWeaklyRegular при перестановке rs' относительно rs с соответствующим условием совместимости подперестановки.
LaTeX
$$$\\text{prototype_perm}$ asserts regularity is invariant under an allowed permutation of rs.$$
Lean4
theorem prototype_perm {rs : List R} (h : IsWeaklyRegular M rs) {rs'} (h'' : rs ~ rs')
(h' :
∀ a b rs',
(a :: b :: rs') <+~ rs →
let K := torsionBy R (M ⧸ (Ideal.ofList rs' • ⊤ : Submodule R M)) b
K = a • K → K = ⊥) :
IsWeaklyRegular M rs' :=
have H :=
LinearEquiv.isWeaklyRegular_congr <| quotEquivOfEqBot _ <| Eq.trans (congrArg (· • ⊤) Ideal.ofList_nil) (bot_smul ⊤)
(H rs').mp <| (aux [] h'' (.refl rs) (h''.symm.subperm)) <| (H rs).mpr h
where aux {rs₁ rs₂} (rs₀ : List R) (h₁₂ : rs₁ ~ rs₂) (H₁ : rs₀ ++ rs₁ <+~ rs) (H₃ : rs₀ ++ rs₂ <+~ rs)
(h : IsWeaklyRegular (M ⧸ (Ideal.ofList rs₀ • ⊤ : Submodule R M)) rs₁) :
IsWeaklyRegular (M ⧸ (Ideal.ofList rs₀ • ⊤ : Submodule R M)) rs₂ := by {
induction h₁₂ generalizing rs₀ with
| nil => exact .nil R _
| cons r _ ih =>
let e := quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
rw [isWeaklyRegular_cons_iff, ← e.isWeaklyRegular_congr] at h ⊢
refine h.imp_right (ih (r :: rs₀) ?_ ?_) <;> exact List.perm_middle.subperm_right.mp ‹_›
| swap a b
t =>
rw [show ∀ x y z, x :: y :: z = [x, y] ++ z from fun _ _ _ => rfl, isWeaklyRegular_append_iff] at h ⊢
have : Ideal.ofList [b, a] = Ideal.ofList [a, b] :=
congrArg Ideal.span <| Set.ext fun _ => (List.Perm.swap a b []).mem_iff
rw [(quotEquivOfEq _ _ (congrArg₂ _ this rfl)).isWeaklyRegular_congr] at h
rw [List.append_cons, List.append_cons, List.append_assoc _ [b] [a]] at H₁
apply(List.sublist_append_left (rs₀ ++ [b, a]) _).subperm.trans at H₁
apply List.perm_append_comm.subperm.trans at H₁
exact h.imp_left (swap · (h' b a rs₀ H₁))
| trans h₁₂ _ ih₁₂ ih₂₃ =>
have H₂ := (h₁₂.append_left rs₀).subperm_right.mp H₁
exact ih₂₃ rs₀ H₂ H₃ (ih₁₂ rs₀ H₁ H₂ h)
}
-- putting `{rs' : List R}` and `h2` after `h3` would be better for partial
-- application, but this argument order seems nicer overall
