instNonemptyObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor

English

If A ⊆ B is invariant under the action of a finite group G, the induced invariants form an integral extension and behave well with field of fractions in the invariant setting.

Русский

Если A ⊆ B инвариантна относительно действия конечной группы G, образованные инварианты образуют целое расширение и ведут себя корректно в поле дробей в инвариантной настройке.

LaTeX

$$$[A,B,G] \\text{IsInvariant} \\Rightarrow \\text{IsIntegral} A B$$$

Lean4

instance (P : Ideal A) (Q : Ideal B) [Q.IsPrime] [Q.LiesOver P] [Algebra.IsInvariant A B G]
    (σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q) (N : OpenNormalSubgroup G) :
    Nonempty ((stabilizerHomSurjectiveAuxFunctor P Q σ).obj N) :=
  by
  have :
    IsScalarTower (A ⧸ P) (FixedPoints.subalgebra A B N.1.1 ⧸ Q.under (FixedPoints.subalgebra A B N.1.1)) (B ⧸ Q) :=
    IsScalarTower.of_algebraMap_eq (Quotient.ind fun x ↦ rfl)
  obtain ⟨σ', hσ'⟩ :=
    Ideal.Quotient.exists_algEquiv_fixedPoint_quotient_under (G ⧸ N.1.1) P (Q.under (FixedPoints.subalgebra A B N.1.1))
      σ
  obtain ⟨τ, rfl⟩ :=
    Ideal.Quotient.stabilizerHom_surjective (G ⧸ N.1.1) P (Q.under (FixedPoints.subalgebra A B N.1.1)) σ'
  refine ⟨τ, ?_⟩
  ext x
  obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
  exact hσ' x

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