Module

FiniteOpenFactor.lean

Nyll.SchemeTheory.RingTheory.FiniteOpenFactor

1 declaration indexed from sourceView source ↗

Module documentation

A finite open affine factor is a quotient

If an affine open subscheme is finite over a common base, its map into any intermediate affine scheme is finite. An open immersion is a monomorphism, so the corresponding finite ring epimorphism is surjective. Together with the idempotent quotient decomposition this extracts an actual algebra factor.

Imports4

Mathlib.Algebra.Category.Ring.Epi
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Mathlib.CategoryTheory.EpiMono

Imported by2

theorem

surjective_of_finite_of_isOpenImmersion

L33 ↗

AlgHom.surjective_of_finite_of_isOpenImmersion

Documentation

An algebra map inducing an open immersion on spectra is surjective if its target is finite over the common base. The source need not be finite.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgHom

Lean source · statement

theorem surjective_of_finite_of_isOpenImmersion
    {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B] [Module.Finite R B] (f : A →ₐ[R] B)
    [IsOpenImmersion (Spec.map (CommRingCat.ofHom f.toRingHom))] :
    Function.Surjective f

Module documentation

A finite open affine factor is a quotient

Declarations

surjective_of_finite_of_isOpenImmersion