NYLL
Module

bijective_app_of_bijective_appTop_morphismRestrict.lean

Nyll.AlgebraicCurves.Geometry.Schemes.bijective_app_of_bijective_appTop_morphismRestrict
2 declarations indexed from sourceView source ↗

Module documentation

bijective app of bijective app Top morphism Restrict

Imports4
  • Mathlib.AlgebraicGeometry.Restrict
  • Mathlib.CategoryTheory.ConcreteCategory.EpiMono
  • Mathlib.CategoryTheory.EqToHom
  • Mathlib.CategoryTheory.Opposites
Imported by2

Declarations

theorem

bijective_app_congr

L35 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_app_of_bijective_appTop_morphismRestrict.P4Aux.bijective_app_congr
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.bijective_app_of_bijective_appTop_morphismRestrict
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
open TopologicalSpace Opposite
namespace P4Aux
Lean source · statement
theorem bijective_app_congr {X B : Scheme.{u}} (p : X ⟶ B) {V W : B.Opens} (e : V = W)
    (h : Function.Bijective (p.app V)) : Function.Bijective (p.app W)
theorem

bijective_app_of_bijective_appTop_morphismRestrict

L44 ↗
AlgebraicGeometry.bijective_app_of_bijective_appTop_morphismRestrict
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.bijective_app_of_bijective_appTop_morphismRestrict
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
open TopologicalSpace Opposite
open P4Aux
Lean source · statement
theorem _root_.AlgebraicGeometry.bijective_app_of_bijective_appTop_morphismRestrict {X B :
  Scheme.{u}} (p : X ⟶ B) (U : B.Opens)
    (h : Function.Bijective (p ∣_ U).appTop) : 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.