NYLL
Module

Scheme_Hom_finrank_comp_of_finrank_eq_const.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_finrank_comp_of_finrank_eq_const
5 declarations indexed from sourceView source ↗

Module documentation

Ranks of composites of finite flat morphisms

When the first finite flat morphism has constant rank, the rank of its composite with a second finite flat morphism is the product of that constant and the second rank.

Imports3
  • Mathlib.AlgebraicGeometry.Morphisms.FlatRank
  • Mathlib.AlgebraicGeometry.ResidueField
  • Mathlib.RingTheory.Artinian.Module
Imported by3

Declarations

theorem

finrank_eq_mul_of_rankAtStalk_eq

L40 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_finrank_comp_of_finrank_eq_const.AlgebraicGeometry.FinrankComp.finrank_eq_mul_of_rankAtStalk_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_finrank_comp_of_finrank_eq_const
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace FinrankComp
open _root_.AlgebraicGeometry
Lean source · statement
theorem finrank_eq_mul_of_rankAtStalk_eq (K B C : Type u) [Field K] [CommRing B] [Algebra K B]
    [CommRing C] [Algebra B C] [Algebra K C] [IsScalarTower K B C]
    [Module.Finite K B] [Module.Finite B C] [Module.Flat B C]
    (m : ℕ) (h : ∀ p : PrimeSpectrum B, Module.rankAtStalk (R := B) C p = m) :
    Module.finrank K C = m * Module.finrank K B
theorem

finrank_comp_SpecMap

L67 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_finrank_comp_of_finrank_eq_const.AlgebraicGeometry.FinrankComp.finrank_comp_SpecMap
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_finrank_comp_of_finrank_eq_const
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace FinrankComp
open _root_.AlgebraicGeometry
Lean source · statement
theorem finrank_comp_SpecMap {K : Type u} [Field K] {B C : CommRingCat.{u}} (ψ : CommRingCat.of
    K ⟶ B)
    (φ : B ⟶ C)
    [IsFinite (Spec.map ψ)] [Flat (Spec.map ψ)] [IsFinite (Spec.map φ)] [Flat (Spec.map φ)]
    (m : ℕ) (hf : ∀ y, (Spec.map φ).finrank y = m) (z : Spec (CommRingCat.of K)) :
    (Spec.map φ ≫ Spec.map ψ).finrank z = m * (Spec.map ψ).finrank z
theorem

finrank_comp_right_of_isIso

L94 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_finrank_comp_of_finrank_eq_const.AlgebraicGeometry.FinrankComp.finrank_comp_right_of_isIso
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_finrank_comp_of_finrank_eq_const
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace FinrankComp
open _root_.AlgebraicGeometry
Lean source · statement
theorem finrank_comp_right_of_isIso {X Y Y' : Scheme.{u}} (f : X ⟶ Y) (e : Y ⟶ Y') [IsIso e]
    [IsFinite f] [Flat f] (y : Y) : (f ≫ e).finrank (e y) = f.finrank y
theorem

finrank_comp_of_field

L102 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_finrank_comp_of_finrank_eq_const.AlgebraicGeometry.FinrankComp.finrank_comp_of_field
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_finrank_comp_of_finrank_eq_const
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace FinrankComp
open _root_.AlgebraicGeometry
Lean source · statement
theorem finrank_comp_of_field {X Y : Scheme.{u}} (K : Type u) [Field K] (f : X ⟶ Y)
    (g : Y ⟶ Spec (CommRingCat.of K)) [IsFinite f] [Flat f] [IsFinite g] [Flat g]
    (m : ℕ) (hf : ∀ y, f.finrank y = m) (z : Spec (CommRingCat.of K)) :
    (f ≫ g).finrank z = m * g.finrank z
theorem

finrank_comp_of_finrank_eq_const

L136 ↗
AlgebraicGeometry.Scheme.Hom.finrank_comp_of_finrank_eq_const
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_finrank_comp_of_finrank_eq_const
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open AlgebraicGeometry.FinrankComp in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Hom.finrank_comp_of_finrank_eq_const
    {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsFinite f] [Flat f] [IsFinite g] [Flat g]
    (m : ℕ) (hf : ∀ y : Y, f.finrank y = m) (z : Z) :
    (f ≫ g).finrank z = m * g.finrank z

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