English
There is an instance showing that the coindFunctor along a subgroup subtype preserves epimorphisms, i.e., surjective maps remain surjective after coinduction along the subgroup embedding.
Русский
Существует экземпляр, доказывающий, что коинд-функтор вдоль подгруппы сохраняет эпиморфизмы, то есть сюръективные отображения сохраняются после коиндукции вдоль вложения подгруппы.
LaTeX
$$$\text{coindFunctor } k S.\text{subtype} \text{ preserves epi}$$$
Lean4
instance {G : Type u} [Group G] (S : Subgroup G) : (coindFunctor k S.subtype).PreservesEpimorphisms where
preserves {X Y}
f :=
(Rep.epi_iff_surjective _).2 fun y => by
letI := QuotientGroup.rightRel S
choose! s hs using (Rep.epi_iff_surjective f).1 ‹_›
choose! i hi using Quotient.mk'_surjective (α := G)
let γ (g : G) : S :=
⟨g * (i (Quotient.mk' g))⁻¹, (QuotientGroup.rightRel_apply.1 (Quotient.eq'.1 (hi (Quotient.mk' g))))⟩
have hmk (s : S) (g : G) : Quotient.mk' (s.1 * g) = Quotient.mk' g :=
Quotient.eq'.2 (QuotientGroup.rightRel_apply.2 (by simp))
have hγ (s : S) (g : G) : γ (s.1 * g) = s * γ g := by ext; simp [mul_assoc, γ, hmk]
let x (g : G) : X := X.ρ (γ g) (s (y.1 (i (Quotient.mk' g))))
refine ⟨⟨x, fun _ _ => ?_⟩, Subtype.ext <| funext fun g => ?_⟩
· simp [x, ← Module.End.mul_apply, ← map_mul, hmk, hγ]
· simp_all [x, hom_comm_apply, ← y.2 (γ g), γ]
