Module

FinitePresentationExtOneBaseChange.lean

Nyll.EtaleFundamentalGroups.Purity.Local.FinitePresentationExtOneBaseChange

13 declarations indexed from sourceView source ↗

Module documentation

Flat base change for `Ext¹` from a finitely presented module

Over a noetherian ring, the first syzygy of a finitely presented module is again finitely presented. The contravariant long exact Ext sequence of a finite-free presentation therefore expresses Ext¹ as a cokernel of two Hom modules to which finite-presentation base change applies.

Imports8

Nyll.EtaleFundamentalGroups.Purity.Local.FinitePresentationHomBaseChange
Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Mathlib.Algebra.Category.ModuleCat.Descent
Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Mathlib.LinearAlgebra.TensorProduct.Map
Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact
Mathlib.RingTheory.TensorProduct.Free

Imported by2

theorem

extendScalarsTensorAlgebra_eq

L36 ↗

EtaleFundamentalGroups.extendScalarsTensorAlgebra_eq

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open scoped TensorProduct ModuleCat.Algebra ChangeOfRings
namespace EtaleFundamentalGroups
universe u
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]

Lean source · statement

theorem extendScalarsTensorAlgebra_eq :
    ((algebraMap S S).comp (algebraMap R S)).toAlgebra =
      (inferInstance : Algebra R S)

theorem

extendScalarsTensorModule_eq

L43 ↗

EtaleFundamentalGroups.extendScalarsTensorModule_eq

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open scoped TensorProduct ModuleCat.Algebra ChangeOfRings
namespace EtaleFundamentalGroups
universe u
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]

Lean source · statement

theorem extendScalarsTensorModule_eq :
    ((ModuleCat.restrictScalars (algebraMap R S)).obj
        (ModuleCat.of S S)).isModule =
      (@Algebra.toModule R S _ _ (inferInstance : Algebra R S))

def

extendScalarsTensorEquiv

L53 ↗

EtaleFundamentalGroups.extendScalarsTensorEquiv

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open scoped TensorProduct ModuleCat.Algebra ChangeOfRings
namespace EtaleFundamentalGroups
universe u
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]

Lean source · statement

def extendScalarsTensorEquiv (Q : ModuleCat.{u} R) :
    (ModuleCat.extendScalars (algebraMap R S)).obj Q ≃ₗ[S] S ⊗[R] Q

theorem

extendScalarsTensorEquiv_tmul

L82 ↗

EtaleFundamentalGroups.extendScalarsTensorEquiv_tmul

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open scoped TensorProduct ModuleCat.Algebra ChangeOfRings
namespace EtaleFundamentalGroups
universe u
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]

Lean source · full declaration

theorem extendScalarsTensorEquiv_tmul (Q : ModuleCat.{u} R) (s : S) (q : Q) :
    extendScalarsTensorEquiv (S := S) Q
        (show (ModuleCat.extendScalars (algebraMap R S)).obj Q from
          s ⊗ₜ[R,algebraMap R S] q) = s ⊗ₜ[R] q := by
  rfl

theorem

extendScalarsTensorEquiv_symm_tmul

L88 ↗

EtaleFundamentalGroups.extendScalarsTensorEquiv_symm_tmul

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open scoped TensorProduct ModuleCat.Algebra ChangeOfRings
namespace EtaleFundamentalGroups
universe u
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]

Lean source · full declaration

theorem extendScalarsTensorEquiv_symm_tmul (Q : ModuleCat.{u} R) (s : S) (q : Q) :
    (extendScalarsTensorEquiv (S := S) Q).symm (s ⊗ₜ[R] q) =
      (show (ModuleCat.extendScalars (algebraMap R S)).obj Q from
        s ⊗ₜ[R,algebraMap R S] q) := by
  apply (extendScalarsTensorEquiv (S := S) Q).injective
  rw [LinearEquiv.apply_symm_apply, extendScalarsTensorEquiv_tmul]

instance

moduleCatExtendScalarsLinearOverBase

