Module

LinearMap_isOpen_setOf_surjective_baseChange_residueField.lean

Nyll.AlgebraicCurves.Foundations.Algebra.LinearMap_isOpen_setOf_surjective_baseChange_residueField

1 declaration indexed from sourceView source ↗

Module documentation

The locus where a linear map is surjective after residue-field base change is open.

Imports5

Mathlib.RingTheory.LocalRing.Module
Mathlib.RingTheory.Spectrum.Prime.Module
Mathlib.LinearAlgebra.TensorProduct.Quotient
Mathlib.LinearAlgebra.TensorProduct.RightExactness
Mathlib.Tactic.Ext

Imported by2

theorem

isOpen_setOf_surjective_baseChange_residueField

L32 ↗

LinearMap.isOpen_setOf_surjective_baseChange_residueField

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_isOpen_setOf_surjective_baseChange_residueField
universe u v w
open TensorProduct

Lean source · statement

theorem _root_.LinearMap.isOpen_setOf_surjective_baseChange_residueField
    {A : Type u} [CommRing A] {P : Type v} {Q : Type w} [AddCommGroup P] [Module A P]
      [AddCommGroup Q] [Module A Q]
    (d : P →ₗ[A] Q) [Module.Finite A (Q ⧸ LinearMap.range d)] :
    IsOpen {𝔭 : PrimeSpectrum A | Function.Surjective (d.baseChange 𝔭.asIdeal.ResidueField)}

Module documentation

Declarations

isOpen_setOf_surjective_baseChange_residueField