English
For any P,Q with Q lying over P, and any σ, the object (stabilizerHomSurjectiveAuxFunctor P Q σ).obj N is finite for every OpenNormalSubgroup N.
Русский
Для любых P,Q с тем, что Q лежит над P, и любого σ, объект (stabilizerHomSurjectiveAuxFunctor P Q σ).obj N конечен для каждой открытой нормальной подгруппы N.
LaTeX
$$Finite ((stabilizerHomSurjectiveAuxFunctor P Q σ).obj N)$$
Lean4
theorem stabilizerHomSurjectiveAuxFunctor_aux (Q : Ideal B) {N N' : OpenNormalSubgroup G} (e : N ≤ N') (x : G ⧸ N.1.1)
(hx : x ∈ MulAction.stabilizer (G ⧸ N.1.1) (Q.under (FixedPoints.subalgebra A B N.1.1))) :
QuotientGroup.map _ _ (.id _) e x ∈
MulAction.stabilizer (G ⧸ N'.1.1) (Q.under (FixedPoints.subalgebra A B N'.1.1)) :=
by
change _ = _
have h : FixedPoints.subalgebra A B N'.1.1 ≤ FixedPoints.subalgebra A B N.1.1 := fun x hx n ↦ hx ⟨_, e n.2⟩
obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x
replace hx := congr(Ideal.comap (Subalgebra.inclusion h) $hx)
simpa only [Ideal.pointwise_smul_eq_comap, ← Ideal.comap_coe (F := RingEquiv _ _), Ideal.comap_comap] using hx