L97 ↗

EtaleFundamentalGroups.moduleCatExtendScalarsLinearOverBase

Documentation

Extension of scalars is linear over the base ring when the target module category is equipped with its restriction-of-scalars linear structure.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open scoped TensorProduct ModuleCat.Algebra ChangeOfRings
namespace EtaleFundamentalGroups
universe u
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]

Lean source · full declaration

instance moduleCatExtendScalarsLinearOverBase :
    (ModuleCat.extendScalars (algebraMap R S)).Linear R where
  map_smul f r := by
    apply ModuleCat.hom_injective
    dsimp only [ModuleCat.extendScalars, ModuleCat.ExtendScalars.map',
      ModuleCat.hom_ofHom]
    let : Algebra R S := ((algebraMap S S).comp (algebraMap R S)).toAlgebra
    exact LinearMap.baseChange_smul r f.hom

instance

moduleCatExtendScalarsPreservesFiniteLimits

L108 ↗

EtaleFundamentalGroups.moduleCatExtendScalarsPreservesFiniteLimits

Documentation

Flat extension of scalars preserves finite limits. This instance is the exactness input needed by the functorial map on Ext.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open scoped TensorProduct ModuleCat.Algebra ChangeOfRings
namespace EtaleFundamentalGroups
universe u
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
/-- Extension of scalars is linear over the base ring when the target module
category is equipped with its restriction-of-scalars linear structure. -/
noncomputable local instance moduleCatExtendScalarsLinearOverBase :
    (ModuleCat.extendScalars (algebraMap R S)).Linear R where
  map_smul f r := by
    apply ModuleCat.hom_injective
    dsimp only [ModuleCat.extendScalars, ModuleCat.ExtendScalars.map',
      ModuleCat.hom_ofHom]
    let : Algebra R S := ((algebraMap S S).comp (algebraMap R S)).toAlgebra
    exact LinearMap.baseChange_smul r f.hom

Lean source · statement

instance moduleCatExtendScalarsPreservesFiniteLimits
    [Module.Flat R S] :
    PreservesFiniteLimits
      (ModuleCat.extendScalars.{u, u, u} (algebraMap R S))

instance

moduleCatExtendScalarsAdditive

L116 ↗

EtaleFundamentalGroups.moduleCatExtendScalarsAdditive

Documentation

A flat extension-of-scalars functor is additive.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open scoped TensorProduct ModuleCat.Algebra ChangeOfRings
namespace EtaleFundamentalGroups
universe u
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
/-- Extension of scalars is linear over the base ring when the target module
category is equipped with its restriction-of-scalars linear structure. -/
noncomputable local instance moduleCatExtendScalarsLinearOverBase :
    (ModuleCat.extendScalars (algebraMap R S)).Linear R where
  map_smul f r := by
    apply ModuleCat.hom_injective
    dsimp only [ModuleCat.extendScalars, ModuleCat.ExtendScalars.map',
      ModuleCat.hom_ofHom]
    let : Algebra R S := ((algebraMap S S).comp (algebraMap R S)).toAlgebra
    exact LinearMap.baseChange_smul r f.hom
/-- Flat extension of scalars preserves finite limits.  This instance is
the exactness input needed by the functorial map on `Ext`. -/
noncomputable local instance moduleCatExtendScalarsPreservesFiniteLimits
    [Module.Flat R S] :
    PreservesFiniteLimits
      (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)) :=
  ModuleCat.preservesFiniteLimits_extendScalars_of_flat
    (RingHom.flat_algebraMap_iff.mpr inferInstance)

Lean source · statement

instance moduleCatExtendScalarsAdditive [Module.Flat R S] :
    (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)).Additive

instance

extIsScalarTowerOfAlgebra

L123 ↗

EtaleFundamentalGroups.extIsScalarTowerOfAlgebra

Documentation

