Module

HorizontalEtale.lean

Nyll.SchemeTheory.Divisors.HorizontalEtale

1 declaration indexed from sourceView source ↗

Module documentation

Horizontal boundary components after finite etale pullback

Every irreducible component of the pullback of a horizontal boundary maps onto an irreducible component downstairs. Consequently its composite with the structural morphism has dense range. The statement is made directly for the pulled-back ideal sheaf, before packaging it as an effective Cartier divisor.

Imports1

Nyll.SchemeTheory.Divisors.ArithmeticBoundaryEtale

Imported by3

theorem

comap_components_denseRange_of_isHorizontalOver

L33 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.comap_components_denseRange_of_isHorizontalOver

Documentation

Horizontal irreducible components remain horizontal after finite etale pullback.

Source context 6 commands

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

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

Lean source · statement

theorem comap_components_denseRange_of_isHorizontalOver
    (D : EffectiveCartierDivisor X) (p : X ⟶ S)
    (f : Y ⟶ X) [IsFiniteEtale f] (hD : D.IsHorizontalOver p) :
    ∀ (Z : Set (D.1.comap f).subscheme)
      (hZ : Z ∈ irreducibleComponents (D.1.comap f).subscheme),
      DenseRange ((D.1.comap f).componentToBase (f ≫ p) Z hZ)

Module documentation

Horizontal boundary components after finite etale pullback

Declarations

comap_components_denseRange_of_isHorizontalOver