instIsIsoSchemeOverInferInstanceOverClassOfIsEmpty

English

If n is empty, the affine space 𝔸(n; S) over S is canonically isomorphic to S; the base projection is an isomorphism.

Русский

Если тип n пуст, то аффинное пространство над S эквивалентно S; базовая проекция является изоморфизмом.

LaTeX

$$$\text{If } n=\varnothing,\; (\mathbb{A}(n;S) \downarrow S) \cong S$$$

Lean4

instance [IsEmpty n] : IsIso (𝔸(n; S) ↘ S) :=
  pullback_fst (P := isomorphisms _) _ _ <|
    by
    rw [← terminal.comp_from (Spec.map (CommRingCat.ofHom C))]
    apply IsStableUnderComposition.comp_mem
    · rw [HasAffineProperty.iff_of_isAffine (P := isomorphisms _), ← isomorphisms, ←
        arrow_mk_iso_iff (isomorphisms _) (arrowIsoΓSpecOfIsAffine _)]
      exact ⟨inferInstance, (ConcreteCategory.isIso_iff_bijective _).mpr ⟨C_injective n _, C_surjective _⟩⟩
    · exact isIso_of_isTerminal specULiftZIsTerminal terminalIsTerminal (terminal.from _)

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