NYLL
Module

SmallExtension_IsFibreReading_eq_of_isFibreReading_of_flat.lean

Nyll.AlgebraicCurves.Geometry.Deformation.SmallExtension_IsFibreReading_eq_of_isFibreReading_of_flat
3 declarations indexed from sourceView source ↗

Module documentation

Small Extension Is Fibre Reading eq of is Fibre Reading of flat

Imports8
Imported by3

Declarations

theorem

app_res_top

L42 ↗
AlgebraicCurves.Geometry.Deformation.Proofs.FibreReadingUniqueness.T3P3a.app_res_top
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs.FibreReadingUniqueness
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open scoped TensorProduct
universe u
namespace T3P3a
Lean source · statement
theorem app_res_top {X Y : Scheme.{u}} (i : X ⟶ Y) (U : Y.Opens) (x : Γ(Y, ⊤)) :
    (i.app U).hom ((Y.presheaf.map (homOfLE (le_top : U ≤ ⊤)).op).hom x) =
      (X.presheaf.map (homOfLE (le_top : i ⁻¹ᵁ U ≤ ⊤)).op).hom ((i.appTop).hom x)
theorem

specMap_appTop_ΓSpecIso_inv

L51 ↗
AlgebraicCurves.Geometry.Deformation.Proofs.FibreReadingUniqueness.T3P3a.specMap_appTop_ΓSpecIso_inv
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs.FibreReadingUniqueness
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open scoped TensorProduct
universe u
namespace T3P3a
Lean source · statement
theorem specMap_appTop_ΓSpecIso_inv {B k : Type u} [CommRing B] [CommRing k] (r : B →+* k) (b : B) :
    (Spec.map (CommRingCat.ofHom r)).appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of B)).inv.hom b) =
      (Scheme.ΓSpecIso (CommRingCat.of k)).inv.hom (r b)
theorem

eq_of_isFibreReading_of_flat

L60 ↗
AlgebraicGeometry.SmallExtension.IsFibreReading.eq_of_isFibreReading_of_flat
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs.FibreReadingUniqueness
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open scoped TensorProduct
universe u
open T3P3a in
Lean source · statement
theorem _root_.AlgebraicGeometry.SmallExtension.IsFibreReading.eq_of_isFibreReading_of_flat
    {B₁ : Type u} [CommRing B₁] [IsLocalRing B₁]
    (V : Type u) [AddCommGroup V] [Module (ResidueField B₁) V] [Module B₁ V] [IsScalarTower B₁
      (ResidueField B₁) V]
    (ι : V →ₗ[B₁] B₁) (hι : Function.Injective ι)
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of B₁)) [Flat f]
    {Xk : Scheme.{u}} (fk : Xk ⟶ Spec (CommRingCat.of (ResidueField B₁))) (i : Xk ⟶ X)
    (hi : IsPullback i fk f (Spec.map (CommRingCat.ofHom (residue B₁))))
    (U : X.Opens) (hU : IsAffineOpen U) (W : Xk.Opens) (hW : W ≤ i ⁻¹ᵁ U) (δ : Γ(X, U))
    (w w' : Module.Dual (ResidueField B₁) V →ₗ[ResidueField B₁] (OModulePresheaf.unit fk).obj W)
    (hw : IsFibreReading V ι f fk i U W hW δ w) (hw' : IsFibreReading V ι f fk i U W hW δ w') :
    w = w'

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