ModuleFinitePresentationHomBaseChange.lean
Nyll.EtaleFundamentalGroups.Purity.Local.FinitePresentationHomBaseChange
3 declarations indexed from sourceView source ↗ Module documentation
Flat base change for Hom from a finitely presented module
For a flat algebra S / R, the canonical map
Hom_R(M, N) → Hom_S(S ⊗ M, S ⊗ N)
is a base-change map when M is finitely presented. The finite-presentation result follows from Module.FinitePresentation.isBaseChange_map; the finite-free case and precomposition compatibility are recorded here for downstream use.
Imports2
- Mathlib.Algebra.Module.FinitePresentation
- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Imported by2
Declarations
EtaleFundamentalGroups.linearMap_baseChangeHom_comp_lcomp
DocumentationBase change of a linear map commutes with precomposition. This is the commutative square used in both the finite-presentation Hom comparison and the later Ext¹ comparison.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe u v
open scoped TensorProduct
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
variable {M N P : Type v}
variable [AddCommGroup M] [Module R M]
variable [AddCommGroup N] [Module R N]
variable [AddCommGroup P] [Module R P]
EtaleFundamentalGroups.linearMap_baseChangeHom_isBaseChange_of_free_finite
DocumentationThe canonical Hom comparison is a base change when its first variable is finite free.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe u v
open scoped TensorProduct
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
variable {M N P : Type v}
variable [AddCommGroup M] [Module R M]
variable [AddCommGroup N] [Module R N]
variable [AddCommGroup P] [Module R P]
EtaleFundamentalGroups.linearMap_baseChangeHom_isBaseChange_of_finitePresentation_of_flat
DocumentationFor a flat algebra, the canonical Hom comparison is a base change when the first variable is finitely presented.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe u v
open scoped TensorProduct
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
variable {M N P : Type v}
variable [AddCommGroup M] [Module R M]
variable [AddCommGroup N] [Module R N]
variable [AddCommGroup P] [Module R P]