exists_smul_of_under_eq_of_profinite

English

A technical lemma about the auxiliary functor stabilizerHomSurjectiveAuxFunctor: given Q and open normal subgroups N ≤ N', the image under a quotient map preserves stabilizers along the inclusion.

Русский

Техническая лемма о вспомогательном функторе stabilizerHomSurjectiveAuxFunctor: при данных Q и открытых нормальных подгруппах N ≤ N', образ по кватернирующему отображению сохраняет стабилизаторы во включении.

LaTeX

$$$\\forall Q:\\text{Ideal } B,\\ N\\le N':\\; \\operatorname{QuotientGroup.map}(...)\n \\big( \\operatorname{MulAction.stabilizer} (G/N') (Q.under (FixedPoints.subalgebra A B N'.1.1)) \\big) \\subseteq \\mathrm{...}$$$

Lean4

/-- `G` acts transitively on the prime ideals of `B` above a given prime ideal of `A`. -/
theorem exists_smul_of_under_eq_of_profinite [Algebra.IsInvariant A B G] (P Q : Ideal B) [P.IsPrime] [Q.IsPrime]
    (hPQ : P.under A = Q.under A) : ∃ g : G, Q = g • P :=
  by
  let B' := FixedPoints.subalgebra A B
  let F : OpenNormalSubgroup G ⥤ Type _ :=
    { obj N := { g : G ⧸ N.1.1 // Q.under (B' N.1.1) = g • P.under (B' N.1.1) }
      map {N N'} f
        x :=
        ⟨(QuotientGroup.map _ _ (.id _) (leOfHom f)) x.1,
          by
          have h : B' N'.1.1 ≤ B' N.1.1 := fun x hx n ↦ hx ⟨_, f.le n.2⟩
          obtain ⟨x, hx⟩ := x
          obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x
          simpa only [Ideal.comap_comap, Ideal.pointwise_smul_eq_comap, ← Ideal.comap_coe (F := RingEquiv _ _)] using
            congr(Ideal.comap (Subalgebra.inclusion h).toRingHom $hx)⟩
      map_id N := by ext ⟨⟨x⟩, hx⟩; rfl
      map_comp f g := by ext ⟨⟨x⟩, hx⟩; rfl }
  have (N : _) : Nonempty (F.obj N) :=
    by
    obtain ⟨g, hg⟩ := Algebra.IsInvariant.exists_smul_of_under_eq A (B' N.1.1) (G ⧸ N.1.1) (P.under _) (Q.under _) hPQ
    exact ⟨g, hg⟩
  obtain ⟨s, hs⟩ := nonempty_sections_of_finite_cofiltered_system F
  let a :=
    (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv.hom
      ⟨fun N ↦ (s N).1, (fun {N N'} f ↦ congr_arg Subtype.val (hs f))⟩
  have (N : OpenNormalSubgroup G) : QuotientGroup.mk (s := N.1.1) a = s N :=
    by
    change ((ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.hom.hom a).1 N = _
    simp only [a]
    rw [← ProfiniteGrp.comp_apply, Iso.inv_hom_id]
    simp
  refine ⟨a, ?_⟩
  ext x
  obtain ⟨N, hN⟩ := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one (stabilizer_isOpen G x) (one_mem _)
  lift x to B' N.1.1 using fun g ↦ hN g.2
  change x ∈ Q.under (B' N.1.1) ↔ x ∈ Ideal.under (B' N.1.1) ((_ : G) • P)
  rw [(s N).2]
  simp only [Ideal.comap_comap, Ideal.pointwise_smul_eq_comap, ← Ideal.comap_coe (F := RingEquiv _ _)]
  congr! 2
  ext y
  simp [← this]
  rfl

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