no goals
G : Type u_2
inst✝¹ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
⊢ Function.Injective ↑(noncommPiCoprod ϕ hcomm)
classical
  apply (MonoidHom.ker_eq_bot_iff _).mp
  apply eq_bot_iff.mpr
  intro f heq1
  have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
    Subgroup.eq_one_of_noncommProd_eq_one_of_independent _ _ (fun _ _ _ _ h => hcomm _ _ h _ _)
      _ hind (by simp) heq1
  ext i
  apply hinj
  simp [this i (Finset.mem_univ i)]
G : Type u_2
inst✝¹ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
⊢ ker (noncommPiCoprod ϕ hcomm) = ⊥
G : Type u_2
inst✝¹ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
⊢ Function.Injective ↑(noncommPiCoprod ϕ hcomm)
apply (MonoidHom.ker_eq_bot_iff _).mp
G : Type u_2
inst✝¹ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
⊢ ker (noncommPiCoprod ϕ hcomm) ≤ ⊥
G : Type u_2
inst✝¹ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
⊢ ker (noncommPiCoprod ϕ hcomm) = ⊥
apply eq_bot_iff.mpr
G : Type u_2
inst✝¹ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
⊢ f ∈ ⊥
G : Type u_2
inst✝¹ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
⊢ ker (noncommPiCoprod ϕ hcomm) ≤ ⊥
intro f heq1
G : Type u_2
inst✝¹ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
this : ∀ (i : ι), i ∈ Finset.univ → ↑(ϕ i) (f i) = 1
⊢ f ∈ ⊥
G : Type u_2
inst✝¹ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
⊢ f ∈ ⊥
have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
  Subgroup.eq_one_of_noncommProd_eq_one_of_independent _ _ (fun _ _ _ _ h => hcomm _ _ h _ _)
    _ hind (by simp) heq1
case h
G : Type u_2
inst✝¹ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
this : ∀ (i : ι), i ∈ Finset.univ → ↑(ϕ i) (f i) = 1
i : ι
⊢ f i = OfNat.ofNat 1 i
G : Type u_2
inst✝¹ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
this : ∀ (i : ι), i ∈ Finset.univ → ↑(ϕ i) (f i) = 1
⊢ f ∈ ⊥
ext i
case h.a
G : Type u_2
inst✝¹ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
this : ∀ (i : ι), i ∈ Finset.univ → ↑(ϕ i) (f i) = 1
i : ι
⊢ ↑(ϕ i) (f i) = ↑(ϕ i) (OfNat.ofNat 1 i)
case h
G : Type u_2
inst✝¹ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
this : ∀ (i : ι), i ∈ Finset.univ → ↑(ϕ i) (f i) = 1
i : ι
⊢ f i = OfNat.ofNat 1 i
apply hinj
no goals
case h.a
G : Type u_2
inst✝¹ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
this : ∀ (i : ι), i ∈ Finset.univ → ↑(ϕ i) (f i) = 1
i : ι
⊢ ↑(ϕ i) (f i) = ↑(ϕ i) (OfNat.ofNat 1 i)
simp [this i (Finset.mem_univ i)]
no goals
G : Type u_2
inst✝¹ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
⊢ ∀ (x : ι), x ∈ Finset.univ → ↑(ϕ x) (f x) ∈ range (ϕ x)
simp