isArithFrobAt_localize — Mathlib

English

If φ is a Frobenius endomorphism at Q, then its localization is also a Frobenius endomorphism at the maximal ideal of the localized ring (i.e., at the local setting around Q).

Русский

Если φ — Фробениус-отображение по Q, то его локализация также является Фробениус-отображением в локализованной обстановке по максимальному идеалу локализации.

LaTeX

$$H.localize.IsArithFrobAt (IsLocalRing.maximalIdeal (Localization.AtPrime Q))$$

Lean4

theorem isArithFrobAt_localize [Q.IsPrime] : H.localize.IsArithFrobAt (maximalIdeal _) :=
  by
  have h : Nat.card (R ⧸ (maximalIdeal _).comap (algebraMap R (Localization.AtPrime Q))) = Nat.card (R ⧸ Q.under R) :=
    by
    congr 2
    rw [IsScalarTower.algebraMap_eq R S (Localization.AtPrime Q), ← Ideal.comap_comap,
      Localization.AtPrime.comap_maximalIdeal]
  intro x
  obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective Q.primeCompl x
  simp only [localize, coe_mk, Localization.localRingHom_mk', RingHom.coe_coe, h, ← IsLocalization.mk'_pow]
  rw [← IsLocalization.mk'_sub, IsLocalization.AtPrime.mk'_mem_maximal_iff (Localization.AtPrime Q) Q]
  simp only [SubmonoidClass.coe_pow, ← Ideal.Quotient.eq_zero_iff_mem]
  simp [H.mk_apply]

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