Module

IsZariskiLocalAtTarget_sigmaMap.lean

Nyll.AlgebraicCurves.Geometry.Schemes.IsZariskiLocalAtTarget_sigmaMap

3 declarations indexed from sourceView source ↗

Module documentation

Is Zariski Local At Target sigma Map

Imports3

Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.Morphisms.Basic
Mathlib.AlgebraicGeometry.OpenImmersion

Imported by2

theorem

sigmaMap_sigmaι_apply

L45 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.IsZariskiLocalAtTarget_sigmaMap.AlgebraicGeometry.SigmaMapU4.sigmaMap_sigmaι_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.IsZariskiLocalAtTarget_sigmaMap
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace SigmaMapU4
open _root_.AlgebraicGeometry
variable {σ : Type u} {X Y : σ → Scheme.{u}} (f : ∀ i, X i ⟶ Y i)

Lean source · statement

theorem sigmaMap_sigmaι_apply (i : σ) (x : X i) :
    (Limits.Sigma.map f) ((Limits.Sigma.ι X i) x) = (Limits.Sigma.ι Y i) (f i x)

theorem

isPullback_sigmaι_sigmaMap

L50 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.IsZariskiLocalAtTarget_sigmaMap.AlgebraicGeometry.SigmaMapU4.isPullback_sigmaι_sigmaMap

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.IsZariskiLocalAtTarget_sigmaMap
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace SigmaMapU4
open _root_.AlgebraicGeometry
variable {σ : Type u} {X Y : σ → Scheme.{u}} (f : ∀ i, X i ⟶ Y i)

Lean source · statement

theorem isPullback_sigmaι_sigmaMap (j : σ) :
    IsPullback (f j) (Limits.Sigma.ι X j) (Limits.Sigma.ι Y j) (Limits.Sigma.map f)

theorem

sigmaMap

L67 ↗

AlgebraicGeometry.IsZariskiLocalAtTarget.sigmaMap

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.IsZariskiLocalAtTarget_sigmaMap
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open AlgebraicGeometry.SigmaMapU4 in

Lean source · statement

theorem _root_.AlgebraicGeometry.IsZariskiLocalAtTarget.sigmaMap
    (P : MorphismProperty Scheme.{u}) [IsZariskiLocalAtTarget P]
    {σ : Type u} {X Y : σ → Scheme.{u}} (f : ∀ i, X i ⟶ Y i) (hf : ∀ i, P (f i)) :
    P (Limits.Sigma.map f)

Module documentation

Is Zariski Local At Target sigma Map

Declarations

sigmaMap_sigmaι_apply

isPullback_sigmaι_sigmaMap

sigmaMap