Module

IrreducibleComponentMap.lean

Nyll.SchemeTheory.Divisors.IrreducibleComponentMap

7 declarations indexed from sourceView source ↗

Module documentation

Morphisms between reduced irreducible components

This file constructs the induced morphism between the reduced closed subschemes carried by irreducible components. It also supplies the reverse component-lifting statement for surjective closed generalizing maps.

Imports3

Imported by3

lemma

exists_irreducibleComponent_image_eq_of_surjective

L29 ↗

TopologicalSpace.exists_irreducibleComponent_image_eq_of_surjective

Documentation

For a surjective closed generalizing map, every irreducible component of the target is the image of an irreducible component of the source.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace TopologicalSpace
universe u v

Lean source · statement

lemma exists_irreducibleComponent_image_eq_of_surjective
    {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y]
    [T0Space X] [QuasiSober X] [QuasiSober Y]
    {f : X → Y} (hfc : Continuous f) (hfclosed : IsClosedMap f)
    (hfgeneral : GeneralizingMap f) (hfsurj : Function.Surjective f)
    (W : Set Y) (hW : W ∈ irreducibleComponents Y) :
    ∃ Z : Set X, Z ∈ irreducibleComponents X ∧ f '' Z = W

instance

reducedIrreducibleComponent_isReduced

L66 ↗

AlgebraicGeometry.Scheme.reducedIrreducibleComponent_isReduced

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable {X Y : Scheme.{u}}

Lean source · statement

instance reducedIrreducibleComponent_isReduced
    (X : Scheme.{u}) (Z : Set X) (hZ : Z ∈ irreducibleComponents X) :
    AlgebraicGeometry.IsReduced (X.reducedIrreducibleComponent Z hZ)

def

reducedIrreducibleComponentMap

L80 ↗

AlgebraicGeometry.Scheme.reducedIrreducibleComponentMap

Documentation

The morphism between reduced irreducible components induced by a morphism whose image on the chosen source component is the chosen target component.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable {X Y : Scheme.{u}}

Lean source · statement

def reducedIrreducibleComponentMap (f : X ⟶ Y)
    (Z : Set X) (hZ : Z ∈ irreducibleComponents X)
    (W : Set Y) (hW : W ∈ irreducibleComponents Y)
    (himage : f '' Z = W) :
    X.reducedIrreducibleComponent Z hZ ⟶
      Y.reducedIrreducibleComponent W hW

lemma

reducedIrreducibleComponentMap_ι

L102 ↗

AlgebraicGeometry.Scheme.reducedIrreducibleComponentMap_ι

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable {X Y : Scheme.{u}}

Lean source · statement

lemma reducedIrreducibleComponentMap_ι (f : X ⟶ Y)
    (Z : Set X) (hZ : Z ∈ irreducibleComponents X)
    (W : Set Y) (hW : W ∈ irreducibleComponents Y)
    (himage : f '' Z = W) :
    X.reducedIrreducibleComponentMap f Z hZ W hW himage ≫
        Y.reducedIrreducibleComponentι W hW =
      X.reducedIrreducibleComponentι Z hZ ≫ f

instance

(anonymous instance)

L116 ↗

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable {X Y : Scheme.{u}}

Lean source · statement

instance (f : X ⟶ Y) [IsFinite f]
    (Z : Set X) (hZ : Z ∈ irreducibleComponents X)
    (W : Set Y) (hW : W ∈ irreducibleComponents Y)
    (himage : f '' Z = W) :
    IsFinite (X.reducedIrreducibleComponentMap f Z hZ W hW himage)

lemma

reducedIrreducibleComponentMap_surjective

L130 ↗

AlgebraicGeometry.Scheme.reducedIrreducibleComponentMap_surjective

Documentation

If the image of the chosen source component is the chosen target component, the induced morphism of reduced components is surjective.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable {X Y : Scheme.{u}}

Lean source · statement

lemma reducedIrreducibleComponentMap_surjective (f : X ⟶ Y)
    (Z : Set X) (hZ : Z ∈ irreducibleComponents X)
    (W : Set Y) (hW : W ∈ irreducibleComponents Y)
    (himage : f '' Z = W) :
    Function.Surjective
      (X.reducedIrreducibleComponentMap f Z hZ W hW himage)

instance

(anonymous instance)

L156 ↗

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable {X Y : Scheme.{u}}

Lean source · statement

instance (f : X ⟶ Y)
    (Z : Set X) (hZ : Z ∈ irreducibleComponents X)
    (W : Set Y) (hW : W ∈ irreducibleComponents Y)
    (himage : f '' Z = W) :
    Surjective (X.reducedIrreducibleComponentMap f Z hZ W hW himage)

Module documentation

Morphisms between reduced irreducible components

Declarations

exists_irreducibleComponent_image_eq_of_surjective

reducedIrreducibleComponent_isReduced

reducedIrreducibleComponentMap

reducedIrreducibleComponentMap_ι

(anonymous instance)

reducedIrreducibleComponentMap_surjective

(anonymous instance)