English
Let β, γ be preordered types with WellFoundedLT relations, α a lattice with IsModularLattice structure, and suppose there are maps f1: β → α, f2: α → β, g1: γ → α, g2: α → γ forming a Galois coinsertion f1 ⊣ f2 and a Galois insertion g2 ⊣ g1, together with hf and hg as specified. Then α is well-founded with respect to the LT-order.
Русский
Пусть β, γ — предпорядочные множества с хорошо основанными порядками, α — решетка с модульной структурой, существует пара отображений f1: β → α, f2: α → β, g1: γ → α, g2: α → γ образующая ковариантную сопряжённость f1 ⊣ f2 и сопряжённость g2 ⊣ g1, а также условия hf и hg. Тогда α имеет хорошо основанный порядок LT.
LaTeX
$$$\exists f_1,f_2,g_1,g_2,gci,gi\text{ with }\text{GaloisCoinsertion}(f_1,f_2),\text{GaloisInsertion}(g_2,g_1)\text{ and }(hf, hg)\text{ such that }\forall a:\ f_1(f_2 a)=a\wedge K\text{ and }\forall a:\ g_1(g_2 a)=a\vee K\Rightarrow\mathrm{WellFoundedLT}(\alpha).$$$
Lean4
/-- A generalization of the theorem that if `N` is a submodule of `M` and
`N` and `M / N` are both Artinian, then `M` is Artinian. -/
theorem wellFounded_lt_exact_sequence {β γ : Type*} [Preorder β] [Preorder γ] [h₁ : WellFoundedLT β]
[h₂ : WellFoundedLT γ] (K : α) (f₁ : β → α) (f₂ : α → β) (g₁ : γ → α) (g₂ : α → γ) (gci : GaloisCoinsertion f₁ f₂)
(gi : GaloisInsertion g₂ g₁) (hf : ∀ a, f₁ (f₂ a) = a ⊓ K) (hg : ∀ a, g₁ (g₂ a) = a ⊔ K) : WellFoundedLT α :=
StrictMono.wellFoundedLT (f := fun A ↦ (f₂ A, g₂ A)) fun A B hAB ↦
by
simp only [Prod.le_def, lt_iff_le_not_ge, ← gci.l_le_l_iff, ← gi.u_le_u_iff, hf, hg]
exact strictMono_inf_prod_sup hAB
