NYLL
Module

bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing.lean

Nyll.AlgebraicCurves.Geometry.Schemes.bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing
7 declarations indexed from sourceView source ↗

Module documentation

bijective app Top of is Proper of flat of locally Of Finite Presentation of is Local Ring

Imports27
Imported by3

Declarations

theorem

bijective_appTop_of_iso

L68 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing.NewLocalAux.bijective_appTop_of_iso
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing
attribute [-instance] 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] 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 CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
universe u
namespace NewLocalAux
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_ΓSpecIso_inv_comp_iff

L79 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing.NewLocalAux.bijective_ΓSpecIso_inv_comp_iff
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing
attribute [-instance] 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] 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 CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
universe u
namespace NewLocalAux
Lean source · statement
theorem bijective_ΓSpecIso_inv_comp_iff {R : CommRingCat.{u}} {X : Scheme.{u}} (f : X ⟶ Spec R) :
    Function.Bijective ((Scheme.ΓSpecIso R).inv ≫ f.appTop).hom ↔ Function.Bijective f.appTop
def

resMap

L92 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing.NewLocalAux.resMap
Documentation

The residue-field homomorphism induced by the local subalgebra inclusion.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing
attribute [-instance] 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] 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 CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
universe u
namespace NewLocalAux
section stage
variable {T : Type u} [CommRing T] {R : Type u} [CommRing R] [IsLocalRing R] [Algebra T R]
  (S : Subalgebra T R) [IsLocalRing ↥S] (hunit : ∀ x : ↥S, IsUnit x ↔ IsUnit (x : R))
Lean source · statement
def resMap : (↥S ⧸ IsLocalRing.maximalIdeal ↥S) →+* (R ⧸ IsLocalRing.maximalIdeal R)
lemma

resMap_mk

L102 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing.NewLocalAux.resMap_mk
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing
attribute [-instance] 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] 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 CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
universe u
namespace NewLocalAux
section stage
variable {T : Type u} [CommRing T] {R : Type u} [CommRing R] [IsLocalRing R] [Algebra T R]
  (S : Subalgebra T R) [IsLocalRing ↥S] (hunit : ∀ x : ↥S, IsUnit x ↔ IsUnit (x : R))
Lean source · statement
lemma resMap_mk (a : ↥S) : resMap S hunit (Ideal.Quotient.mk _ a) =
    Ideal.Quotient.mk (IsLocalRing.maximalIdeal R) (a : R)
theorem

bijective_stage

L106 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing.NewLocalAux.bijective_stage
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing
attribute [-instance] 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] 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 CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
universe u
namespace NewLocalAux
section stage
variable {T : Type u} [CommRing T] {R : Type u} [CommRing R] [IsLocalRing R] [Algebra T R]
  (S : Subalgebra T R) [IsLocalRing ↥S] (hunit : ∀ x : ↥S, IsUnit x ↔ IsUnit (x : R))
include hunit in
Lean source · statement
theorem bijective_stage [IsNoetherianRing ↥S] {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of T))
    [IsProper f₀] [Flat f₀]
    (h : Function.Bijective (pullback.snd (pullback.snd f₀ (Spec.map (CommRingCat.ofHom (algebraMap
      T R))))
      (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (IsLocalRing.maximalIdeal R))))).appTop) :
    Function.Bijective (pullback.snd f₀ (Spec.map (CommRingCat.ofHom (algebraMap T ↥S)))).appTop
theorem

main

L204 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing.NewLocalAux.main
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing
attribute [-instance] 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] 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 CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
universe u
open NewLocalAux _root_.AlgebraicGeometry.SubalgebraStages in
Lean source · statement
theorem NewLocalAux.main {X : Scheme.{u}} {R : Type u} [CommRing R] [IsLocalRing R]
    (g : X ⟶ Spec (CommRingCat.of R)) [IsProper g] [Flat g] [LocallyOfFinitePresentation g]
    (h : Function.Bijective (pullback.snd g (Spec.map (CommRingCat.ofHom
      (Ideal.Quotient.mk (IsLocalRing.maximalIdeal R))))).appTop) :
    Function.Bijective g.appTop
theorem

bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing

L354 ↗
AlgebraicGeometry.bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicGeometry
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing in
Lean source · statement
theorem bijective_appTop_of_isProper_of_flat_of_locallyOfFinitePresentation_of_isLocalRing
    {X : Scheme.{u}} {A : CommRingCat.{u}} [IsLocalRing A]
    (p : X ⟶ Spec A) [IsProper p] [Flat p] [LocallyOfFinitePresentation p]
    (h : Function.Bijective (pullback.snd p (Spec.map (CommRingCat.ofHom
      (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))))).appTop) :
    Function.Bijective p.appTop

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