Module

RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle

41 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law flat scheme Nsmul of is Finite of abelian Scheme Property Bundle

Imports9

Imported by2

abbrev

KwFF14FiberιStalkMapKer

L44 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.KwFF14FiberιStalkMapKer

Documentation

The affine-base fiber-stalk kernel assertion: the fiber inclusion kills exactly the mapped maximal ideal of the base stalk.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

abbrev KwFF14FiberιStalkMapKer : Prop

theorem

kwFF14_map_stalkMap_congr_point

L52 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.kwFF14_map_stalkMap_congr_point

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

theorem kwFF14_map_stalkMap_congr_point {S X : Scheme.{u}} (f : X ⟶ S) (y y' : X)
    (hyy' : y = y') :
    ((IsLocalRing.maximalIdeal (S.presheaf.stalk (f.base y))).map (f.stalkMap y).hom).map
        (X.presheaf.stalkCongr (.of_eq hyy')).hom.hom =
      (IsLocalRing.maximalIdeal (S.presheaf.stalk (f.base y'))).map (f.stalkMap y').hom

abbrev

KwFF15FiberιStalkMapKerAffine

L62 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.KwFF15FiberιStalkMapKerAffine

Documentation

The fiber-stalk kernel assertion specialized to maps between affine schemes induced by an algebra map.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

abbrev KwFF15FiberιStalkMapKerAffine : Prop

theorem

kwFF15_kerEq_of_congr_hom

L74 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.kwFF15_kerEq_of_congr_hom

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

theorem kwFF15_kerEq_of_congr_hom {S X : Scheme.{u}} (f f' : X ⟶ S) (hff' : f = f')
    (s : S) (q : f.fiber s)
    (hall : ∀ q' : f'.fiber s, RingHom.ker ((f'.fiberι s).stalkMap q').hom =
      (IsLocalRing.maximalIdeal (S.presheaf.stalk (f'.base ((f'.fiberι s).base q')))).map
        (f'.stalkMap ((f'.fiberι s).base q')).hom) :
    RingHom.ker ((f.fiberι s).stalkMap q).hom =
      (IsLocalRing.maximalIdeal (S.presheaf.stalk (f.base ((f.fiberι s).base q)))).map
        (f.stalkMap ((f.fiberι s).base q)).hom

theorem

kwFF15_kerEq_congr_point

L84 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.kwFF15_kerEq_congr_point

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

theorem kwFF15_kerEq_congr_point {S X : Scheme.{u}} (f : X ⟶ S) (s : S)
    (q q' : f.fiber s) (hqq' : q = q')
    (h : RingHom.ker ((f.fiberι s).stalkMap q).hom =
      (IsLocalRing.maximalIdeal (S.presheaf.stalk (f.base ((f.fiberι s).base q)))).map
        (f.stalkMap ((f.fiberι s).base q)).hom) :
    RingHom.ker ((f.fiberι s).stalkMap q').hom =
      (IsLocalRing.maximalIdeal (S.presheaf.stalk (f.base ((f.fiberι s).base q')))).map
        (f.stalkMap ((f.fiberι s).base q')).hom

theorem

kwFF15_ker_hom_comp_of_isIso

L94 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.kwFF15_ker_hom_comp_of_isIso

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

theorem kwFF15_ker_hom_comp_of_isIso {A B C : CommRingCat.{u}} (f : A ⟶ B) (g : B ⟶ C)
    [IsIso g] : RingHom.ker (f ≫ g).hom = RingHom.ker f.hom

theorem

kwFF15_ker_hom_comp_comap

L99 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.kwFF15_ker_hom_comp_comap

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

theorem kwFF15_ker_hom_comp_comap {A B C : CommRingCat.{u}} (f : A ⟶ B) (g : B ⟶ C) :
    RingHom.ker (f ≫ g).hom = (RingHom.ker g.hom).comap f.hom

theorem

kwFF15_comap_map_of_isIso

L103 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.kwFF15_comap_map_of_isIso

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

theorem kwFF15_comap_map_of_isIso {A B : CommRingCat.{u}} (f : A ⟶ B) [IsIso f]
    (I : Ideal A) : (I.map f.hom).comap f.hom = I

theorem

kwFF15_ker_stalkMap_comp_strip

L107 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.kwFF15_ker_stalkMap_comp_strip

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

theorem kwFF15_ker_stalkMap_comp_strip {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    (x : X) [IsIso (f.stalkMap x)] :
    RingHom.ker ((f ≫ g).stalkMap x).hom = RingHom.ker (g.stalkMap (f x)).hom

theorem

kwFF15_ker_stalkMap_comp_peel

L113 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.kwFF15_ker_stalkMap_comp_peel

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

theorem kwFF15_ker_stalkMap_comp_peel {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    (x : X) :
    RingHom.ker ((f ≫ g).stalkMap x).hom =
      (RingHom.ker (f.stalkMap x).hom).comap (g.stalkMap (f x)).hom

theorem

kwFF15_kerEq_of_openImmersion

L120 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.kwFF15_kerEq_of_openImmersion

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

theorem kwFF15_kerEq_of_openImmersion {S X Z : Scheme.{u}} (f : X ⟶ S) (m : Z ⟶ X)
    [IsOpenImmersion m] (s : S) (q : f.fiber s)
    (hq : (f.fiberι s) q ∈ Set.range m)
    (hall : ∀ w : (m ≫ f).fiber s,
      RingHom.ker (((m ≫ f).fiberι s).stalkMap w).hom =
        (IsLocalRing.maximalIdeal
          (S.presheaf.stalk ((m ≫ f) (((m ≫ f).fiberι s) w)))).map
          ((m ≫ f).stalkMap (((m ≫ f).fiberι s) w)).hom) :
    RingHom.ker ((f.fiberι s).stalkMap q).hom =
      (IsLocalRing.maximalIdeal (S.presheaf.stalk (f ((f.fiberι s) q)))).map
        (f.stalkMap ((f.fiberι s) q)).hom

theorem

kwFF15_ker_of_affine

L177 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.kwFF15_ker_of_affine

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

theorem kwFF15_ker_of_affine (hAff : KwFF15FiberιStalkMapKerAffine.{u}) :
    KwFF14FiberιStalkMapKer.{u}

theorem

kwFF16_specStalkMap_toStalk

L201 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.kwFF16_specStalkMap_toStalk

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

theorem kwFF16_specStalkMap_toStalk {R S : Type u} [CommRing R] [CommRing S]
    (φ : R →+* S) (p : Spec (CommRingCat.of S)) :
    StructureSheaf.toStalk R ((Spec.map (CommRingCat.ofHom φ)).base p) ≫
        (Spec.map (CommRingCat.ofHom φ)).stalkMap p =
      CommRingCat.ofHom φ ≫ StructureSheaf.toStalk S p

theorem

kwFF16_wireIdeal_eq_pBq

L208 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.kwFF16_wireIdeal_eq_pBq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

theorem kwFF16_wireIdeal_eq_pBq {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    (x : Spec (CommRingCat.of S)) :
    (IsLocalRing.maximalIdeal (↑((Spec (CommRingCat.of R)).presheaf.stalk
        ((Spec.map (CommRingCat.ofHom (algebraMap R S))).base x)))).map
      ((Spec.map (CommRingCat.ofHom (algebraMap R S))).stalkMap x).hom =
    (((Spec.map (CommRingCat.ofHom (algebraMap R S))).base x).asIdeal.map (algebraMap R S)).map
      (StructureSheaf.toStalk S x).hom

theorem

kwFF16_ker_specIncludeRight_stalkMap

L238 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.kwFF16_ker_specIncludeRight_stalkMap

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

theorem kwFF16_ker_specIncludeRight_stalkMap {R S : Type u} [CommRing R] [CommRing S]
    [Algebra R S] (s : PrimeSpectrum R) (Q : Spec (CommRingCat.of (s.asIdeal.Fiber S)))
    [hLO : ((Spec.map (CommRingCat.ofHom (RingHomClass.toRingHom
      (Algebra.TensorProduct.includeRight
        (R := R) (A := s.asIdeal.ResidueField) (B := S))))).base Q).asIdeal.LiesOver
      s.asIdeal] :
    RingHom.ker ((Spec.map (CommRingCat.ofHom (RingHomClass.toRingHom
        (Algebra.TensorProduct.includeRight
          (R := R) (A := s.asIdeal.ResidueField) (B := S))))).stalkMap Q).hom =
      (s.asIdeal.map (algebraMap R S)).map
        (StructureSheaf.toStalk S ((Spec.map (CommRingCat.ofHom (RingHomClass.toRingHom
          (Algebra.TensorProduct.includeRight
            (R := R) (A := s.asIdeal.ResidueField) (B := S))))).base Q)).hom

theorem

kwFF16_kerEq_congr_ι

L301 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.kwFF16_kerEq_congr_ι

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

theorem kwFF16_kerEq_congr_ι {S X W : Scheme.{u}} (f : X ⟶ S) (ι ι' : W ⟶ X)
    (hι : ι = ι') (q : W)
    (h : RingHom.ker (ι'.stalkMap q).hom =
      (IsLocalRing.maximalIdeal (S.presheaf.stalk (f.base (ι'.base q)))).map
        (f.stalkMap (ι'.base q)).hom) :
    RingHom.ker (ι.stalkMap q).hom =
      (IsLocalRing.maximalIdeal (S.presheaf.stalk (f.base (ι.base q)))).map
        (f.stalkMap (ι.base q)).hom

theorem

kwFF16_affineKer_discharge

L311 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.KERPort.kwFF16_affineKer_discharge

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable section
namespace KERPort

Lean source · statement

theorem kwFF16_affineKer_discharge : KwFF15FiberιStalkMapKerAffine.{u}

theorem

ker_fiberIota_stalkMap_eq_maximalIdeal_map

L353 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.FOFUInline.ker_fiberIota_stalkMap_eq_maximalIdeal_map

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory AlgebraicGeometry KERPort in

Lean source · statement

theorem FOFUInline.ker_fiberIota_stalkMap_eq_maximalIdeal_map
    {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R))
    (s : Spec (CommRingCat.of R)) (q : f.fiber s) :
    RingHom.ker ((f.fiberι s).stalkMap q).hom =
      (IsLocalRing.maximalIdeal
        ((Spec (CommRingCat.of R)).presheaf.stalk (f.base ((f.fiberι s).base q)))).map
        (f.stalkMap ((f.fiberι s).base q)).hom

abbrev

KwSchemeEndoFibrewiseFlat

L369 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.KwSchemeEndoFibrewiseFlat

Documentation

The assertion that the endomorphism induced on every scheme-theoretic fiber is flat.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

abbrev KwSchemeEndoFibrewiseFlat {S X : Scheme.{u}} (f : X ⟶ S) (h : X ⟶ X)
    (hcomm : h ≫ f = f) : Prop

abbrev

KwFF7StalkFibreFlatBridgeSpecR

L375 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.KwFF7StalkFibreFlatBridgeSpecR

Documentation

The assertion transporting fiberwise flatness to the induced map between stalk quotients by the base maximal ideal.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

abbrev KwFF7StalkFibreFlatBridgeSpecR : Prop

theorem

kwFF8_fibreEndo_fst

L401 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.kwFF8_fibreEndo_fst

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

theorem kwFF8_fibreEndo_fst {S X : Scheme.{u}} (f : X ⟶ S) (h : X ⟶ X)
    (hcomm : h ≫ f = f) (s : S) :
    schemeFibreEndo f h hcomm s ≫ Limits.pullback.fst _ _
      = Limits.pullback.fst _ _ ≫ h

theorem

kwFF8_fiberι_fibreEndo

L407 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.kwFF8_fiberι_fibreEndo

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

theorem kwFF8_fiberι_fibreEndo {S X : Scheme.{u}} (f : X ⟶ S) (h : X ⟶ X)
    (hcomm : h ≫ f = f) (s : S) (p : f.fiber s) :
    f.fiberι s (schemeFibreEndo f h hcomm s p) = h (f.fiberι s p)

def

kwFF8_asFiberOf

L416 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.kwFF8_asFiberOf

Documentation

View the original point in the fiber above the base image of its endomorphism image, using the over-base identity.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

def kwFF8_asFiberOf {S X : Scheme.{u}} (f : X ⟶ S) (h : X ⟶ X) (hcomm : h ≫ f = f)
    (x : X) : f.fiber (f.base (h.base x))

theorem

kwFF8_fiberι_asFiberOf

L421 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.kwFF8_fiberι_asFiberOf

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

theorem kwFF8_fiberι_asFiberOf {S X : Scheme.{u}} (f : X ⟶ S) (h : X ⟶ X)
    (hcomm : h ≫ f = f) (x : X) :
    f.fiberι (f.base (h.base x)) (kwFF8_asFiberOf f h hcomm x) = x

theorem

kwFF8_fibreEndo_asFiberOf

L426 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.kwFF8_fibreEndo_asFiberOf

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

theorem kwFF8_fibreEndo_asFiberOf {S X : Scheme.{u}} (f : X ⟶ S) (h : X ⟶ X)
    (hcomm : h ≫ f = f) (x : X) :
    (schemeFibreEndo f h hcomm (f.base (h.base x))).base (kwFF8_asFiberOf f h hcomm x)
      = f.asFiber (h.base x)

abbrev

KwFF8KmfEquivNaturality

L435 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.KwFF8KmfEquivNaturality

Documentation

The assertion that the stalk-to-fiber-quotient identifications commute with the over-base endomorphism.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

abbrev KwFF8KmfEquivNaturality : Prop

theorem

kwFF8_specRbridge_of_kmfNat

L468 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.kwFF8_specRbridge_of_kmfNat

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

theorem kwFF8_specRbridge_of_kmfNat (hNat : KwFF8KmfEquivNaturality.{u}) :
    KwFF7StalkFibreFlatBridgeSpecR.{u}

abbrev

KwFF14FiberιStalkMapKer

L502 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.KwFF14FiberιStalkMapKer

Documentation

The affine-base fiber-stalk kernel assertion: the fiber inclusion kills exactly the mapped maximal ideal of the base stalk.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

abbrev KwFF14FiberιStalkMapKer : Prop

theorem

fiberιKer_stub

L510 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.fiberιKer_stub

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

theorem fiberιKer_stub : KwFF14FiberιStalkMapKer.{u}

theorem

kwFF14_fiberιStalkMap_surjective

L514 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.kwFF14_fiberιStalkMap_surjective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

theorem kwFF14_fiberιStalkMap_surjective {X Y : Scheme.{u}} (f : X ⟶ Y) (s : Y)
    (q : f.fiber s) : Function.Surjective ((f.fiberι s).stalkMap q).hom

theorem

kwFF14_map_stalkMap_congr_point

L518 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.kwFF14_map_stalkMap_congr_point

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

theorem kwFF14_map_stalkMap_congr_point {S X : Scheme.{u}} (f : X ⟶ S) (y y' : X)
    (hyy' : y = y') :
    ((IsLocalRing.maximalIdeal (S.presheaf.stalk (f.base y))).map (f.stalkMap y).hom).map
        (X.presheaf.stalkCongr (.of_eq hyy')).hom.hom =
      (IsLocalRing.maximalIdeal (S.presheaf.stalk (f.base y'))).map (f.stalkMap y').hom

theorem

kwFF14_stalkMap_stalkCongr_nat

L526 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.kwFF14_stalkMap_stalkCongr_nat

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

theorem kwFF14_stalkMap_stalkCongr_nat {X : Scheme.{u}} (h : X ⟶ X) (y y' z : X)
    (hyy' : y = y') (hzy : z = h.base y) (hzy' : z = h.base y') (a : X.presheaf.stalk z) :
    (h.stalkMap y').hom ((X.presheaf.stalkCongr (.of_eq hzy')).hom a) =
      (X.presheaf.stalkCongr (.of_eq hyy')).hom
        ((h.stalkMap y).hom ((X.presheaf.stalkCongr (.of_eq hzy)).hom a))

theorem

kwFF14_wireIdeal_congr_hom

L535 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.kwFF14_wireIdeal_congr_hom

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

theorem kwFF14_wireIdeal_congr_hom {S X : Scheme.{u}} (g g' : X ⟶ S) (hgg' : g = g')
    (y : X) :
    (IsLocalRing.maximalIdeal (S.presheaf.stalk (g.base y))).map (g.stalkMap y).hom =
      (IsLocalRing.maximalIdeal (S.presheaf.stalk (g'.base y))).map (g'.stalkMap y).hom

theorem

kwFF14_kmfCompatEquiv

L541 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.kwFF14_kmfCompatEquiv

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

theorem kwFF14_kmfCompatEquiv {X Y : Scheme.{u}} (f : X ⟶ Y) (s : Y) (q : f.fiber s)
    {I : Ideal (X.presheaf.stalk ((f.fiberι s).base q))}
    (hI : RingHom.ker ((f.fiberι s).stalkMap q).hom = I) :
    ∃ (e : (f.fiber s).presheaf.stalk q ≃+* (X.presheaf.stalk ((f.fiberι s).base q)) ⧸ I),
      ∀ a, e (((f.fiberι s).stalkMap q).hom a) = Ideal.Quotient.mk I a

theorem

kwFF14_kmfCompatEquiv_transport

L555 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.kwFF14_kmfCompatEquiv_transport

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

theorem kwFF14_kmfCompatEquiv_transport {X Y : Scheme.{u}} (f : X ⟶ Y) (s : Y)
    (q : f.fiber s) (y' : X) (hyy' : (f.fiberι s).base q = y')
    {I' : Ideal (X.presheaf.stalk y')}
    (hI' : (RingHom.ker ((f.fiberι s).stalkMap q).hom).map
        (X.presheaf.stalkCongr (.of_eq hyy')).hom.hom = I') :
    ∃ (e : (f.fiber s).presheaf.stalk q ≃+* (X.presheaf.stalk y') ⧸ I'),
      e.toRingHom.comp ((f.fiberι s).stalkMap q).hom =
        (Ideal.Quotient.mk I').comp (X.presheaf.stalkCongr (.of_eq hyy')).hom.hom

theorem

kwFF14_kmfNat_of_ker

L572 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.StalkFibrePort.kwFF14_kmfNat_of_ker

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
namespace StalkFibrePort

Lean source · statement

theorem kwFF14_kmfNat_of_ker (hKer : KwFF14FiberιStalkMapKer.{u}) :
    KwFF8KmfEquivNaturality.{u}

theorem

flat_stalkQuotient_of_forall_flat_schemeFibreEndo

L681 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.FOFUInline.flat_stalkQuotient_of_forall_flat_schemeFibreEndo

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open CategoryTheory AlgebraicGeometry

Lean source · full declaration

theorem FOFUInline.flat_stalkQuotient_of_forall_flat_schemeFibreEndo
    {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R))
    (h : X ⟶ X) (hcomm : h ≫ f = f) [Smooth f] [IsSeparated f] (x : X)
    (hfib : ∀ s, Flat (schemeFibreEndo f h hcomm s)) :
    letI := (f.stalkMap (h.base x)).hom.toAlgebra
    letI := (h.stalkMap x).hom.toAlgebra
    letI := ((h.stalkMap x).hom.comp (f.stalkMap (h.base x)).hom).toAlgebra
    haveI : IsScalarTower ((Spec (CommRingCat.of R)).presheaf.stalk (f.base (h.base x)))
        (X.presheaf.stalk (h.base x)) (X.presheaf.stalk x) := .of_algebraMap_eq' rfl
    letI := Ideal.Quotient.algebraQuotientOfLEComap
      (p := (IsLocalRing.maximalIdeal
        ((Spec (CommRingCat.of R)).presheaf.stalk (f.base (h.base x)))).map
        (f.stalkMap (h.base x)).hom)
      (P := (IsLocalRing.maximalIdeal
        ((Spec (CommRingCat.of R)).presheaf.stalk (f.base (h.base x)))).map
        ((h.stalkMap x).hom.comp (f.stalkMap (h.base x)).hom))
      (by rw [← Ideal.map_le_iff_le_comap, Ideal.map_map]; exact le_rfl)
    Module.Flat ((X.presheaf.stalk (h.base x)) ⧸
        (IsLocalRing.maximalIdeal
          ((Spec (CommRingCat.of R)).presheaf.stalk (f.base (h.base x)))).map
          (f.stalkMap (h.base x)).hom)
      ((X.presheaf.stalk x) ⧸
        (IsLocalRing.maximalIdeal
          ((Spec (CommRingCat.of R)).presheaf.stalk (f.base (h.base x)))).map
          ((h.stalkMap x).hom.comp (f.stalkMap (h.base x)).hom)) := by
  exact (StalkFibrePort.kwFF8_specRbridge_of_kmfNat (StalkFibrePort.kwFF14_kmfNat_of_ker
    StalkFibrePort.fiberιKer_stub))
    R f h hcomm x (fun s => hfib s)

theorem

isPullback_schemeFibreEndo

L714 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.Ws6Bf75.isPullback_schemeFibreEndo

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open CategoryTheory AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace Ws6Bf75

Lean source · statement

theorem isPullback_schemeFibreEndo {S X : Scheme.{u}} (f : X ⟶ S) (h : X ⟶ X)
    (hcomm : h ≫ f = f) (s : S) :
    IsPullback (schemeFibreEndo f h hcomm s)
      (pullback.fst f (S.fromSpecResidueField s))
      (pullback.fst f (S.fromSpecResidueField s)) h

theorem

flat_schemeFibreEndo_schemeNsmul

L730 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.FOFUInline.flat_schemeFibreEndo_schemeNsmul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open CategoryTheory AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian

Lean source · statement

theorem FOFUInline.flat_schemeFibreEndo_schemeNsmul
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    {J : Scheme.{u}} {f : J ⟶ Spec (CommRingCat.of R)} (L : RelativeGroupLaw R f)
    (hJ : AbelianSchemePropertyBundle R f) (n : ℕ)
    (hfin : IsFinite (L.schemeNsmul n)) (s : Spec (CommRingCat.of R)) :
    Flat (schemeFibreEndo f (L.schemeNsmul n) (L.schemeNsmul_over n) s)

theorem

flat_schemeNsmul_of_fibrewiseFlat

L748 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle.FOFUInline.flat_schemeNsmul_of_fibrewiseFlat

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
attribute [-instance] instTopologicallyFGOfFiniteType
attribute [-simp] RegularLocalRingQuotientAscent.dualNumberFst_apply
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open CategoryTheory AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
open CategoryTheory AlgebraicGeometry CategoryTheory.Limits NeronModelInfra GoodReductionJacobian

Lean source · statement

theorem FOFUInline.flat_schemeNsmul_of_fibrewiseFlat
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    {J : Scheme.{u}} {f : J ⟶ Spec (CommRingCat.of R)} (L : RelativeGroupLaw R f)
    (hJ : AbelianSchemePropertyBundle R f) (n : ℕ)
    (hfib : ∀ s, Flat (schemeFibreEndo f (L.schemeNsmul n) (L.schemeNsmul_over n) s)) :
    Flat (L.schemeNsmul n)

theorem

flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle

L805 ↗

GoodReductionJacobian.RelativeGroupLaw.flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle

Source context 7 commands

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

section ProofImplementation
namespace GoodReductionJacobian.RelativeGroupLaw
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open NeronModelInfra GoodReductionJacobian
open _root_.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs in
open RelativeGroupLaw_flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle in

Lean source · statement

theorem flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    {J : Scheme.{u}} {f : J ⟶ Spec (CommRingCat.of R)} (L : RelativeGroupLaw R f)
    (hJ : AbelianSchemePropertyBundle R f)
    (n : ℕ) (hfin : IsFinite (L.schemeNsmul n)) :
    Flat (L.schemeNsmul n)

Module documentation

Relative Group Law flat scheme Nsmul of is Finite of abelian Scheme Property Bundle

Declarations