Module

Transport.lean

Nyll.SchemeTheory.Divisors.NormalCrossings.Transport

1 declaration indexed from sourceView source ↗

Module documentation

Transport of split normal-crossings charts

The explicit local chart is invariant under a change of ring model by an isomorphism. This is used to pass between a scheme stalk and the canonical prime-localization model of the same local ring.

Imports3

Nyll.SchemeTheory.Divisors.Basic
Nyll.SchemeTheory.Divisors.NormalCrossings.Basic
Mathlib.RingTheory.Ideal.Quotient.Operations

Imported by3

theorem

map_ringEquiv

L25 ↗

EtaleFundamentalGroups.IsSplitStrictNormalCrossingsAt.map_ringEquiv

Documentation

Split strict-normal-crossings charts are preserved by ring isomorphisms.

Source context 2 commands

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

namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem IsSplitStrictNormalCrossingsAt.map_ringEquiv
    {R S : Type u} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S]
    (e : R ≃+* S) {d r : ℕ} {f : R} {t : Fin d → R}
    (h : IsSplitStrictNormalCrossingsAt f t r) :
    IsSplitStrictNormalCrossingsAt (e f) (e ∘ t) r

Module documentation

Transport of split normal-crossings charts

Declarations

map_ringEquiv