Source indexedlemma · leanprover/lean4:v4.33.0-rc1

goursat

PFR.HomPFR · PFR/HomPFR.lean:46 to 65

Source documentation

Let $H$ be a subgroup of $G \times G'$ . Then there exists a subgroup $H_0$ of $G$ , a subgroup $H_1$ of $G'$ , and a homomorphism $\phi: G \to G'$ such that $H := \{ (x, \phi(x) + y): x \in H_0, y \in H_1 \}.$ In particular, $|H| = |H_0| |H_1|$ .

Exact Lean statement

lemma goursat (H : Submodule (ZMod 2) (G × G')) :
    ∃ (H₀ : Submodule (ZMod 2) G) (H₁ : Submodule (ZMod 2) G') (φ : G →+ G'),
      (∀ x : G × G', x ∈ H ↔ (x.1 ∈ H₀ ∧ x.2 - φ x.1 ∈ H₁)) ∧
        Nat.card H = Nat.card H₀ * Nat.card H₁

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma goursat (H : Submodule (ZMod 2) (G × G')) :    ∃ (H₀ : Submodule (ZMod 2) G) (H₁ : Submodule (ZMod 2) G') (φ : G →+ G'),      (∀ x : G × G', x ∈ H ↔ (x.1 ∈ H₀ ∧ x.2 - φ x.1 ∈ H₁)) ∧        Nat.card H = Nat.card H₀ * Nat.card H₁ := by  obtain ⟨S₁, S₂, f, φ, hf, hf_inv⟩ := H.exists_equiv_fst_sndModFst  use S₁, S₂, φ  constructor ; swap  · show Nat.card H = _    exact Eq.trans (Nat.card_eq_of_bijective f f.bijective) (Nat.card_prod S₁ S₂)  · intro x    · constructor      · intro hx        let x : H := { val := x, property := hx }        · constructor          · exact Set.mem_of_eq_of_mem (hf x).1.symm (f x).1.property          · exact Set.mem_of_eq_of_mem (hf x).2.symm (f x).2.property      · intro hx        · let x₁ : S₁ := { val := x.1, property := hx.1 }          let x₂ : S₂ := { val := x.2 - φ x.1, property := hx.2 }          exact Set.mem_of_eq_of_mem (by rw [hf_inv, sub_add_cancel]) (f.symm (x₁, x₂)).property