instSurjectiveOverSchemeInferInstanceOverClass

English

The projection 𝔸(n; S) ↓ S is a surjective morphism of schemes (for any finite n).

Русский

Проекция 𝔸(n; S) ↓ S является сюръективным морфизмом схем (для любого конечного n).

LaTeX

$$$\\text{Surjective}(\\mathbb{A}(n; S) \\downarrow S).$$$

Lean4

instance : Surjective (𝔸(n; S) ↘ S) :=
  MorphismProperty.pullback_fst _ _ <|
    by
    have := isIso_of_isTerminal specULiftZIsTerminal terminalIsTerminal (terminal.from _)
    rw [← terminal.comp_from (Spec.map (CommRingCat.ofHom C)),
      MorphismProperty.cancel_right_of_respectsIso (P := @Surjective)]
    exact ⟨MvPolynomial.comap_C_surjective⟩

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