range_awayMapAux_subset — Mathlib

English

A simplified form of nontriviality for AtPrime, expressing a basic nontriviality property.

Русский

Упрощенная форма не тривиальности для AtPrime, выражающая базовую не тривиальность.

LaTeX

$$$$ \text{Nontrivial.} (\mathrm{HomogeneousLocalization.AtPrime}(\mathcal{A}, \mathfrak{p})). $$$$

Lean4

theorem range_awayMapAux_subset : Set.range (awayMapAux 𝒜 (f := f) ⟨_, hx⟩) ⊆ Set.range (val (𝒜 := 𝒜)) :=
  by
  rintro _ ⟨z, rfl⟩
  obtain ⟨⟨n, ⟨a, ha⟩, ⟨b, hb'⟩, j, rfl : _ = b⟩, rfl⟩ := mk_surjective z
  use mk ⟨n + j • e, ⟨a * g ^ j, ?_⟩, ⟨x ^ j, ?_⟩, j, rfl⟩
  · simp [awayMapAux_mk 𝒜 (hx := hx)]
  · apply SetLike.mul_mem_graded ha
    exact SetLike.pow_mem_graded _ hg
  · rw [hx, mul_pow]
    apply SetLike.mul_mem_graded hb'
    exact SetLike.pow_mem_graded _ hg

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