Module

Ideal_span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing.lean

Nyll.AlgebraicCurves.Valuations.Ideal_span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing

5 declarations indexed from sourceView source ↗

Module documentation

Ideal span algebra Norm eq of ker eq span of is Discrete Valuation Ring

Imports7

Mathlib.RingTheory.Localization.BaseChange
Mathlib.RingTheory.LocalProperties.Basic
Mathlib.LinearAlgebra.ExteriorPower.Basis
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.TensorProduct.Free
Nyll.AlgebraicCurves.Foundations.Algebra.exteriorPower_map_mulLeft_apply_eq_norm_smul
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.exteriorPower_range_map_subtype_eq_maximalIdeal_smul_top

Imported by2

theorem

range_smul_id_eq

L34 ↗

AlgebraicCurves.Valuations.Proofs.Ideal_span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing.N3Alg.range_smul_id_eq

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace Ideal_span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing
open scoped TensorProduct
namespace N3Alg

Lean source · statement

theorem range_smul_id_eq {R : Type*} [CommRing R] {V : Type*} [AddCommGroup V] [Module R V] (r : R)
  :
    LinearMap.range (r • (LinearMap.id : V →ₗ[R] V)) = Ideal.span {r} • (⊤ : Submodule R V)

theorem

ideal_eq_of_smul_top_eq

L46 ↗

AlgebraicCurves.Valuations.Proofs.Ideal_span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing.N3Alg.ideal_eq_of_smul_top_eq

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace Ideal_span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing
open scoped TensorProduct
namespace N3Alg

Lean source · statement

theorem ideal_eq_of_smul_top_eq {R : Type*} [CommRing R] {V : Type*} [AddCommGroup V] [Module R V]
    {ι : Type*} [Unique ι] (b : Module.Basis ι R V) {I J : Ideal R} (h : I • (⊤ : Submodule R V) =
      J • ⊤) : I = J

theorem

norm_one_tmul_eq

L56 ↗

AlgebraicCurves.Valuations.Proofs.Ideal_span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing.N3Alg.norm_one_tmul_eq

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace Ideal_span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing
open scoped TensorProduct
namespace N3Alg

Lean source · statement

theorem norm_one_tmul_eq {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
    {ι : Type*} [Finite ι]
     (b : Module.Basis ι A B) (L : Type*) [CommRing L] [Algebra A L] (x : B) :
    Algebra.norm L ((1 : L) ⊗ₜ[A] x) = algebraMap A L (Algebra.norm A x)

theorem

span_norm_tmul_eq_maximalIdeal

L80 ↗

AlgebraicCurves.Valuations.Proofs.Ideal_span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing.N3Alg.span_norm_tmul_eq_maximalIdeal

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace Ideal_span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing
open scoped TensorProduct
namespace N3Alg
section AtM
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] [Module.Free A B] [Module.Finite A B]
  {K : Type*} [Field K] (χ : B →+* K) (hχ : Function.Surjective (χ.comp (algebraMap A B)))
  (g : B) (hg : RingHom.ker χ = Ideal.span {g})
  (𝔪 : Ideal A) (h𝔪 : RingHom.ker (χ.comp (algebraMap A B)) = 𝔪) [𝔪.IsMaximal]
  (L : Type*) [CommRing L] [Algebra A L] [IsLocalization.AtPrime L 𝔪] [IsDomain L]
    [IsDiscreteValuationRing L]
include hχ hg h𝔪 in

Lean source · statement

theorem span_norm_tmul_eq_maximalIdeal :
    Ideal.span {Algebra.norm L ((1 : L) ⊗ₜ[A] g)} = IsLocalRing.maximalIdeal L

theorem

span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing

L177 ↗

Ideal.span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace Ideal_span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing
open scoped TensorProduct
namespace N3Alg
universe u

Lean source · statement

theorem _root_.Ideal.span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing
    {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] [Module.Free A B] [Module.Finite A B]
    {K : Type u} [Field K] (χ : B →+* K) (hχ : Function.Surjective (χ.comp (algebraMap A B)))
    (g : B) (hg : RingHom.ker χ = Ideal.span {g})
    (𝔪 : Ideal A) (h𝔪 : RingHom.ker (χ.comp (algebraMap A B)) = 𝔪) [𝔪.IsMaximal]
    (Aₘ : Type u) [CommRing Aₘ] [Algebra A Aₘ] [IsLocalization.AtPrime Aₘ 𝔪]
    [IsDomain Aₘ] [IsDiscreteValuationRing Aₘ] :
    Ideal.span {Algebra.norm A g} = 𝔪

Module documentation

Ideal span algebra Norm eq of ker eq span of is Discrete Valuation Ring

Declarations

range_smul_id_eq

ideal_eq_of_smul_top_eq

norm_one_tmul_eq

span_norm_tmul_eq_maximalIdeal

span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing