NYLL
Module

exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
17 declarations indexed from sourceView source ↗

Module documentation

exists fg subalgebra iso pullback of iso pullback of locally Of Finite Presentation

Imports3
Imported by2

Declarations

abbrev

XR

L56 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.IsoDesc.XR
Documentation

The base change of the scheme to the spectrum of a base algebra.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace IsoDesc
variable {A₀ : Type u} [CommRing A₀]
Lean source · statement
abbrev XR {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀)) (R : Type u) [CommRing
  R] [Algebra A₀ R] : Scheme.{u}
theorem

spec_comp

L67 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.IsoDesc.spec_comp
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace IsoDesc
variable {A₀ : Type u} [CommRing A₀]
section Stage
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))
  {R R' : Type u} [CommRing R] [Algebra A₀ R] [CommRing R'] [Algebra A₀ R']
  (φ : R →+* R') (hφ : φ.comp (algebraMap A₀ R) = algebraMap A₀ R')
include hφ in
Lean source · statement
theorem spec_comp : Spec.map (CommRingCat.ofHom φ) ≫ Spec.map (CommRingCat.ofHom (algebraMap A₀ R))
  =
    Spec.map (CommRingCat.ofHom (algebraMap A₀ R'))
def

stMap

L73 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.IsoDesc.stMap
Documentation

The base-change transition map induced by a compatible algebra morphism.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace IsoDesc
variable {A₀ : Type u} [CommRing A₀]
section Stage
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))
  {R R' : Type u} [CommRing R] [Algebra A₀ R] [CommRing R'] [Algebra A₀ R']
  (φ : R →+* R') (hφ : φ.comp (algebraMap A₀ R) = algebraMap A₀ R')
Lean source · statement
def stMap : XR f R' ⟶ XR f R
theorem

stMap_fst

L77 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.IsoDesc.stMap_fst
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace IsoDesc
variable {A₀ : Type u} [CommRing A₀]
section Stage
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))
  {R R' : Type u} [CommRing R] [Algebra A₀ R] [CommRing R'] [Algebra A₀ R']
  (φ : R →+* R') (hφ : φ.comp (algebraMap A₀ R) = algebraMap A₀ R')
Lean source · statement
theorem stMap_fst : stMap f φ hφ ≫ pullback.fst _ _ = pullback.fst _ _
theorem

stMap_snd

L79 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.IsoDesc.stMap_snd
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace IsoDesc
variable {A₀ : Type u} [CommRing A₀]
section Stage
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))
  {R R' : Type u} [CommRing R] [Algebra A₀ R] [CommRing R'] [Algebra A₀ R']
  (φ : R →+* R') (hφ : φ.comp (algebraMap A₀ R) = algebraMap A₀ R')
Lean source · statement
theorem stMap_snd : stMap f φ hφ ≫ pullback.snd _ _ = pullback.snd _ _ ≫
  Spec.map (CommRingCat.ofHom φ)
theorem

eq_stMap

L83 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.IsoDesc.eq_stMap
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace IsoDesc
variable {A₀ : Type u} [CommRing A₀]
section Stage
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))
  {R R' : Type u} [CommRing R] [Algebra A₀ R] [CommRing R'] [Algebra A₀ R']
  (φ : R →+* R') (hφ : φ.comp (algebraMap A₀ R) = algebraMap A₀ R')
Lean source · statement
theorem eq_stMap (q : XR f R' ⟶ XR f R) (h1 : q ≫ pullback.fst _ _ = pullback.fst _ _)
    (h2 : q ≫ pullback.snd _ _ = pullback.snd _ _ ≫ Spec.map (CommRingCat.ofHom φ)) : q = stMap f φ
      hφ
theorem

stMap_stMap

L102 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.IsoDesc.stMap_stMap
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace IsoDesc
variable {A₀ : Type u} [CommRing A₀]
section Comp
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))
  {R R' R'' : Type u} [CommRing R] [Algebra A₀ R] [CommRing R'] [Algebra A₀ R'] [CommRing R'']
    [Algebra A₀ R'']
  (φ : R →+* R') (hφ : φ.comp (algebraMap A₀ R) = algebraMap A₀ R')
  (ψ : R' →+* R'') (hψ : ψ.comp (algebraMap A₀ R') = algebraMap A₀ R'')
  (χ : R →+* R'') (hχ : χ.comp (algebraMap A₀ R) = algebraMap A₀ R'') (h : ψ.comp φ = χ)
include h in
Lean source · statement
theorem stMap_stMap : stMap f ψ hψ ≫ stMap f φ hφ = stMap f χ hχ
def

bc

L119 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.IsoDesc.bc
Documentation

The map on base changes induced by the given morphism over the intermediate base.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace IsoDesc
variable {A₀ : Type u} [CommRing A₀]
section BC
variable {X₁ X₂ : Scheme.{u}} (f₁ : X₁ ⟶ Spec (CommRingCat.of A₀)) (f₂ : X₂ ⟶ Spec (CommRingCat.of
  A₀))
  {R R' : Type u} [CommRing R] [Algebra A₀ R] [CommRing R'] [Algebra A₀ R']
  (φ : R →+* R') (hφ : φ.comp (algebraMap A₀ R) = algebraMap A₀ R')
  (g₀ : XR f₁ R ⟶ XR f₂ R) (hg₀ : g₀ ≫ pullback.snd _ _ = pullback.snd _ _)
Lean source · statement
def bc : XR f₁ R' ⟶ XR f₂ R'
theorem

bc_fst

L125 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.IsoDesc.bc_fst
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace IsoDesc
variable {A₀ : Type u} [CommRing A₀]
section BC
variable {X₁ X₂ : Scheme.{u}} (f₁ : X₁ ⟶ Spec (CommRingCat.of A₀)) (f₂ : X₂ ⟶ Spec (CommRingCat.of
  A₀))
  {R R' : Type u} [CommRing R] [Algebra A₀ R] [CommRing R'] [Algebra A₀ R']
  (φ : R →+* R') (hφ : φ.comp (algebraMap A₀ R) = algebraMap A₀ R')
  (g₀ : XR f₁ R ⟶ XR f₂ R) (hg₀ : g₀ ≫ pullback.snd _ _ = pullback.snd _ _)
Lean source · statement
theorem bc_fst : bc f₁ f₂ φ hφ g₀ hg₀ ≫ pullback.fst _ _ = stMap f₁ φ hφ ≫
  g₀ ≫ pullback.fst _ _
theorem

bc_snd

L128 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.IsoDesc.bc_snd
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace IsoDesc
variable {A₀ : Type u} [CommRing A₀]
section BC
variable {X₁ X₂ : Scheme.{u}} (f₁ : X₁ ⟶ Spec (CommRingCat.of A₀)) (f₂ : X₂ ⟶ Spec (CommRingCat.of
  A₀))
  {R R' : Type u} [CommRing R] [Algebra A₀ R] [CommRing R'] [Algebra A₀ R']
  (φ : R →+* R') (hφ : φ.comp (algebraMap A₀ R) = algebraMap A₀ R')
  (g₀ : XR f₁ R ⟶ XR f₂ R) (hg₀ : g₀ ≫ pullback.snd _ _ = pullback.snd _ _)
Lean source · statement
theorem bc_snd : bc f₁ f₂ φ hφ g₀ hg₀ ≫ pullback.snd _ _ = pullback.snd _ _
theorem

bc_stMap

L131 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.IsoDesc.bc_stMap
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace IsoDesc
variable {A₀ : Type u} [CommRing A₀]
section BC
variable {X₁ X₂ : Scheme.{u}} (f₁ : X₁ ⟶ Spec (CommRingCat.of A₀)) (f₂ : X₂ ⟶ Spec (CommRingCat.of
  A₀))
  {R R' : Type u} [CommRing R] [Algebra A₀ R] [CommRing R'] [Algebra A₀ R']
  (φ : R →+* R') (hφ : φ.comp (algebraMap A₀ R) = algebraMap A₀ R')
  (g₀ : XR f₁ R ⟶ XR f₂ R) (hg₀ : g₀ ≫ pullback.snd _ _ = pullback.snd _ _)
Lean source · statement
theorem bc_stMap : bc f₁ f₂ φ hφ g₀ hg₀ ≫ stMap f₂ φ hφ = stMap f₁ φ hφ ≫ g₀
theorem

bc_compat

L136 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.IsoDesc.bc_compat
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace IsoDesc
variable {A₀ : Type u} [CommRing A₀]
section BC
variable {X₁ X₂ : Scheme.{u}} (f₁ : X₁ ⟶ Spec (CommRingCat.of A₀)) (f₂ : X₂ ⟶ Spec (CommRingCat.of
  A₀))
  {R R' : Type u} [CommRing R] [Algebra A₀ R] [CommRing R'] [Algebra A₀ R']
  (φ : R →+* R') (hφ : φ.comp (algebraMap A₀ R) = algebraMap A₀ R')
  (g₀ : XR f₁ R ⟶ XR f₂ R) (hg₀ : g₀ ≫ pullback.snd _ _ = pullback.snd _ _)
Lean source · statement
theorem bc_compat {A : Type u} [CommRing A] [Algebra A₀ A]
    (ψ : R →+* A) (hψ : ψ.comp (algebraMap A₀ R) = algebraMap A₀ A)
    (ψ' : R' →+* A) (hψ' : ψ'.comp (algebraMap A₀ R') = algebraMap A₀ A) (hcomp : ψ'.comp φ = ψ)
    (e : XR f₁ A ⟶ XR f₂ A) (he : e ≫ pullback.snd _ _ = pullback.snd _ _)
    (h : stMap f₁ ψ hψ ≫ g₀ = e ≫ stMap f₂ ψ hψ) :
    stMap f₁ ψ' hψ' ≫ bc f₁ f₂ φ hφ g₀ hg₀ = e ≫ stMap f₂ ψ' hψ'
theorem

inclusion_comp_algebraMap

L164 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.IsoDesc.inclusion_comp_algebraMap
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
attribute [local simp] IsoDesc.stMap_fst
attribute [local simp] IsoDesc.stMap_snd
attribute [local simp] IsoDesc.bc_fst
attribute [local simp] IsoDesc.bc_snd
namespace IsoDesc
section Main
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
Lean source · statement
theorem inclusion_comp_algebraMap {T T' : Subalgebra A₀ A} (h : T ≤ T') :
    (Subalgebra.inclusion h).toRingHom.comp (algebraMap A₀ ↥T) = algebraMap A₀ ↥T'
theorem

val_comp_algebraMap

L168 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.IsoDesc.val_comp_algebraMap
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
attribute [local simp] IsoDesc.stMap_fst
attribute [local simp] IsoDesc.stMap_snd
attribute [local simp] IsoDesc.bc_fst
attribute [local simp] IsoDesc.bc_snd
namespace IsoDesc
section Main
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
Lean source · statement
theorem val_comp_algebraMap (T : Subalgebra A₀ A) : T.val.toRingHom.comp (algebraMap A₀ ↥T) =
  algebraMap A₀ A
theorem

val_comp_inclusion

L172 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.IsoDesc.val_comp_inclusion
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
attribute [local simp] IsoDesc.stMap_fst
attribute [local simp] IsoDesc.stMap_snd
attribute [local simp] IsoDesc.bc_fst
attribute [local simp] IsoDesc.bc_snd
namespace IsoDesc
section Main
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
Lean source · statement
theorem val_comp_inclusion {T T' : Subalgebra A₀ A} (h : T ≤ T') :
    T'.val.toRingHom.comp (Subalgebra.inclusion h).toRingHom = T.val.toRingHom
theorem

exists_fg_stMap_comp_eq

L176 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation.IsoDesc.exists_fg_stMap_comp_eq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
attribute [local simp] IsoDesc.stMap_fst
attribute [local simp] IsoDesc.stMap_snd
attribute [local simp] IsoDesc.bc_fst
attribute [local simp] IsoDesc.bc_snd
namespace IsoDesc
section Main
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
Lean source · statement
theorem exists_fg_stMap_comp_eq {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀)) [QuasiCompact
  f] [LocallyOfFinitePresentation f]
    (B : Subalgebra A₀ A) (a : XR f ↥B ⟶ XR f ↥B) (ha : a ≫ pullback.snd _ _ = pullback.snd _ _)
    (hlim : stMap f B.val.toRingHom (val_comp_algebraMap B) ≫ a = stMap f B.val.toRingHom
      (val_comp_algebraMap B)) :
    ∃ T' : Subalgebra ↥B A, T'.FG ∧
      pullback.fst (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥B))))
          (Spec.map (CommRingCat.ofHom (algebraMap ↥B ↥T'))) ≫ a =
        pullback.fst (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥B))))
          (Spec.map (CommRingCat.ofHom (algebraMap ↥B ↥T')))
theorem

exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation

L238 ↗
AlgebraicGeometry.exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits
open AlgebraicCurves.Geometry.Schemes.Proofs
  exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
universe u
open IsoDesc
Lean source · statement
theorem exists_fg_subalgebra_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation
    {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
    {X₁ X₂ : Scheme.{u}} (f₁ : X₁ ⟶ Spec (CommRingCat.of A₀)) (f₂ : X₂ ⟶ Spec (CommRingCat.of A₀))
    [QuasiCompact f₁] [QuasiSeparated f₁] [LocallyOfFinitePresentation f₁]
    [QuasiCompact f₂] [QuasiSeparated f₂] [LocallyOfFinitePresentation f₂]
    (e : pullback f₁ (Spec.map (CommRingCat.ofHom (algebraMap A₀ A))) ≅
      pullback f₂ (Spec.map (CommRingCat.ofHom (algebraMap A₀ A))))
    (he : e.hom ≫ pullback.snd f₂ _ = pullback.snd f₁ _) (s : Finset A) :
    ∃ (T : Subalgebra A₀ A), T.FG ∧ (↑s : Set A) ⊆ T ∧
      ∃ e₀ : pullback f₁ (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥T))) ≅
          pullback f₂ (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥T))),
        e₀.hom ≫ pullback.snd f₂ _ = pullback.snd f₁ _ ∧
        ∀ (q₁ : pullback f₁ (Spec.map (CommRingCat.ofHom (algebraMap A₀ A))) ⟶
              pullback f₁ (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥T))))
          (q₂ : pullback f₂ (Spec.map (CommRingCat.ofHom (algebraMap A₀ A))) ⟶
              pullback f₂ (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥T)))),
          q₁ ≫ pullback.fst f₁ _ = pullback.fst f₁ _ →
          q₁ ≫ pullback.snd f₁ _ = pullback.snd f₁ _ ≫ Spec.map (CommRingCat.ofHom T.val.toRingHom)
            →
          q₂ ≫ pullback.fst f₂ _ = pullback.fst f₂ _ →
          q₂ ≫ pullback.snd f₂ _ = pullback.snd f₂ _ ≫ Spec.map (CommRingCat.ofHom T.val.toRingHom)
            →
          q₁ ≫ e₀.hom = e.hom ≫ q₂

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.