finite_quotient_of_pretransitive_of_finite_quotient

English

If the action is pretransitive and the quotient α/H is finite, then the orbit relation quotient orbitRel.Quotient H β is finite.

Русский

Если действие предварительно транситивно и фактор-выражение α/H конечно, тогда орбитальная отношения в β конечна.

LaTeX

$$Finite (orbitRel.Quotient H β)$$

Lean4

@[to_additive]
instance finite_quotient_of_pretransitive_of_finite_quotient [IsPretransitive α β] {H : Subgroup α} [Finite (α ⧸ H)] :
    Finite <| orbitRel.Quotient H β :=
  by
  rcases isEmpty_or_nonempty β with he | ⟨⟨b⟩⟩
  · exact Quotient.finite _
  · have h' : Finite (Quotient (rightRel H)) := Finite.of_equiv _ (quotientRightRelEquivQuotientLeftRel _).symm
    let f : Quotient (rightRel H) → orbitRel.Quotient H β := fun a ↦
      Quotient.liftOn' a (fun g ↦ ⟦g • b⟧) fun g₁ g₂ r ↦
        by
        replace r := Setoid.symm' _ r
        rw [rightRel_eq] at r
        simp only [Quotient.eq, orbitRel_apply, mem_orbit_iff]
        exact ⟨⟨g₁ * g₂⁻¹, r⟩, by simp [mul_smul]⟩
    exact
      Finite.of_surjective f
        ((Quotient.surjective_liftOn' _).2 (Quotient.mk''_surjective.comp (MulAction.surjective_smul _ _)))

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