Module

Algebra_exists_lift_basis_of_surjective_of_monogenic_specialFibre.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_exists_lift_basis_of_surjective_of_monogenic_specialFibre

2 declarations indexed from sourceView source ↗

Module documentation

Algebra exists lift basis of surjective of monogenic special Fibre

Imports7

Mathlib.LinearAlgebra.Charpoly.Basic
Mathlib.RingTheory.AdjoinRoot
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.Nakayama
Mathlib.Tactic.Conv
Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.SplitIfs

Imported by2

theorem

main

L39 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_exists_lift_basis_of_surjective_of_monogenic_specialFibre.MonogenicLiftSol.main

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_exists_lift_basis_of_surjective_of_monogenic_specialFibre
open Polynomial
universe u v w x
noncomputable section
namespace MonogenicLiftSol
open Classical in

Lean source · statement

theorem main
    (R' : Type u) [CommRing R'] [IsLocalRing R'] (R : Type v) [CommRing R] [IsLocalRing R]
    (π : R' →+* R) (hπ : Function.Surjective π)
    (C : Type w) [CommRing C] [Algebra R C] (ι : Type x) [Finite ι]
    (e : Module.Basis ι R C) (i₀ : ι) (he : e i₀ = 1)
    (y : C) (hy : ∀ z : C, ∃ q : R[X],
      z - aeval y q ∈ (IsLocalRing.maximalIdeal R) • (⊤ : Submodule R C)) :
    ∃ (C' : Type u) (_ : CommRing C') (_ : Algebra R' C') (e' : Module.Basis ι R' C')
      (σ : C' →+* C),
      e' i₀ = 1 ∧ (∀ r, σ (algebraMap R' C' r) = algebraMap R C (π r)) ∧ ∀ i, σ (e' i) = e i

theorem

exists_lift_basis_of_surjective_of_monogenic_specialFibre

L214 ↗

Algebra.exists_lift_basis_of_surjective_of_monogenic_specialFibre

Source context 5 commands