FormalConjectures/Kourovka/1_40.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

4 declarations, 1 contain sorry, 0 declared as axioms

Conjecture 1.40

by Sh. S. Kemkhadze

Is a group a nilgroup if it is the product of two normal nilsubgroups?

Here a nilgroup (Engel group) is a group in which every element is an Engel element. This is the Engel-group analogue of Fitting's theorem, which guarantees that the product of two normal nilpotent subgroups is nilpotent.

Reference: The Kourovka Notebook

Imports (1)
  1. def Kourovka.«1.40».engelCommutator The iterated commutator $[x,\, {}_n y]$, defined by $[x,\, {}_0 y] = x$ and $[x,\, {}_{n+1} y] = [[x,\, {}_n y], y]$ line 44 source

    Source documentation

    The iterated commutator $[x,\, {}_n y]$, defined by $[x,\, {}_0 y] = x$ and $[x,\, {}_{n+1} y] = [[x,\, {}_n y], y]$.

    no axioms what this means

    Statement uses: Group, Nat

    2 instances, coercions and auxiliary constants left out.

    def engelCommutator (x y : G) : ℕ → G
  | 0 => x
  | n + 1 => ⁅engelCommutator x y n, y⁆

/-- An element $y$ of a group $G$ is a (left) Engel element if for every
$x \in G$ there is some $n$ with $[x,\, {}_n y] = 1$. -/
  2. def Kourovka.«1.40».IsEngelElement An element $y$ of a group $G$ is a (left) Engel element if for every $x \in G$ there is some $n$ with $[x,\, {}_n y] = 1$ line 50 source

    Source documentation

    An element $y$ of a group $G$ is a (left) Engel element if for every $x \in G$ there is some $n$ with $[x,\, {}_n y] = 1$.

    standard axioms: propext what this means

    Statement uses: Group

    Proof uses: Exists, Nat, Eq, Kourovka.«1.40».engelCommutator, OfNat.ofNat

    5 instances, coercions and auxiliary constants left out.

    def IsEngelElement (y : G) : Prop :=
…
  3. def Kourovka.«1.40».IsEngelGroup A nilgroup (Engel group) is a group in which every element is an Engel element line 55 source

    Source documentation

    A nilgroup (Engel group) is a group in which every element is an Engel element.

    standard axioms: propext what this means

    Statement uses: Group

    Proof uses: Kourovka.«1.40».IsEngelElement

    def IsEngelGroup (G : Type*) [Group G] : Prop :=
…
  4. theorem Kourovka.«1.40».kourovka_1_40 Is a group a nilgroup if it is the product of two normal nilsubgroups? sorry line 66 source

    Source documentation

    Is a group a nilgroup if it is the product of two normal nilsubgroups?

    Since $H$ and $K$ are normal, the product $HK$ coincides with the join $H \sqcup K$, so "$G$ is the product of $H$ and $K$" is stated as $H \sqcup K = G$.

    depends on sorry what this means

    Statement uses: Iff, True, Group, Subgroup, Subgroup.Normal, Kourovka.«1.40».IsEngelGroup, Subtype, Membership.mem, Eq, Max.max, Top.top

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem kourovka_1_40 : answer(sorry) ↔
    ∀ (G : Type) [Group G] (H K : Subgroup G),
      H.Normal → K.Normal → IsEngelGroup H → IsEngelGroup K → H ⊔ K = ⊤ →
      IsEngelGroup G := by
…

    Mentions: Kourovka.«1.40».IsEngelGroup