NYLL
Module

flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo.lean

Nyll.AlgebraicCurves.Geometry.Schemes.flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
14 declarations indexed from sourceView source ↗

Module documentation

flat of locally Of Finite Presentation of forall flat scheme Fibre Endo

Imports23
  • Mathlib.AlgebraicGeometry.Cover.MorphismProperty
  • Mathlib.AlgebraicGeometry.Cover.Open
  • Mathlib.AlgebraicGeometry.GammaSpecAdjunction
  • Mathlib.AlgebraicGeometry.Morphisms.Basic
  • Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
  • Mathlib.AlgebraicGeometry.Morphisms.Flat
  • Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
  • Mathlib.AlgebraicGeometry.Pullbacks
  • Mathlib.AlgebraicGeometry.ResidueField
  • Mathlib.AlgebraicGeometry.Scheme
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
  • Mathlib.CategoryTheory.MorphismProperty.Basic
  • Mathlib.CategoryTheory.MorphismProperty.Limits
  • Mathlib.RingTheory.FinitePresentation
  • Mathlib.RingTheory.RingHom.Flat
  • Mathlib.RingTheory.TensorProduct.Basic
  • Mathlib.RingTheory.TensorProduct.Maps
  • Mathlib.Tactic.Algebraize
  • Mathlib.Tactic.WLOG
  • Nyll.AlgebraicCurves.Geometry.Schemes.SchemeFibreEndo
  • Nyll.AlgebraicCurves.Foundations.Algebra.Module_Flat_of_finitePresentation_of_forall_flat_residueField_tensorProduct
Imported by2

Declarations

instance

(anonymous instance)

L55 ↗
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
universe u
Lean source · statement
instance : IsZariskiLocalAtTarget (@Flat.{u})
instance

(anonymous instance)

