Module

bijective_algebraMap_appTop_of_isProper_of_isIntegral.lean

Nyll.AlgebraicCurves.Geometry.Schemes.bijective_algebraMap_appTop_of_isProper_of_isIntegral

1 declaration indexed from sourceView source ↗

Module documentation

bijective algebra Map app Top of is Proper of is Integral

Imports11

Mathlib.Algebra.Polynomial.FieldDivision
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.AlgebraicGeometry.Properties
Mathlib.AlgebraicGeometry.Morphisms.Proper
Mathlib.AlgebraicGeometry.Morphisms.Integral
Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.RingTheory.Polynomial.Basic
Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.Tactic.Ext

Imported by2

theorem

bijective_algebraMap_appTop_of_isProper_of_isIntegral

L44 ↗

AlgebraicGeometry.bijective_algebraMap_appTop_of_isProper_of_isIntegral

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_algebraMap_appTop_of_isProper_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial

Lean source · statement

theorem _root_.AlgebraicGeometry.bijective_algebraMap_appTop_of_isProper_of_isIntegral
    (k : Type u) [Field k] [IsAlgClosed k] {X : Scheme.{u}}
    (fX : X ⟶ Spec (CommRingCat.of k)) [IsProper fX] [IsIntegral X] :
    Function.Bijective ((Scheme.ΓSpecIso (CommRingCat.of k)).inv ≫ fX.appTop).hom

Module documentation

bijective algebra Map app Top of is Proper of is Integral

Declarations

bijective_algebraMap_appTop_of_isProper_of_isIntegral