Module

IdealSheafData_flat_subschemeInclusion_comp_of_forall_mul_mem_of_isDiscreteValuationRing.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.IdealSheafData_flat_subschemeInclusion_comp_of_forall_mul_mem_of_isDiscreteValuationRing

3 declarations indexed from sourceView source ↗

Module documentation

Ideal Sheaf Data flat subscheme Inclusion comp of forall mul mem of is Discrete Valuation

Ring

Imports6

Mathlib.AlgebraicGeometry.Morphisms.Flat
Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.RingTheory.Flat.TorsionFree
Mathlib.Tactic.Ring
Mathlib.Tactic.Set
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv

Imported by2

theorem

ringHom_flat_mk_comp

L35 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.IdealSheafData_flat_subschemeInclusion_comp_of_forall_mul_mem_of_isDiscreteValuationRing.SatFlat.ringHom_flat_mk_comp

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace IdealSheafData_flat_subschemeInclusion_comp_of_forall_mul_mem_of_isDiscreteValuationRing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace SatFlat

Lean source · statement

theorem ringHom_flat_mk_comp {O : Type u} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O] {A
  : Type u} [CommRing A]
    (θ : O →+* A) (J : Ideal A) (hsat : ∀ (ϖ : O), Irreducible ϖ → ∀ s : A, θ ϖ * s ∈ J → s ∈ J) :
    ((Ideal.Quotient.mk J).comp θ).Flat

instance

(anonymous instance)

L71 ↗

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace IdealSheafData_flat_subschemeInclusion_comp_of_forall_mul_mem_of_isDiscreteValuationRing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry

Lean source · statement

instance {X : Scheme.{u}} (J : X.IdealSheafData) :
    ∀ i : J.subschemeCover.openCover.I₀,
      IsAffine (J.subschemeCover.openCover.X i)

theorem

flat_subschemeInclusion_comp_of_forall_mul_mem_of_isDiscreteValuationRing

L87 ↗

AlgebraicGeometry.IdealSheafData.flat_subschemeInclusion_comp_of_forall_mul_mem_of_isDiscreteValuationRing

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicGeometry.IdealSheafData
universe u
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs in
open IdealSheafData_flat_subschemeInclusion_comp_of_forall_mul_mem_of_isDiscreteValuationRing in
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry in
open SatFlat in

Lean source · statement

theorem flat_subschemeInclusion_comp_of_forall_mul_mem_of_isDiscreteValuationRing
    {O : Type u} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {X : Scheme.{u}} (q : X ⟶ Spec (CommRingCat.of O)) (J : X.IdealSheafData)
    (hsat : ∀ (ϖ : O), Irreducible ϖ → ∀ (U : X.affineOpens) (s : Γ(X, U)),
        X.presheaf.map (homOfLE (le_top : (U : X.Opens) ≤ ⊤)).op
            (q.appTop ((Scheme.ΓSpecIso (CommRingCat.of O)).inv ϖ)) * s ∈ J.ideal U →
          s ∈ J.ideal U) :
    Flat (J.subschemeι ≫ q)

Module documentation

Ideal Sheaf Data flat subscheme Inclusion comp of forall mul mem of is Discrete Valuation

Declarations

ringHom_flat_mk_comp

(anonymous instance)

flat_subschemeInclusion_comp_of_forall_mul_mem_of_isDiscreteValuationRing