Module

Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma

10 declarations indexed from sourceView source ↗

Module documentation

Scheme is Clopen preimage sigma Inj and exists Unique lift of hom sigma

Imports2

Mathlib.AlgebraicGeometry.Limits
Mathlib.Topology.Compactness.Compact

Imported by3

theorem

range_sigmaι_eq

L33 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma.CoprodPtsA.range_sigmaι_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
namespace CoprodPtsA
variable {σ : Type u} (H : σ → Scheme.{u}) {T : Scheme.{u}} (u : T ⟶ ∐ H)

Lean source · statement

theorem range_sigmaι_eq (i : σ) :
    Set.range (Sigma.ι H i).base = sigmaMk H '' Set.range (Sigma.mk i)

theorem

isClosed_opensRange

L42 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma.CoprodPtsA.isClosed_opensRange

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
namespace CoprodPtsA
variable {σ : Type u} (H : σ → Scheme.{u}) {T : Scheme.{u}} (u : T ⟶ ∐ H)

Lean source · statement

theorem isClosed_opensRange (i : σ) : IsClosed ((Sigma.ι H i).opensRange : Set ↥(∐ H))

theorem

iSup_opensRange

L46 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma.CoprodPtsA.iSup_opensRange

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
namespace CoprodPtsA
variable {σ : Type u} (H : σ → Scheme.{u}) {T : Scheme.{u}} (u : T ⟶ ∐ H)

Lean source · statement

theorem iSup_opensRange : (⨆ i, (Sigma.ι H i).opensRange) = ⊤

theorem

closed

L52 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma.CoprodPtsA.closed

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
namespace CoprodPtsA
variable {σ : Type u} (H : σ → Scheme.{u}) {T : Scheme.{u}} (u : T ⟶ ∐ H)

Lean source · statement

theorem closed (i : σ) : IsClosed ((u ⁻¹ᵁ (Sigma.ι H i).opensRange : T.Opens) : Set T)

theorem

disjoint

L55 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma.CoprodPtsA.disjoint

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
namespace CoprodPtsA
variable {σ : Type u} (H : σ → Scheme.{u}) {T : Scheme.{u}} (u : T ⟶ ∐ H)

Lean source · statement

theorem disjoint (i j : σ) (hij : i ≠ j) :
    Disjoint (u ⁻¹ᵁ (Sigma.ι H i).opensRange) (u ⁻¹ᵁ (Sigma.ι H j).opensRange)

theorem

cover

L60 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma.CoprodPtsA.cover

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
namespace CoprodPtsA
variable {σ : Type u} (H : σ → Scheme.{u}) {T : Scheme.{u}} (u : T ⟶ ∐ H)

Lean source · statement

theorem cover : (⨆ i, u ⁻¹ᵁ (Sigma.ι H i).opensRange) = ⊤

theorem

range_subset

L63 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma.CoprodPtsA.range_subset

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
namespace CoprodPtsA
variable {σ : Type u} (H : σ → Scheme.{u}) {T : Scheme.{u}} (u : T ⟶ ∐ H)

Lean source · statement

theorem range_subset (i : σ) :
    Set.range ((u ⁻¹ᵁ (Sigma.ι H i).opensRange).ι ≫ u).base ⊆ Set.range (Sigma.ι H i).base

theorem

lift

L72 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma.CoprodPtsA.lift

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
namespace CoprodPtsA
variable {σ : Type u} (H : σ → Scheme.{u}) {T : Scheme.{u}} (u : T ⟶ ∐ H)

Lean source · statement

theorem lift (i : σ) : ∃! v : ((u ⁻¹ᵁ (Sigma.ι H i).opensRange : T.Opens) : Scheme.{u}) ⟶ H i,
      v ≫ Sigma.ι H i = (u ⁻¹ᵁ (Sigma.ι H i).opensRange).ι ≫ u

theorem

finite

L81 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma.CoprodPtsA.finite

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
namespace CoprodPtsA
variable {σ : Type u} (H : σ → Scheme.{u}) {T : Scheme.{u}} (u : T ⟶ ∐ H)

Lean source · statement

theorem finite [CompactSpace T] :
    {i : σ | ((u ⁻¹ᵁ (Sigma.ι H i).opensRange : T.Opens) : Set T).Nonempty}.Finite

theorem

isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma

L100 ↗

AlgebraicGeometry.Scheme.isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma

Source context 5 commands

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

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

Lean source · statement

theorem
  _root_.AlgebraicGeometry.Scheme.isClopen_preimage_sigmaInj_and_existsUnique_lift_of_hom_sigma
    {σ : Type u} (H : σ → Scheme.{u}) {T : Scheme.{u}} (u : T ⟶ ∐ H) :
    (∀ i, IsClosed ((u ⁻¹ᵁ (Sigma.ι H i).opensRange : T.Opens) : Set T)) ∧
    (∀ i j, i ≠ j → Disjoint (u ⁻¹ᵁ (Sigma.ι H i).opensRange) (u ⁻¹ᵁ (Sigma.ι H j).opensRange)) ∧
    (⨆ i, u ⁻¹ᵁ (Sigma.ι H i).opensRange) = ⊤ ∧
    (∀ i, ∃! v : ((u ⁻¹ᵁ (Sigma.ι H i).opensRange : T.Opens) : Scheme.{u}) ⟶ H i,
      v ≫ Sigma.ι H i = (u ⁻¹ᵁ (Sigma.ι H i).opensRange).ι ≫ u) ∧
    (CompactSpace T → {i : σ | ((u ⁻¹ᵁ (Sigma.ι H i).opensRange : T.Opens) : Set
      T).Nonempty}.Finite)

Module documentation

Scheme is Clopen preimage sigma Inj and exists Unique lift of hom sigma

Declarations