NYLL
Module

bijective_app_of_isProper_of_flat_of_forall_bijective_appTop_fiberToSpecResidueField.lean

Nyll.AlgebraicCurves.Geometry.Schemes.bijective_app_of_isProper_of_flat_of_forall_bijective_appTop_fiberToSpecResidueField
3 declarations indexed from sourceView source ↗

Module documentation

bijective app of is Proper of flat of forall bijective app Top fiber To Spec Residue Field

Imports22
Imported by2

Declarations

theorem

bijective_appTop_of_iso

L85 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_app_of_isProper_of_flat_of_forall_bijective_appTop_fiberToSpecResidueField.H0AuxGen.bijective_appTop_of_iso
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_app_of_isProper_of_flat_of_forall_bijective_appTop_fiberToSpecResidueField
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
  IsDirectLimit.Module.instDirectLimitCoeLinearMapIdOfOfNonempty
  AlgebraicGeometry.ChowDatum.hι_closed AlgebraicGeometry.ChowDatumProj.hιN_closed
  AlgebraicGeometry.ChowDatumProj.hp_proper AlgebraicGeometry.ChowDatum.hp_isoU
  AlgebraicGeometry.ChowDatum.hp_proper AlgebraicGeometry.ProjSpace.algebraAway
  AlgebraicGeometry.ProjSpace.instIsProperProdOverπ AlgebraicGeometry.ChowDatumProj.hp_isoU
  AlgebraicGeometry.ProjSpace.isProper_π AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
  AdicCompletion.instIsLocalRingMaximalIdeal
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans IsDirectLimit.Module.linearEquiv_symm_apply
  IsDirectLimit.linearEquiv_symm_apply IsDirectLimit.lift_of IsDirectLimit.Module.linearEquiv_apply
  IsDirectLimit.Module.lift_of IsDirectLimit.Equiv_apply
  AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec AlgebraicGeometry.ChowDatum.mk.sizeOf_spec
  AlgebraicGeometry.ChowDatumProj.mk.injEq AlgebraicGeometry.ChowDatum.mk.injEq
open AlgebraicGeometry CategoryTheory
universe u
open CategoryTheory.Limits TopologicalSpace
namespace H0AuxGen
Lean source · statement
theorem bijective_appTop_of_iso {P P' Y : Scheme.{u}} (e : P ≅ P') (s : P ⟶ Y) (s' : P' ⟶ Y) (w :
  e.hom ≫ s' = s)
    (h : Function.Bijective s'.appTop) : Function.Bijective s.appTop
theorem

bijective_appTop_of_affine

L97 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_app_of_isProper_of_flat_of_forall_bijective_appTop_fiberToSpecResidueField.H0AuxGen.bijective_appTop_of_affine
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_app_of_isProper_of_flat_of_forall_bijective_appTop_fiberToSpecResidueField
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
  IsDirectLimit.Module.instDirectLimitCoeLinearMapIdOfOfNonempty
  AlgebraicGeometry.ChowDatum.hι_closed AlgebraicGeometry.ChowDatumProj.hιN_closed
  AlgebraicGeometry.ChowDatumProj.hp_proper AlgebraicGeometry.ChowDatum.hp_isoU
  AlgebraicGeometry.ChowDatum.hp_proper AlgebraicGeometry.ProjSpace.algebraAway
  AlgebraicGeometry.ProjSpace.instIsProperProdOverπ AlgebraicGeometry.ChowDatumProj.hp_isoU
  AlgebraicGeometry.ProjSpace.isProper_π AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
  AdicCompletion.instIsLocalRingMaximalIdeal
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans IsDirectLimit.Module.linearEquiv_symm_apply
  IsDirectLimit.linearEquiv_symm_apply IsDirectLimit.lift_of IsDirectLimit.Module.linearEquiv_apply
  IsDirectLimit.Module.lift_of IsDirectLimit.Equiv_apply
  AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec AlgebraicGeometry.ChowDatum.mk.sizeOf_spec
  AlgebraicGeometry.ChowDatumProj.mk.injEq AlgebraicGeometry.ChowDatum.mk.injEq
open AlgebraicGeometry CategoryTheory
universe u
open CategoryTheory.Limits TopologicalSpace
namespace H0AuxGen
open _root_.AlgebraicGeometry in
Lean source · statement
theorem bijective_appTop_of_affine {X : Scheme.{u}} {R : CommRingCat.{u}}
    (q : X ⟶ Spec R) [IsProper q] [Flat q] [LocallyOfFinitePresentation q]
    (h : ∀ {K : Type u} [Field K] (k : Spec (CommRingCat.of K) ⟶ Spec R), Function.Bijective
      (pullback.snd q k).appTop) :
    Function.Bijective q.appTop
theorem

bijective_app_of_isProper_of_flat_of_forall_bijective_appTop_fiberToSpecResidueField

L151 ↗
AlgebraicGeometry.bijective_app_of_isProper_of_flat_of_forall_bijective_appTop_fiberToSpecResidueField
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicGeometry
universe u
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open bijective_app_of_isProper_of_flat_of_forall_bijective_appTop_fiberToSpecResidueField in
open AlgebraicGeometry CategoryTheory in
open CategoryTheory.Limits TopologicalSpace in
Lean source · statement
theorem bijective_app_of_isProper_of_flat_of_forall_bijective_appTop_fiberToSpecResidueField
    {X B : Scheme.{u}} (p : X ⟶ B) [IsProper p] [Flat p] [LocallyOfFinitePresentation p]
    (h : ∀ b : B, Function.Bijective (p.fiberToSpecResidueField b).appTop) (U : B.Opens) :
    Function.Bijective (p.app U)

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