English
If all φ_i are injective, then each canonical inclusion of G_i into the pushout (the map of i) is itself injective.
Русский
Если все φ_i инъективны, то каждое встроение G_i в пушаут (отображение i) инъективно.
LaTeX
$$$$\\forall i, \\; \\mathrm{Injective} (\\mathrm{of}\; i).$$$$
Lean4
/-- All maps into the `PushoutI`, or amalgamated product of groups are injective,
provided all maps in the diagram are injective.
See also `base_injective` -/
theorem of_injective (hφ : ∀ i, Function.Injective (φ i)) (i : ι) : Function.Injective (of (φ := φ) i) :=
by
rcases transversal_nonempty φ hφ with ⟨d⟩
let _ := Classical.decEq ι
let _ := fun i => Classical.decEq (G i)
refine Function.Injective.of_comp (f := ((· • ·) : PushoutI φ → NormalWord d → NormalWord d)) ?_
intro _ _ h
exact eq_of_smul_eq_smul (fun w : NormalWord d => by simp_all [funext_iff, of_smul_eq_smul])
