Module

Scheme_TwoAffineOpenCover_flat_sections_of_flat.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_flat_sections_of_flat

1 declaration indexed from sourceView source ↗

Module documentation

Flat sections on affine opens

For a flat scheme over an affine base, the sections on an affine open are flat over the base ring with the algebra structure induced by the scheme morphism.

Imports2

Mathlib.AlgebraicGeometry.Morphisms.Flat
Nyll.SchemeTheory.Cohomology.Cech.TwoAffineOpenCover

Imported by13

theorem

flat_sections_of_flat

L32 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.flat_sections_of_flat

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_flat_sections_of_flat
universe u
open CategoryTheory AlgebraicGeometry

Lean source · full declaration

theorem _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.flat_sections_of_flat
    {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (CommRingCat.of R)) [Flat c]
    (U : X.Opens) (hU : IsAffineOpen U) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
    Module.Flat R Γ(X, U) := by
  let := Scheme.TwoAffineOpenCover.algebraOfHom c U
  have h1 : (c.appLE ⊤ U le_top).hom.Flat :=
    HasRingHomProperty.appLE @Flat c inferInstance ⟨⊤, isAffineOpen_top _⟩ ⟨U, hU⟩ le_top
  have hb : ((Scheme.ΓSpecIso (CommRingCat.of R)).inv.hom).Flat :=
    RingHom.Flat.of_bijective (Scheme.ΓSpecIso (CommRingCat.of
        R)).symm.commRingCatIsoToRingEquiv.bijective
  have h2 : ((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ c.appLE ⊤ U le_top).hom.Flat := by
    rw [CommRingCat.hom_comp]
    exact RingHom.Flat.comp hb h1
  exact RingHom.flat_algebraMap_iff.mp h2

Module documentation

Flat sections on affine opens

Declarations

flat_sections_of_flat