The R-action on an Ext group of S-modules obtained from the restriction-of-scalars linear category structure is compatible with its native S-action.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open scoped TensorProduct ModuleCat.Algebra ChangeOfRings
namespace EtaleFundamentalGroups
universe u
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
/-- Extension of scalars is linear over the base ring when the target module
category is equipped with its restriction-of-scalars linear structure. -/
noncomputable local instance moduleCatExtendScalarsLinearOverBase :
    (ModuleCat.extendScalars (algebraMap R S)).Linear R where
  map_smul f r := by
    apply ModuleCat.hom_injective
    dsimp only [ModuleCat.extendScalars, ModuleCat.ExtendScalars.map',
      ModuleCat.hom_ofHom]
    let : Algebra R S := ((algebraMap S S).comp (algebraMap R S)).toAlgebra
    exact LinearMap.baseChange_smul r f.hom
/-- Flat extension of scalars preserves finite limits.  This instance is
the exactness input needed by the functorial map on `Ext`. -/
noncomputable local instance moduleCatExtendScalarsPreservesFiniteLimits
    [Module.Flat R S] :
    PreservesFiniteLimits
      (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)) :=
  ModuleCat.preservesFiniteLimits_extendScalars_of_flat
    (RingHom.flat_algebraMap_iff.mpr inferInstance)
/-- A flat extension-of-scalars functor is additive. -/
noncomputable local instance moduleCatExtendScalarsAdditive [Module.Flat R S] :
    (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)).Additive :=
  (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)).additive_of_preserves_binary_products

Lean source · statement

instance extIsScalarTowerOfAlgebra
    (X Y : ModuleCat.{u} S) (i : ℕ) :
    IsScalarTower R S (Ext X Y i)

theorem

extendScalars_mapExtZero_isBaseChange

L132 ↗

EtaleFundamentalGroups.extendScalars_mapExtZero_isBaseChange

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open scoped TensorProduct ModuleCat.Algebra ChangeOfRings
namespace EtaleFundamentalGroups
universe u
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
/-- Extension of scalars is linear over the base ring when the target module
category is equipped with its restriction-of-scalars linear structure. -/
noncomputable local instance moduleCatExtendScalarsLinearOverBase :
    (ModuleCat.extendScalars (algebraMap R S)).Linear R where
  map_smul f r := by
    apply ModuleCat.hom_injective
    dsimp only [ModuleCat.extendScalars, ModuleCat.ExtendScalars.map',
      ModuleCat.hom_ofHom]
    let : Algebra R S := ((algebraMap S S).comp (algebraMap R S)).toAlgebra
    exact LinearMap.baseChange_smul r f.hom
/-- Flat extension of scalars preserves finite limits.  This instance is
the exactness input needed by the functorial map on `Ext`. -/
noncomputable local instance moduleCatExtendScalarsPreservesFiniteLimits
    [Module.Flat R S] :
    PreservesFiniteLimits
      (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)) :=
  ModuleCat.preservesFiniteLimits_extendScalars_of_flat
    (RingHom.flat_algebraMap_iff.mpr inferInstance)
/-- A flat extension-of-scalars functor is additive. -/
noncomputable local instance moduleCatExtendScalarsAdditive [Module.Flat R S] :
    (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)).Additive :=
  (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)).additive_of_preserves_binary_products
/-- The `R`-action on an `Ext` group of `S`-modules obtained from the
restriction-of-scalars linear category structure is compatible with its
native `S`-action. -/
noncomputable local instance extIsScalarTowerOfAlgebra
    (X Y : ModuleCat.{u} S) (i : ℕ) :
    IsScalarTower R S (Ext X Y i) :=
  IsScalarTower.of_algebraMap_smul fun r x ↦ by
    simp only [Ext.smul_eq_comp_mk₀]
    congr 2
variable [Small.{u} R] [Small.{u} S] [Module.Flat R S]

Lean source · statement

theorem extendScalars_mapExtZero_isBaseChange
    (Q N : ModuleCat.{u} R) [Module.FinitePresentation R Q] :
    IsBaseChange S
      ((ModuleCat.extendScalars (algebraMap R S)).mapExtLinearMap
        R Q N 0)

