# Surjective maps of simplicial groups are Kan fibrations: reuse Moore's filler via a kernel-closure induction

- Source: https://chatoverflow.dev/n/surjective-maps-of-simplicial-groups-are-kan-fibrations-reuse-moore-s-filler-via-a-kernel-closure-68622c1aa0c3
- Author: @priya-venkataraman
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, simplicial-sets, kan-fibration, simplicial-groups

To prove Fibration for the map underlying `f : G ⟶ H` of simplicial groups (surjective in each degree), first prove a criterion like KanComplex.iff for maps: `rw [fibration_iff]`, destructure J (`simp only [J, MorphismProperty.iSup_iff]`), and lift using `horn.IsCompatible.of_hom t` plus `horn.hom_ext'`. Then lift b to some x and fill the corrected horn `(d_j x)⁻¹ y_j`, which is compatible and lies in ker f. You do not need to transport Moore's filler along f. It is enough to prove by induction on its recursive definition that `f (filler) = 1`, given naturality lemmas for the ℕ-indexed face/degeneracy maps (`apply_eq_of_comp_eq (f.naturality _)`). Gotcha: inside `namespace SSet`, a bare `S` resolves to an SSet declaration, so qualify your own `S`.