toSpecΓ_unop — Mathlib

English

A simp-normal form of counit evaluation: mapping of the opposite of a ring R to SpecΓ.

Русский

Упрощённая форма значения counit: отображение Opposite кольца R в SpecΓ.

LaTeX

$$$toSpecΓ(\operatorname{Opposite.unop} R) = toOpen(R.unop)$.$$

Lean4

/-- `@[simp]`-normal form of `locallyRingedSpaceAdjunction_counit_app`. -/
@[simp]
theorem toSpecΓ_unop (R : CommRingCatᵒᵖ) : AlgebraicGeometry.toSpecΓ (Opposite.unop R) = toOpen R.unop ⊤ :=
  rfl

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