AlgebraicGeometry.bijective_app_of_isProper_of_flat_of_geometricallyReduced_of_geometricallyConnected
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry
universe u
open _root_.AlgebraicCurves.Geometry.Curves.Proofs in
open bijective_app_of_isProper_of_flat_of_geometricallyReduced_of_geometricallyConnected in
open AlgebraicGeometry CategoryTheory inLean source · statement
theorem bijective_app_of_isProper_of_flat_of_geometricallyReduced_of_geometricallyConnected
{X B : Scheme.{u}} (p : X ⟶ B) [IsProper p] [Flat p] [LocallyOfFinitePresentation p]
[GeometricallyReduced p] [GeometricallyConnected p] (U : B.Opens) :
Function.Bijective (p.app U)