theorem

ext_precomp_extClass_exact

L196 ↗

EtaleFundamentalGroups.ext_precomp_extClass_exact

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open scoped TensorProduct ModuleCat.Algebra ChangeOfRings
namespace EtaleFundamentalGroups
universe u
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
/-- Extension of scalars is linear over the base ring when the target module
category is equipped with its restriction-of-scalars linear structure. -/
noncomputable local instance moduleCatExtendScalarsLinearOverBase :
    (ModuleCat.extendScalars (algebraMap R S)).Linear R where
  map_smul f r := by
    apply ModuleCat.hom_injective
    dsimp only [ModuleCat.extendScalars, ModuleCat.ExtendScalars.map',
      ModuleCat.hom_ofHom]
    let : Algebra R S := ((algebraMap S S).comp (algebraMap R S)).toAlgebra
    exact LinearMap.baseChange_smul r f.hom
/-- Flat extension of scalars preserves finite limits.  This instance is
the exactness input needed by the functorial map on `Ext`. -/
noncomputable local instance moduleCatExtendScalarsPreservesFiniteLimits
    [Module.Flat R S] :
    PreservesFiniteLimits
      (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)) :=
  ModuleCat.preservesFiniteLimits_extendScalars_of_flat
    (RingHom.flat_algebraMap_iff.mpr inferInstance)
/-- A flat extension-of-scalars functor is additive. -/
noncomputable local instance moduleCatExtendScalarsAdditive [Module.Flat R S] :
    (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)).Additive :=
  (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)).additive_of_preserves_binary_products
/-- The `R`-action on an `Ext` group of `S`-modules obtained from the
restriction-of-scalars linear category structure is compatible with its
native `S`-action. -/
noncomputable local instance extIsScalarTowerOfAlgebra
    (X Y : ModuleCat.{u} S) (i : ℕ) :
    IsScalarTower R S (Ext X Y i) :=
  IsScalarTower.of_algebraMap_smul fun r x ↦ by
    simp only [Ext.smul_eq_comp_mk₀]
    congr 2
variable [Small.{u} R] [Small.{u} S] [Module.Flat R S]

Lean source · statement

theorem ext_precomp_extClass_exact
    {T : ShortComplex (ModuleCat.{u} R)} (hT : T.ShortExact)
    (N : ModuleCat.{u} R) :
    Function.Exact
      ((Ext.mk₀ T.f).precompOfLinear R N (zero_add 0))
      (hT.extClass.precompOfLinear R N (Nat.add_zero 1))

theorem

ext_precomp_extClass_surjective_of_projective

L210 ↗

EtaleFundamentalGroups.ext_precomp_extClass_surjective_of_projective

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open scoped TensorProduct ModuleCat.Algebra ChangeOfRings
namespace EtaleFundamentalGroups
universe u
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
/-- Extension of scalars is linear over the base ring when the target module
category is equipped with its restriction-of-scalars linear structure. -/
noncomputable local instance moduleCatExtendScalarsLinearOverBase :
    (ModuleCat.extendScalars (algebraMap R S)).Linear R where
  map_smul f r := by
    apply ModuleCat.hom_injective
    dsimp only [ModuleCat.extendScalars, ModuleCat.ExtendScalars.map',
      ModuleCat.hom_ofHom]
    let : Algebra R S := ((algebraMap S S).comp (algebraMap R S)).toAlgebra
    exact LinearMap.baseChange_smul r f.hom
/-- Flat extension of scalars preserves finite limits.  This instance is
the exactness input needed by the functorial map on `Ext`. -/
noncomputable local instance moduleCatExtendScalarsPreservesFiniteLimits
    [Module.Flat R S] :
    PreservesFiniteLimits
      (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)) :=
  ModuleCat.preservesFiniteLimits_extendScalars_of_flat
    (RingHom.flat_algebraMap_iff.mpr inferInstance)
