English
A mirrored instance ensuring finiteness for the open normal subgroup stages of stabilizerHomSurjectiveAuxFunctor.
Русский
Зеркальное доказательство конечности на стадиях открытой нормальной подгруппы для stabilizerHomSurjectiveAuxFunctor.
LaTeX
$$Finite ((stabilizerHomSurjectiveAuxFunctor P Q σ).obj N)$$
Lean4
/-- (Implementation)
The functor taking an open normal subgroup `N ≤ G` to the set of lifts of `σ` in `G ⧸ N`.
We will show that its inverse limit is nonempty to conclude that there exists a lift in `G`. -/
def stabilizerHomSurjectiveAuxFunctor (P : Ideal A) (Q : Ideal B) [Q.LiesOver P] (σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q) :
OpenNormalSubgroup G ⥤ Type _
where
obj
N :=
letI B' := FixedPoints.subalgebra A B N.1.1
letI f : (B' ⧸ Q.under B') →ₐ[A ⧸ P] B ⧸ Q :=
{ toRingHom := Ideal.quotientMap _ B'.subtype le_rfl, commutes' := Quotient.ind fun _ ↦ rfl }
{ σ' // f.comp (Ideal.Quotient.stabilizerHom (Q.under B') P (G ⧸ N.1.1) σ') = σ.toAlgHom.comp f }
map {N N'} i
x :=
⟨⟨(QuotientGroup.map _ _ (.id _) (leOfHom i)) x.1,
Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor_aux Q i.le x.1.1 x.1.2⟩,
by
have h : FixedPoints.subalgebra A B N'.1.1 ≤ FixedPoints.subalgebra A B N.1.1 := fun x hx n ↦ hx ⟨_, i.le n.2⟩
obtain ⟨⟨x, hx⟩, hx'⟩ := x
obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x
ext g
obtain ⟨g, rfl⟩ := Ideal.Quotient.mk_surjective g
exact DFunLike.congr_fun hx' (Ideal.Quotient.mk _ (Subalgebra.inclusion h g))⟩
map_id N := by ext ⟨⟨⟨x⟩, hx⟩, hx'⟩; rfl
map_comp f g := by ext ⟨⟨⟨x⟩, hx⟩, hx'⟩; rfl
