mem_carrier_iff' — Mathlib

English

Full variant of mem-carrier lemmas combining mem_mul, power-degree relations and localization maps.

Русский

Полная версия лемм mem-carrier, сочетающая mem_mul, связи степеней и локализационные отображения.

LaTeX

$$$\text{mem_carrier_iff_of_mem_mul}$ (full)$$

Lean4

theorem mem_carrier_iff' (q : Spec.T A⁰_ f) (a : A) :
    a ∈ carrier f_deg q ↔
      ∀ i,
        (Localization.mk (proj 𝒜 i a ^ m) ⟨f ^ i, ⟨i, rfl⟩⟩ : Localization.Away f) ∈
          algebraMap (HomogeneousLocalization.Away 𝒜 f) (Localization.Away f) '' {s | s ∈ q.1} :=
  (mem_carrier_iff f_deg q a).trans
    (by
      constructor <;> intro h i <;> specialize h i
      · rw [Set.mem_image]; refine ⟨_, h, rfl⟩
      · rw [Set.mem_image] at h; rcases h with ⟨x, h, hx⟩
        change x ∈ q.asIdeal at h
        convert h
        rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk]
        dsimp only [Subtype.coe_mk]; rw [← hx]; rfl)

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