Module

isIso_of_isIso_pullback_closedFibre_of_isFinite_of_etale_of_isProper.lean

Nyll.SchemeTheory.FiniteEtale.isIso_of_isIso_pullback_closedFibre_of_isFinite_of_etale_of_isProper

4 declarations indexed from sourceView source ↗

Module documentation

is Iso of is Iso pullback closed Fibre of is Finite of etale of is Proper

Imports4

Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.Proper
Mathlib.AlgebraicGeometry.PullbackCarrier

Imported by3

theorem

exists_specializes_over_closedPoint

L33 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isIso_of_isIso_pullback_closedFibre_of_isFinite_of_etale_of_isProper.F1dE121.exists_specializes_over_closedPoint

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIso_of_isIso_pullback_closedFibre_of_isFinite_of_etale_of_isProper
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace F1dE121

Lean source · statement

theorem exists_specializes_over_closedPoint {R : Type u} [CommRing R] [IsLocalRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) [UniversallyClosed f] (x : X) :
    ∃ x' : X, x ⤳ x' ∧ f.base x' = IsLocalRing.closedPoint R

theorem

closedPoint_mem_range_residue

L43 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isIso_of_isIso_pullback_closedFibre_of_isFinite_of_etale_of_isProper.F1dE121.closedPoint_mem_range_residue

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIso_of_isIso_pullback_closedFibre_of_isFinite_of_etale_of_isProper
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace F1dE121

Lean source · statement

theorem closedPoint_mem_range_residue {R : Type u} [CommRing R] [IsLocalRing R] :
    IsLocalRing.closedPoint R ∈
      Set.range (Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))).base

theorem

apply_eq_of_specializes

L50 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isIso_of_isIso_pullback_closedFibre_of_isFinite_of_etale_of_isProper.F1dE121.apply_eq_of_specializes

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIso_of_isIso_pullback_closedFibre_of_isFinite_of_etale_of_isProper
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace F1dE121

Lean source · statement

theorem apply_eq_of_specializes {α β : Type*} [TopologicalSpace α] {g : α → β}
    (hg : IsLocallyConstant g) {x x' : α} (h : x ⤳ x') : g x' = g x

theorem

isIso_of_isIso_pullback_closedFibre_of_isFinite_of_etale_of_isProper

L58 ↗

AlgebraicGeometry.isIso_of_isIso_pullback_closedFibre_of_isFinite_of_etale_of_isProper

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIso_of_isIso_pullback_closedFibre_of_isFinite_of_etale_of_isProper
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open F1dE121 in

Lean source · statement

theorem
  _root_.AlgebraicGeometry.isIso_of_isIso_pullback_closedFibre_of_isFinite_of_etale_of_isProper
    {R : Type u} [CommRing R] [IsLocalRing R]
    {X U : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f]
    (π : U ⟶ X) [IsFinite π] [AlgebraicGeometry.Etale π]
    (hk : IsIso (pullback.snd π (pullback.fst f (Spec.map (CommRingCat.ofHom (IsLocalRing.residue
      R)))))) :
    IsIso π

Module documentation

is Iso of is Iso pullback closed Fibre of is Finite of etale of is Proper

Declarations

exists_specializes_over_closedPoint

closedPoint_mem_range_residue

apply_eq_of_specializes

isIso_of_isIso_pullback_closedFibre_of_isFinite_of_etale_of_isProper