Module

RelEffCartierDiv_card_le_of_subset_support.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_card_le_of_subset_support

3 declarations indexed from sourceView source ↗

Module documentation

Rel Eff Cartier Div card le of subset support

Imports10

Mathlib.RingTheory.Artinian.Ring
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.LinearAlgebra.Dimension.Constructions
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.Flat
Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Mathlib.Tactic.Choose
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv

Imported by1

Nyll.AlgebraicCurves.RelativeDivisors.All

theorem

card_le_finrank_of_primes

L39 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_card_le_of_subset_support.FltWs21.B1.card_le_finrank_of_primes

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_card_le_of_subset_support
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace FltWs21
namespace B1

Lean source · statement

theorem card_le_finrank_of_primes {k A : Type u} [Field k] [CommRing A] [Algebra k A]
  [Module.Finite k A]
    (F : Finset (PrimeSpectrum A)) : F.card ≤ Module.finrank k A

theorem

card_le_finrank_of_isFinite

L74 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_card_le_of_subset_support.FltWs21.B1.card_le_finrank_of_isFinite

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_card_le_of_subset_support
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace FltWs21
namespace B1

Lean source · statement

theorem card_le_finrank_of_isFinite {k : Type u} [Field k] {Z : Scheme.{u}} (q : Z ⟶ Spec
  (CommRingCat.of k))
    [IsFinite q] [Flat q] (F : Finset Z) : F.card ≤ q.finrank (IsLocalRing.closedPoint k)

theorem

card_le_of_subset_support

L117 ↗

AlgebraicGeometry.RelEffCartierDiv.card_le_of_subset_support

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_card_le_of_subset_support
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open FltWs21.B1 in

Lean source · statement

theorem _root_.AlgebraicGeometry.RelEffCartierDiv.card_le_of_subset_support
    {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ} {k : Type u} [Field k] {x : Spec (CommRingCat.of k) ⟶ S}
    (D : RelEffCartierDiv f r x) (F : Finset ↥(pullback f x)) (hF : ∀ z ∈ F, z ∈ D.I.support) :
    F.card ≤ r

Module documentation

Rel Eff Cartier Div card le of subset support

Declarations

card_le_finrank_of_primes

card_le_finrank_of_isFinite

card_le_of_subset_support