Module

isIso_of_isOpenImmersion_of_isClosedImmersion_of_section_of_isConnected_fibres.lean

Nyll.AlgebraicCurves.Geometry.Schemes.isIso_of_isOpenImmersion_of_isClosedImmersion_of_section_of_isConnected_fibres

2 declarations indexed from sourceView source ↗

Module documentation

is Iso of is Open Immersion of is Closed Immersion of section of is Connected fibres

Imports3

Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Morphisms.IsIso
Mathlib.Topology.Connected.Clopen

Imported by2

theorem

eq_univ_of_isClopen_of_section

L32 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isIso_of_isOpenImmersion_of_isClosedImmersion_of_section_of_isConnected_fibres.Ws23G2.eq_univ_of_isClopen_of_section

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isIso_of_isOpenImmersion_of_isClosedImmersion_of_section_of_isConnected_fibres
open CategoryTheory AlgebraicGeometry
namespace Ws23G2
universe u

Lean source · statement

theorem eq_univ_of_isClopen_of_section {X S : Scheme.{u}} (g : X ⟶ S) (Z : Set X) (hZ : IsClopen Z)
    (hconn : ∀ s : S, _root_.IsPreconnected (g.base ⁻¹' {s}))
    (σ : S ⟶ X) (hσ : σ ≫ g = 𝟙 S) (hσZ : ∀ s : S, σ.base s ∈ Z) : Z = Set.univ

theorem

isIso_of_isOpenImmersion_of_isClosedImmersion_of_section_of_isConnected_fibres

L55 ↗

AlgebraicGeometry.isIso_of_isOpenImmersion_of_isClosedImmersion_of_section_of_isConnected_fibres

Source context 5 commands