NYLL
Module

UniversalHomeomorphismFullyFaithful.lean

Nyll.SchemeTheory.FiniteEtale.UniversalHomeomorphismFullyFaithful
7 declarations indexed from sourceView source ↗

Module documentation

Fully faithful finite étale pullback along universal homeomorphisms

Étale sections descend along integral, universally injective, surjective morphisms. Applying section descent after pullback by the source object gives fullness. Relative maps into a separated unramified scheme are determined after a surjective morphism, giving faithfulness.

Imports5
Imported by5

Declarations

instance

finiteEtaleInfStableUnderBaseChangeUniversalHomeomorphism

L32 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleInfStableUnderBaseChangeUniversalHomeomorphism
Source context 4 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
Lean source · statement
instance finiteEtaleInfStableUnderBaseChangeUniversalHomeomorphism :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale)
instance

finiteEtaleInfStableUnderBaseChangeAlongUniversalHomeomorphism

L37 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleInfStableUnderBaseChangeAlongUniversalHomeomorphism
Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeUniversalHomeomorphism :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
Lean source · statement
instance finiteEtaleInfStableUnderBaseChangeAlongUniversalHomeomorphism
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) f
theorem

pullback_map_surjective_of_integral_universallyInjective_surjective

L46 ↗
AlgebraicGeometry.FiniteEtale.pullback_map_surjective_of_integral_universallyInjective_surjective
Documentation

Pullback along a universal homeomorphism is surjective on maps into any étale object of the slice, with an arbitrary source object.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeUniversalHomeomorphism :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
local instance finiteEtaleInfStableUnderBaseChangeAlongUniversalHomeomorphism
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale)) h hf⟩
Lean source · statement
theorem pullback_map_surjective_of_integral_universallyInjective_surjective
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsIntegralHom f] [UniversallyInjective f] [Surjective f]
    (T V : CategoryTheory.Over Y) [Etale V.hom] :
    Function.Surjective ((CategoryTheory.Over.pullback f).map (X := T) (Y := V))
theorem

pullback_map_bijective_of_integral_universallyInjective_surjective

L76 ↗
AlgebraicGeometry.FiniteEtale.pullback_map_bijective_of_integral_universallyInjective_surjective
Documentation

Maps into a separated étale object are invariant under universal homeomorphisms, even when the source object is arbitrary.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeUniversalHomeomorphism :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
local instance finiteEtaleInfStableUnderBaseChangeAlongUniversalHomeomorphism
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale)) h hf⟩
Lean source · statement
theorem pullback_map_bijective_of_integral_universallyInjective_surjective
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsIntegralHom f] [UniversallyInjective f] [Surjective f]
    (T V : CategoryTheory.Over Y) [Etale V.hom] [IsSeparated V.hom] :
    Function.Bijective ((CategoryTheory.Over.pullback f).map (X := T) (Y := V))
theorem

pullback_full_of_integral_universallyInjective_surjective

L96 ↗
AlgebraicGeometry.FiniteEtale.pullback_full_of_integral_universallyInjective_surjective
Documentation

Finite étale pullback along a universal homeomorphism is full.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeUniversalHomeomorphism :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
local instance finiteEtaleInfStableUnderBaseChangeAlongUniversalHomeomorphism
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale)) h hf⟩
Lean source · statement
theorem pullback_full_of_integral_universallyInjective_surjective
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsIntegralHom f] [UniversallyInjective f] [Surjective f] :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ f).Full
theorem

pullback_faithful_of_integral_universallyInjective_surjective

L111 ↗
AlgebraicGeometry.FiniteEtale.pullback_faithful_of_integral_universallyInjective_surjective
Documentation

Finite étale pullback along a universal homeomorphism is faithful.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeUniversalHomeomorphism :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
local instance finiteEtaleInfStableUnderBaseChangeAlongUniversalHomeomorphism
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale)) h hf⟩
Lean source · statement
theorem pullback_faithful_of_integral_universallyInjective_surjective
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsIntegralHom f] [UniversallyInjective f] [Surjective f] :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ f).Faithful
def

pullback_fullyFaithful_of_integral_universallyInjective_surjective

L127 ↗
AlgebraicGeometry.FiniteEtale.pullback_fullyFaithful_of_integral_universallyInjective_surjective
Documentation

The fully faithful structure for finite étale pullback along a universal homeomorphism.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeUniversalHomeomorphism :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
local instance finiteEtaleInfStableUnderBaseChangeAlongUniversalHomeomorphism
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale)) h hf⟩
Lean source · statement
def pullback_fullyFaithful_of_integral_universallyInjective_surjective
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsIntegralHom f] [UniversallyInjective f] [Surjective f] :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ f).FullyFaithful

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