English
For any two indices i ≠ j, the intersection of the images of the corresponding maps into the amalgamated product equals the image of the base group.
Русский
Для любых i ≠ j пересечение образов соответствующих вложений в амальгамированное произведение равно образу базовой группы.
LaTeX
$$$(\\operatorname{of} i).\\mathrm{range} \\cap (\\operatorname{of} j).\\mathrm{range} = (\\mathrm{base} \\phi).\\mathrm{range}$$$
Lean4
/-- The intersection of the images of the maps from any two distinct groups in the diagram
into the amalgamated product is the image of the map from the base group in the diagram. -/
theorem inf_of_range_eq_base_range (hφ : ∀ i, Injective (φ i)) {i j : ι} (hij : i ≠ j) :
(of i).range ⊓ (of j).range = (base φ).range :=
le_antisymm
(by
intro x ⟨⟨g₁, hg₁⟩, ⟨g₂, hg₂⟩⟩
by_contra hx
have hx1 : x ≠ 1 := by rintro rfl; simp_all only [ne_eq, one_mem, not_true_eq_false]
have hg₁1 : g₁ ≠ 1 := ne_of_apply_ne (of (φ := φ) i) (by simp_all)
have hg₂1 : g₂ ≠ 1 := ne_of_apply_ne (of (φ := φ) j) (by simp_all)
have hg₁r : g₁ ∉ (φ i).range := by
rintro ⟨y, rfl⟩
subst hg₁
exact hx (of_apply_eq_base φ i y ▸ MonoidHom.mem_range.2 ⟨y, rfl⟩)
have hg₂r : g₂ ∉ (φ j).range := by
rintro ⟨y, rfl⟩
subst hg₂
exact hx (of_apply_eq_base φ j y ▸ MonoidHom.mem_range.2 ⟨y, rfl⟩)
let w : Word G := ⟨[⟨_, g₁⟩, ⟨_, g₂⁻¹⟩], by simp_all, by simp_all⟩
have hw : Reduced φ w := by
simp only [w, Reduced, List.mem_cons, forall_eq_or_imp, not_false_eq_true, hg₁r, hg₂r, List.mem_nil_iff,
false_imp_iff, imp_true_iff, and_true, inv_mem_iff]
have :=
hw.eq_empty_of_mem_range hφ
(by
simp only [w, Word.prod, List.map_cons, List.prod_cons, List.prod_nil, List.map_nil, map_mul, ofCoprodI_of,
hg₁, hg₂, map_inv, mul_one, mul_inv_cancel, one_mem])
simp [w, Word.empty] at this)
(le_inf
(by
rw [← of_comp_eq_base i]
rintro _ ⟨h, rfl⟩
exact MonoidHom.mem_range.2 ⟨φ i h, rfl⟩)
(by
rw [← of_comp_eq_base j]
rintro _ ⟨h, rfl⟩
exact MonoidHom.mem_range.2 ⟨φ j h, rfl⟩))
