Module

comp_section_comp_eq_of_isClosedMap_of_surjective_app.lean

Nyll.AlgebraicCurves.Geometry.Schemes.comp_section_comp_eq_of_isClosedMap_of_surjective_app

3 declarations indexed from sourceView source ↗

Module documentation

comp section comp eq of is Closed Map of surjective app

Imports3

Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Gluing
Mathlib.Tactic.CategoryTheory.Reassoc

Imported by2

theorem

appLE_self_eq_id_of_eq_id

L32 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.comp_section_comp_eq_of_isClosedMap_of_surjective_app.SolRigidityBase.appLE_self_eq_id_of_eq_id

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace comp_section_comp_eq_of_isClosedMap_of_surjective_app
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u
namespace SolRigidityBase

Lean source · statement

theorem appLE_self_eq_id_of_eq_id {B : Scheme.{u}} (q : B ⟶ B) (hq : q = 𝟙 B) (U : B.Opens)
    (e : U ≤ q ⁻¹ᵁ U) : q.appLE U U e = 𝟙 _

theorem

main

L39 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.comp_section_comp_eq_of_isClosedMap_of_surjective_app.SolRigidityBase.main

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace comp_section_comp_eq_of_isClosedMap_of_surjective_app
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u
namespace SolRigidityBase

Lean source · statement

theorem main
    {X B Y : Scheme.{u}} (p : X ⟶ B) (ε : B ⟶ X) (hε : ε ≫ p = 𝟙 B)
    (hp : IsClosedMap p)
    (hH0 : ∀ U : B.Opens, IsAffineOpen U → Function.Surjective (p.app U))
    (f : X ⟶ Y) (hf : ∀ x : X, f (ε (p x)) = f x) :
    p ≫ ε ≫ f = f

theorem

comp_section_comp_eq_of_isClosedMap_of_surjective_app

L95 ↗

AlgebraicGeometry.comp_section_comp_eq_of_isClosedMap_of_surjective_app

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace comp_section_comp_eq_of_isClosedMap_of_surjective_app
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u

Lean source · statement

theorem _root_.AlgebraicGeometry.comp_section_comp_eq_of_isClosedMap_of_surjective_app
    {X B Y : Scheme.{u}} (p : X ⟶ B) (ε : B ⟶ X) (hε : ε ≫ p = 𝟙 B)
    (hp : IsClosedMap p)
    (hH0 : ∀ U : B.Opens, IsAffineOpen U → Function.Surjective (p.app U))
    (f : X ⟶ Y) (hf : ∀ x : X, f (ε (p x)) = f x) :
    p ≫ ε ≫ f = f

Module documentation

comp section comp eq of is Closed Map of surjective app

Declarations

appLE_self_eq_id_of_eq_id

main

comp_section_comp_eq_of_isClosedMap_of_surjective_app