English
Over a field K, if for every q ⊆ M invariant under all reflections we have q = ⊤ whenever q ≠ ⊥, then P.IsIrreducible.
Русский
Над полем K, если для каждого q ⊆ M инвариантного относительно всех отражений справедливо, что q ≠ ⊥ следует q = ⊤, тогда P.IsIrreducible.
LaTeX
$$$$ \forall q \subseteq M, (\forall i, q \in invtSubmodule(P.reflection i)) \rightarrow q \neq \bot \rightarrow q = \top \Rightarrow P.IsIrreducible. $$$$
Lean4
/-- When the coefficients are a field, the coroot conditions for irreducibility follow from those
for the roots. -/
theorem mk' {K : Type*} [Field K] [Module K M] [Module K N] [Nontrivial M] (P : RootPairing ι K M N)
(h : ∀ (q : Submodule K M), (∀ i, q ∈ invtSubmodule (P.reflection i)) → q ≠ ⊥ → q = ⊤) : P.IsIrreducible
where
nontrivial := inferInstance
nontrivial' := (Module.nontrivial_dual_iff K).mp P.toPerfPair.symm.nontrivial
eq_top_of_invtSubmodule_reflection := h
eq_top_of_invtSubmodule_coreflection q stab
ne_bot :=
by
specialize
h (q.dualAnnihilator.map P.toPerfPair.symm) fun i ↦
invtSubmodule_reflection_of_invtSubmodule_coreflection P i q (stab i)
rw [Submodule.map_eq_top_iff, not_imp_comm] at h
replace ne_bot : q.dualAnnihilator ≠ ⊤ := by simpa
simpa using h ne_bot
