NYLL
Module

Flat.lean

Nyll.SchemeTheory.Pi1.Morphisms.Flat
3 declarations indexed from sourceView source ↗

Module documentation

Openness and immersion consequences of flatness

Flat ring maps of finite presentation induce open maps on prime spectra. Flat scheme morphisms with the stated finiteness, surjectivity, or monomorphism hypotheses give isomorphisms and open immersions.

Imports1
  • Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Imported by3

Declarations

lemma

isOpenMap_comap_of_finitePresentation

L40 ↗
RingHom.Flat.isOpenMap_comap_of_finitePresentation
Source context 4 commands

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

@[expose] public section
universe u v
open TensorProduct
open CategoryTheory Limits MorphismProperty
Lean source · statement
lemma RingHom.Flat.isOpenMap_comap_of_finitePresentation
    {R S : Type*} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.Flat)
    (hfin : f.FinitePresentation) :
    IsOpenMap (PrimeSpectrum.comap f)
instance

isIso

L49 ↗
AlgebraicGeometry.Flat.isIso
Source context 5 commands

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

@[expose] public section
universe u v
open TensorProduct
open CategoryTheory Limits MorphismProperty
namespace AlgebraicGeometry
Lean source · statement
instance (priority := low) Flat.isIso {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f]
    [QuasiCompact f] [Surjective f] [Mono f] : IsIso f
instance

isOpenImmersion

L53 ↗
AlgebraicGeometry.Flat.isOpenImmersion
Source context 5 commands

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

@[expose] public section
universe u v
open TensorProduct
open CategoryTheory Limits MorphismProperty
namespace AlgebraicGeometry
Lean source · statement
instance (priority := low) Flat.isOpenImmersion {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f]
    [LocallyOfFinitePresentation f] [Mono f] : IsOpenImmersion f

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.