English
A more elaborate permutation-based induction statement that propagates regularity across isomorphisms and reorganizations of the index list via a proof-structure auxiliary lemma.
Русский
Более сложное высказывание с перестановками, которое распространяет регулярность через изоморфизмы и перераспределение списка индексов через вспомогательную лемму структуры доказательства.
LaTeX
$$$\\text{prototype_perm}$ expresses that regularity is preserved under index permutations with an auxiliary compatibility condition.$$
Lean4
theorem isWeaklyRegular_rTensor [Module.Flat R M₂] {rs : List R} (h : IsWeaklyRegular M rs) :
IsWeaklyRegular (M ⊗[R] M₂) rs := by
induction h with
| nil N => exact nil R (N ⊗[R] M₂)
| @cons N _ _ r rs' h1 _ ih =>
let e := quotSMulTopTensorEquivQuotSMulTop r M₂ N
exact
((e.isWeaklyRegular_congr rs').mp ih).cons
(h1.rTensor M₂)
-- TODO: apply the above to localization and completion (Corollary 1.1.3 in B&H)
