English
Same criterion as mk' but stated for P.IsIrreducible with coefficients in a field K.
Русский
Та же критерий, что и mk', но для P.IsIrreducible с коэффициентами в поле K.
LaTeX
$$$$ \text{IsIrreducible}(P) \\text{ under field } K, \; \text{iff } \ldots $$$$
Lean4
theorem isIrreducible_iff_invtRootSubmodule {K : Type*} [Field K] [Module K M] [Module K N] [Nontrivial M]
(P : RootPairing ι K M N) : P.IsIrreducible ↔ IsSimpleOrder P.invtRootSubmodule :=
by
refine ⟨fun h ↦ ⟨fun ⟨q, hq⟩ ↦ ?_⟩, fun h ↦ IsIrreducible.mk' P fun q hq hq' ↦ ?_⟩
· simp only [invtRootSubmodule.bot_mem, invtRootSubmodule.top_mem, Subtype.mk_eq_bot_iff, Subtype.mk_eq_top_iff]
rw [mem_invtRootSubmodule_iff] at hq
have := IsIrreducible.eq_top_of_invtSubmodule_reflection q hq
tauto
· let q' : P.invtRootSubmodule := ⟨q, P.mem_invtRootSubmodule_iff.mpr hq⟩
replace hq' : ⊥ < q' := by simpa [q', bot_lt_iff_ne_bot, -IsSimpleOrder.bot_lt_iff_eq_top]
suffices q' = ⊤ by simpa [q'] using this
exact IsSimpleOrder.eq_top_of_lt hq'