L58 ↗
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
universe u
local instance : IsZariskiLocalAtTarget (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtTarget (P := @Flat.{u}) (Q := RingHom.Flat)
Lean source · statement
instance : IsZariskiLocalAtSource (@Flat.{u})
instance

(anonymous instance)

L61 ↗
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
universe u
local instance : IsZariskiLocalAtTarget (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtTarget (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : IsZariskiLocalAtSource (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtSource (P := @Flat.{u}) (Q := RingHom.Flat)
Lean source · statement
instance : MorphismProperty.RespectsIso (@Flat.{u})
lemma

flat_snd_comp

L80 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo.AlgebraicGeometry.FlatFibreCriterionSol.flat_snd_comp
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
universe u
local instance : IsZariskiLocalAtTarget (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtTarget (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : IsZariskiLocalAtSource (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtSource (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : MorphismProperty.RespectsIso (@Flat.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.respectsIso
namespace AlgebraicGeometry
namespace FlatFibreCriterionSol
open _root_.AlgebraicGeometry
Lean source · statement
lemma flat_snd_comp {X Y Z Z' : Scheme.{u}} (g : X ⟶ Y) (a : Z ⟶ Y) (ψ : Z' ⟶ Z)
    [Flat (pullback.snd g a)] : Flat (pullback.snd g (ψ ≫ a))
lemma

flat_snd_snd

L85 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo.AlgebraicGeometry.FlatFibreCriterionSol.flat_snd_snd
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
universe u
local instance : IsZariskiLocalAtTarget (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtTarget (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : IsZariskiLocalAtSource (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtSource (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : MorphismProperty.RespectsIso (@Flat.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.respectsIso
namespace AlgebraicGeometry
namespace FlatFibreCriterionSol
open _root_.AlgebraicGeometry
Lean source · statement
lemma flat_snd_snd {X Y Y' Z : Scheme.{u}} (g : X ⟶ Y) (c : Y' ⟶ Y) (b : Z ⟶ Y')
    [Flat (pullback.snd g (b ≫ c))] : Flat (pullback.snd (pullback.snd g c) b)
lemma

flat_snd_comp_left

L90 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo.AlgebraicGeometry.FlatFibreCriterionSol.flat_snd_comp_left
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
universe u
local instance : IsZariskiLocalAtTarget (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtTarget (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : IsZariskiLocalAtSource (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtSource (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : MorphismProperty.RespectsIso (@Flat.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.respectsIso
namespace AlgebraicGeometry
namespace FlatFibreCriterionSol
open _root_.AlgebraicGeometry
Lean source · statement
lemma flat_snd_comp_left {X X' Y Z : Scheme.{u}} (g : X ⟶ Y) (i : X' ⟶ X) [Flat i]
    (a : Z ⟶ Y) [Flat (pullback.snd g a)] : Flat (pullback.snd (i ≫ g) a)
lemma

flat_of_isOpenImmersion

L95 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo.AlgebraicGeometry.FlatFibreCriterionSol.flat_of_isOpenImmersion
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
universe u
local instance : IsZariskiLocalAtTarget (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtTarget (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : IsZariskiLocalAtSource (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtSource (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : MorphismProperty.RespectsIso (@Flat.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.respectsIso
namespace AlgebraicGeometry
namespace FlatFibreCriterionSol
open _root_.AlgebraicGeometry
Lean source · statement
lemma flat_of_isOpenImmersion {X Y : Scheme.{u}} (i : X ⟶ Y) [IsOpenImmersion i] : Flat i
def

FibrewiseFlat

L99 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo.AlgebraicGeometry.FlatFibreCriterionSol.FibrewiseFlat
Documentation

The morphism is flat after base change to every fibre of the target over the base.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
universe u
local instance : IsZariskiLocalAtTarget (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtTarget (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : IsZariskiLocalAtSource (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtSource (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : MorphismProperty.RespectsIso (@Flat.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.respectsIso
namespace AlgebraicGeometry
namespace FlatFibreCriterionSol
open _root_.AlgebraicGeometry
Lean source · statement
def FibrewiseFlat {S X Y : Scheme.{u}} (g : X ⟶ Y) (pY : Y ⟶ S) : Prop
lemma

map_id_toAlgHom_toRingHom_eq

L102 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo.AlgebraicGeometry.FlatFibreCriterionSol.map_id_toAlgHom_toRingHom_eq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
universe u
local instance : IsZariskiLocalAtTarget (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtTarget (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : IsZariskiLocalAtSource (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtSource (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : MorphismProperty.RespectsIso (@Flat.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.respectsIso
namespace AlgebraicGeometry
namespace FlatFibreCriterionSol
open _root_.AlgebraicGeometry
Lean source · statement
lemma map_id_toAlgHom_toRingHom_eq {R A B K : Type u} [CommRing R] [CommRing A] [CommRing B]
    [CommRing K] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] [Algebra R K] :
    (Algebra.TensorProduct.map (AlgHom.id K K) (IsScalarTower.toAlgHom R A B)).toRingHom =
      ((Algebra.TensorProduct.comm R B K).toRingHom.comp
        (Algebra.TensorProduct.cancelBaseChange R A A B K).toRingHom).comp
      ((Algebra.TensorProduct.includeRight :
          A ⊗[R] K →ₐ[A] B ⊗[A] (A ⊗[R] K)).toRingHom.comp
        (Algebra.TensorProduct.comm R K A).toRingHom)
lemma

flat_map_of_flat_pullback_snd

L116 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo.AlgebraicGeometry.FlatFibreCriterionSol.flat_map_of_flat_pullback_snd
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
universe u
local instance : IsZariskiLocalAtTarget (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtTarget (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : IsZariskiLocalAtSource (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtSource (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : MorphismProperty.RespectsIso (@Flat.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.respectsIso
namespace AlgebraicGeometry
namespace FlatFibreCriterionSol
open _root_.AlgebraicGeometry
Lean source · statement
lemma flat_map_of_flat_pullback_snd {R A B K : Type u} [CommRing R] [CommRing A] [CommRing B]
    [CommRing K] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] [Algebra R K]
    [Flat (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap A B)))
      (Spec.map (CommRingCat.ofHom (algebraMap A (A ⊗[R] K)))))] :
    (Algebra.TensorProduct.map (AlgHom.id K K) (IsScalarTower.toAlgHom R A B)).toRingHom.Flat
theorem

flat_SpecMap_of_forall_flat_pullback_snd_fibre

L135 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo.AlgebraicGeometry.FlatFibreCriterionSol.flat_SpecMap_of_forall_flat_pullback_snd_fibre
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
universe u
local instance : IsZariskiLocalAtTarget (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtTarget (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : IsZariskiLocalAtSource (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtSource (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : MorphismProperty.RespectsIso (@Flat.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.respectsIso
namespace AlgebraicGeometry
namespace FlatFibreCriterionSol
open _root_.AlgebraicGeometry
Lean source · statement
theorem flat_SpecMap_of_forall_flat_pullback_snd_fibre
    {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B]
    (hflat : Flat (Spec.map (CommRingCat.ofHom (algebraMap R B))))
    (hfpB : LocallyOfFinitePresentation (Spec.map (CommRingCat.ofHom (algebraMap R B))))
    (hfpA : LocallyOfFinitePresentation (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    (hfib : ∀ s : Spec (.of R), Flat (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap A B)))
      (pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap R A)))
        ((Spec (.of R)).fromSpecResidueField s)))) :
    Flat (Spec.map (CommRingCat.ofHom (algebraMap A B)))
theorem

flat_of_forall_flat_pullback_snd_fibre

L175 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo.AlgebraicGeometry.FlatFibreCriterionSol.flat_of_forall_flat_pullback_snd_fibre
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
universe u
local instance : IsZariskiLocalAtTarget (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtTarget (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : IsZariskiLocalAtSource (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtSource (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : MorphismProperty.RespectsIso (@Flat.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.respectsIso
namespace AlgebraicGeometry
namespace FlatFibreCriterionSol
open _root_.AlgebraicGeometry
Lean source · statement
theorem flat_of_forall_flat_pullback_snd_fibre
    {S X Y : Scheme.{u}} (g : X ⟶ Y) (pY : Y ⟶ S)
    [Flat (g ≫ pY)] [LocallyOfFinitePresentation (g ≫ pY)] [LocallyOfFinitePresentation pY]
    (hfib : FibrewiseFlat g pY) :
    Flat g
lemma

isPullback_schemeFibreEndo

L277 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo.AlgebraicGeometry.FlatFibreCriterionSol.isPullback_schemeFibreEndo
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
universe u
local instance : IsZariskiLocalAtTarget (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtTarget (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : IsZariskiLocalAtSource (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtSource (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : MorphismProperty.RespectsIso (@Flat.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.respectsIso
namespace AlgebraicGeometry
namespace FlatFibreCriterionSol
open _root_.AlgebraicGeometry
Lean source · statement
lemma isPullback_schemeFibreEndo {S X : Scheme.{u}} (f : X ⟶ S) (h : X ⟶ X) (hh : h ≫ f = f)
    (s : S) :
    IsPullback (schemeFibreEndo f h hh s) (pullback.fst f (S.fromSpecResidueField s))
      (pullback.fst f (S.fromSpecResidueField s)) h
theorem

flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo

L290 ↗
AlgebraicGeometry.flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
universe u
local instance : IsZariskiLocalAtTarget (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtTarget (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : IsZariskiLocalAtSource (@Flat.{u}) :=
  HasRingHomProperty.instIsZariskiLocalAtSource (P := @Flat.{u}) (Q := RingHom.Flat)
local instance : MorphismProperty.RespectsIso (@Flat.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.respectsIso
open AlgebraicGeometry.FlatFibreCriterionSol in
Lean source · statement
theorem _root_.AlgebraicGeometry.flat_of_locallyOfFinitePresentation_of_forall_flat_schemeFibreEndo
    {S X : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f]
    (h : X ⟶ X) (hh : h ≫ f = f)
    (hfib : ∀ s : S, Flat (schemeFibreEndo f h hh s)) :
    Flat h

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