instFiniteObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor

English

There exists at least one element in the stabilizer-specified object at each stage, i.e., the object (stabilizerHomSurjectiveAuxFunctor P Q σ).obj N is nonempty.

Русский

Существует по крайней мере одна точка в объекте стабилизатора на каждой стадии: (stabilizerHomSurjectiveAuxFunctor P Q σ).obj N ≠ ∅.

LaTeX

$$Nonempty ((stabilizerHomSurjectiveAuxFunctor P Q σ).obj N)$$

Lean4

instance (P : Ideal A) (Q : Ideal B) [Q.LiesOver P] (σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q) (N : OpenNormalSubgroup G) :
    Finite ((stabilizerHomSurjectiveAuxFunctor P Q σ).obj N) :=
  by
  dsimp [stabilizerHomSurjectiveAuxFunctor]
  infer_instance

Похожие утверждения