/-- A flat extension-of-scalars functor is additive. -/
noncomputable local instance moduleCatExtendScalarsAdditive [Module.Flat R S] :
    (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)).Additive :=
  (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)).additive_of_preserves_binary_products
/-- The `R`-action on an `Ext` group of `S`-modules obtained from the
restriction-of-scalars linear category structure is compatible with its
native `S`-action. -/
noncomputable local instance extIsScalarTowerOfAlgebra
    (X Y : ModuleCat.{u} S) (i : ℕ) :
    IsScalarTower R S (Ext X Y i) :=
  IsScalarTower.of_algebraMap_smul fun r x ↦ by
    simp only [Ext.smul_eq_comp_mk₀]
    congr 2
variable [Small.{u} R] [Small.{u} S] [Module.Flat R S]

Lean source · statement

theorem ext_precomp_extClass_surjective_of_projective
    {T : ShortComplex (ModuleCat.{u} R)} (hT : T.ShortExact)
    (N : ModuleCat.{u} R) [Projective T.X₂] :
    Function.Surjective
      (hT.extClass.precompOfLinear R N (Nat.add_zero 1))

theorem

mapExtOne_isBaseChange_of_finitePresentation_of_flat

L222 ↗

EtaleFundamentalGroups.mapExtOne_isBaseChange_of_finitePresentation_of_flat

Documentation

For a flat algebra over a noetherian ring, the functorial map on Ext¹ from a finitely presented first variable is a base-change map.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open scoped TensorProduct ModuleCat.Algebra ChangeOfRings
namespace EtaleFundamentalGroups
universe u
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
/-- Extension of scalars is linear over the base ring when the target module
category is equipped with its restriction-of-scalars linear structure. -/
noncomputable local instance moduleCatExtendScalarsLinearOverBase :
    (ModuleCat.extendScalars (algebraMap R S)).Linear R where
  map_smul f r := by
    apply ModuleCat.hom_injective
    dsimp only [ModuleCat.extendScalars, ModuleCat.ExtendScalars.map',
      ModuleCat.hom_ofHom]
    let : Algebra R S := ((algebraMap S S).comp (algebraMap R S)).toAlgebra
    exact LinearMap.baseChange_smul r f.hom
/-- Flat extension of scalars preserves finite limits.  This instance is
the exactness input needed by the functorial map on `Ext`. -/
noncomputable local instance moduleCatExtendScalarsPreservesFiniteLimits
    [Module.Flat R S] :
    PreservesFiniteLimits
      (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)) :=
  ModuleCat.preservesFiniteLimits_extendScalars_of_flat
    (RingHom.flat_algebraMap_iff.mpr inferInstance)
/-- A flat extension-of-scalars functor is additive. -/
noncomputable local instance moduleCatExtendScalarsAdditive [Module.Flat R S] :
    (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)).Additive :=
  (ModuleCat.extendScalars.{u, u, u} (algebraMap R S)).additive_of_preserves_binary_products
/-- The `R`-action on an `Ext` group of `S`-modules obtained from the
restriction-of-scalars linear category structure is compatible with its
native `S`-action. -/
noncomputable local instance extIsScalarTowerOfAlgebra
    (X Y : ModuleCat.{u} S) (i : ℕ) :
    IsScalarTower R S (Ext X Y i) :=
  IsScalarTower.of_algebraMap_smul fun r x ↦ by
    simp only [Ext.smul_eq_comp_mk₀]
    congr 2
variable [Small.{u} R] [Small.{u} S] [Module.Flat R S]

Lean source · statement

theorem mapExtOne_isBaseChange_of_finitePresentation_of_flat
    [IsNoetherianRing R]
    (Q N : ModuleCat.{u} R) [Module.FinitePresentation R Q] :
    IsBaseChange S
      ((ModuleCat.extendScalars (algebraMap R S)).mapExtLinearMap
        R Q N 1)

Module documentation

Flat base change for Ext¹ from a finitely presented module

Declarations

Flat base change for `Ext¹` from a finitely presented module