Module

ConnectedSourceToCoproduct.lean

Nyll.SchemeTheory.Etale.OverField.ConnectedSourceToCoproduct

3 declarations indexed from sourceView source ↗

Module documentation

Maps from a connected scheme to a coproduct

This file supplies the coproduct-fiber step used internally for Stacks Project, Tag 03QR. A morphism from a connected scheme to a coproduct factors through a unique summand, so its morphism set is the dependent sum of the morphism sets to the individual summands.

Imports3

Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.Topology.Connected.Clopen

Imported by2

def

homSigmaEquiv

L34 ↗

AlgebraicGeometry.Scheme.homSigmaEquiv

Documentation

Morphisms from a connected scheme to a coproduct are uniquely morphisms to one of its summands.

Source context 5 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme

Lean source · statement

def homSigmaEquiv {ι : Type u} (Y : ι → Scheme.{u})
    (Z : Scheme.{u}) [ConnectedSpace Z] :
    (Z ⟶ ∐ Y) ≃ Σ i, (Z ⟶ Y i)

theorem

homSigmaEquiv_symm_apply

L70 ↗

AlgebraicGeometry.Scheme.homSigmaEquiv_symm_apply

Source context 5 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme

Lean source · statement

theorem homSigmaEquiv_symm_apply {ι : Type u} (Y : ι → Scheme.{u})
    (Z : Scheme.{u}) [ConnectedSpace Z] (f : Σ i, (Z ⟶ Y i)) :
    (homSigmaEquiv Y Z).symm f = f.2 ≫ Sigma.ι Y f.1

theorem

homSigmaEquiv_comp

L77 ↗

AlgebraicGeometry.Scheme.homSigmaEquiv_comp

Documentation

The coproduct decomposition of morphisms is natural under precomposition. In particular, precomposition cannot change the selected summand.

Source context 5 commands

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

@[expose] public section
universe u
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme

Lean source · statement

theorem homSigmaEquiv_comp {ι : Type u} (Y : ι → Scheme.{u})
    {Z Z' : Scheme.{u}} [ConnectedSpace Z] [ConnectedSpace Z']
    (f : Z' ⟶ Z) (g : Z ⟶ ∐ Y) :
    homSigmaEquiv Y Z' (f ≫ g) =
      ⟨(homSigmaEquiv Y Z g).1, f ≫ (homSigmaEquiv Y Z g).2⟩

Module documentation

Maps from a connected scheme to a coproduct

Declarations

homSigmaEquiv

homSigmaEquiv_symm_apply

homSigmaEquiv_comp