Module

InertiaCoefficientContraction.lean

Nyll.SchemeTheory.RingTheory.Ramification.InertiaCoefficientContraction

1 declaration indexed from sourceView source ↗

Module documentation

Contraction of inertia difference conditions

Proves that the inertia difference condition descends to a contracted ideal along a commuting square of coefficient maps.

Imports2

Mathlib.RingTheory.Ideal.Maps
Mathlib.Algebra.Ring.Hom.Defs

Imported by2

theorem

inertiaDifference_comap_of_coefficient_square

L23 ↗

SchemeTheory.inertiaDifference_comap_of_coefficient_square

Documentation

The actual inertia difference condition descends along a proved coefficient square to the literal contracted prime.

Source context 2 commands

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

namespace SchemeTheory
universe u v

Lean source · statement

theorem inertiaDifference_comap_of_coefficient_square
    {B : Type u} {C : Type v} [CommRing B] [CommRing C]
    (f : B →+* C) (s : B →+* B) (t : C →+* C) (Q : Ideal C)
    (hcomm : f.comp s = t.comp f)
    (ht : ∀ c : C, t c - c ∈ Q) :
    ∀ b : B, s b - b ∈ Q.comap f

Module documentation

Contraction of inertia difference conditions

Declarations

inertiaDifference_comap_of_coefficient_square