SwappedBaseChange.lean`

64 declarations, 0 contain sorry, 0 declared as axioms

Closed base change, affine denominator clearing and coherent Grothendieck groups

This development accompanies A Complete Local Domain without a Small Cohen–Macaulay Module (OpenAI, 2026).

lemma OAI.SourcePullbackChart.completedClosedChart_swappedMate_isIso line 27
lemma OAI.SourcePullbackChart.swappedActualMate_chart_isIso line 35
lemma OAI.SourcePullbackChart.swappedActualMate_isIso line 63
abbrev OAI.SourceConeMorphism.completedParameterSpec line 91
abbrev OAI.SourceConeMorphism.parameterModule line 93
lemma OAI.SourceConeMorphism.parameters_preimage_puncture line 96
lemma OAI.SourceConeMorphism.parameterModule_free line 106
instance OAI.SourceConeMorphism.parameterModule_finite line 112
def OAI.SourceConeMorphism.basisIndex line 124
instance OAI.SourceConeMorphism.basisIndex_finite line 130
def OAI.SourceConeMorphism.parameterSheafFreeIso line 137
def OAI.IsoPuncturePushforward.pushPullIso line 162
def OAI.IsoPuncturePushforward.restrictFreeIso line 170
def OAI.IsoPuncturePushforward.pushFreeIso line 177
def OAI.IsoPuncturePushforward.pushforwardComparison line 184
def OAI.IsoPuncturePushforward.reflectFreeIso line 194
def OAI.SourceConeMorphism.pushforwardOverBaseIso line 211
Source documentation
Pushforward along the commuting parameter square.
```
def pushforwardOverBaseIso (M : ModuleCat.{0} ExplicitCone.completedRing) :
    (pushforward completedBlowdown).obj (modelPushforward M) ≅
      (pushforward completedParameterSpec).obj ((pushforward p).obj (E M)) :=
…
```
Mentions: OAI.ExplicitCone.completedRing, OAI.SourceConeMorphism.completedParameterSpec, OAI.SourceConeMorphism.p, OAI.SourceConeMorphism.E
def OAI.SourceConeMorphism.p_puncturePushforwardIso line 222
def OAI.SourceConeMorphism.p_parametersPunctureIso line 228
def OAI.SourceConeMorphism.overBasePunctureComparison line 235
def OAI.SourceConeMorphism.overBasePunctureFreeIso line 247
abbrev OAI.SourceConeMorphism.baseModelPuncture line 255
def OAI.SourceConeMorphism.modelPushforwardFreeIso line 258
Source documentation
The required source framing, obtained from CM freeness and the puncture isomorphisms of both models.
```
def modelPushforwardFreeIso :
    (restrictFunctor baseModelPuncture.ι).obj (modelPushforward M) ≅
    SheafOfModules.free (basisIndex M hdepth) :=
…
```
Mentions: OAI.SourceConeMorphism.basisIndex
def OAI.ActualOpenComparison.pullOverHom line 277
Source documentation
Pull a morphism on a target open to a chart open whose image it contains. The scalar restriction uses the chart ring isomorphism.
```
def pullOverHom (a : M.over W ⟶ N.over W) :
    ((restrictFunctor f).obj M).over V ⟶ ((restrictFunctor f).obj N).over V where
…
```
lemma OAI.ActualOpenComparison.pullOverHom_id line 289
lemma OAI.ActualOpenComparison.pullOverHom_comp line 292
def OAI.ActualOpenComparison.pullOverIso line 297
Source documentation
A puncture isomorphism restricts functorially to the puncture on every affine chart.
```
def pullOverIso (e : M.over W ≅ N.over W) :
    ((restrictFunctor f).obj M).over V ≅ ((restrictFunctor f).obj N).over V where
…
```
lemma OAI.ActualOpenComparison.pullOverHom_global line 305
Source documentation
Compatibility of a global morphism and this chart-open pullback.
```
lemma pullOverHom_global (a : M ⟶ N) :
    pullOverHom f V W h (a.over W) = ((restrictFunctor f).map a).over V := by
…
```
Mentions: OAI.ActualOpenComparison.pullOverHom
lemma OAI.CartierAffineLattice.regular_pow line 319
lemma OAI.CartierAffineLattice.injective_localization line 331

lemma OAI.CartierAffineLattice.exists_sandwich line 340

Source documentation

Clearing denominators in an isomorphism of principal localizations of finitely presented modules gives embeddings in both directions. Their composites are powers of the Cartier equation, by localization of finite-presentation Hom.

lemma exists_sandwich [Module.FinitePresentation R M] [Module.FinitePresentation R N]
    (t : R) (htM : IsSMulRegular M t) (htN : IsSMulRegular N t)
    (f : M →ₗ[R] L) [IsLocalizedModule.Away t f]
    (g : N →ₗ[R] K) [IsLocalizedModule.Away t g] (e : L ≃ₗ[R] K) :
    ∃ (a : M →ₗ[R] N) (b : N →ₗ[R] M) (k : ℕ),
      Function.Injective a ∧ Function.Injective b ∧
      a.comp b = t ^ k • (LinearMap.id : N →ₗ[R] N) ∧
      b.comp a = t ^ k • (LinearMap.id : M →ₗ[R] M) := by
…

def OAI.CartierAffineLattice.punctureSectionsIso line 390
Source documentation
Restriction to a principal open supplies the localized-module isomorphism used for clearing denominators.
```
def punctureSectionsIso {M N : (Spec R).Modules} (U : (Spec R).Opens)
    (e : M.over U ≅ N.over U) : Γ(M, U) ≃ₗ[R] Γ(N, U) := by
…
```

lemma OAI.CartierAffineLattice.exists_sandwich_of_puncture line 398

Source documentation

On an affine Cartier chart the lattice embeddings are obtained from a punctured sheaf isomorphism, rather than supplied as hypotheses.

lemma exists_sandwich_of_puncture
    (M N : ModuleCat R) [Module.FinitePresentation R M] [Module.FinitePresentation R N]
    (t : R) (htM : IsSMulRegular M t) (htN : IsSMulRegular N t)
    (e : (tilde M).over (PrimeSpectrum.basicOpen t) ≅
      (tilde N).over (PrimeSpectrum.basicOpen t)) :
    ∃ (a : M →ₗ[R] N) (b : N →ₗ[R] M) (k : ℕ),
      Function.Injective a ∧ Function.Injective b ∧
      a.comp b = t ^ k • (LinearMap.id : N →ₗ[R] N) ∧
      b.comp a = t ^ k • (LinearMap.id : M →ₗ[R] M) :=
…

lemma OAI.CartierAffineLattice.sandwich_annihilates_quotient line 411

Source documentation

The constructed sandwich kills the cokernel by the same power.

lemma sandwich_annihilates_quotient {M N : Type*} [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] (a : M →ₗ[R] N) (b : N →ₗ[R] M) (t : R) (k : ℕ)
    (hab : a.comp b = t ^ k • (LinearMap.id : N →ₗ[R] N)) :
    ∀ q : N ⧸ a.range, t ^ k • q = 0 := by
…

lemma OAI.CartierAffineLattice.exists_compatible_sandwich line 435

Source documentation

The cleared maps agree with the prescribed puncture isomorphism after multiplication by a shared denominator.

lemma exists_compatible_sandwich
    [Module.FinitePresentation R M] [Module.FinitePresentation R N]
    (t : R) (htM : IsSMulRegular M t) (htN : IsSMulRegular N t)
    (f : M →ₗ[R] L) [IsLocalizedModule.Away t f]
    (g : N →ₗ[R] K) [IsLocalizedModule.Away t g] (e : L ≃ₗ[R] K) :
    ∃ (n : ℕ) (a : M →ₗ[R] N) (b : N →ₗ[R] M),
      Function.Injective a ∧ Function.Injective b ∧
      (∀ x, g (a x) = t ^ n • e (f x)) ∧
      (∀ y, f (b y) = t ^ n • e.symm (g y)) ∧
      a.comp b = t ^ (2 * n) • (LinearMap.id : N →ₗ[R] N) ∧
      b.comp a = t ^ (2 * n) • (LinearMap.id : M →ₗ[R] M) := by
…

lemma OAI.CartierAffineLattice.cleared_extension_unique line 489
Source documentation
A cleared extension of a puncture morphism is unique when the Cartier equation acts regularly on the target.
```
lemma cleared_extension_unique (t : R) (htN : IsSMulRegular N t)
    (g : N →ₗ[R] K) [IsLocalizedModule.Away t g]
    (a b : M →ₗ[R] N) (h : g.comp a = g.comp b) : a = b := by
…
```
def OAI.AffineNaturalScalar.scalar line 503
Source documentation
The scalar of a natural endomorphism on affine module sheaves.
```
def scalar : R := ((tilde.functor R).preimage (b.app (tilde (ModuleCat.of R R)))) 1
```
lemma OAI.AffineNaturalScalar.preimage_apply line 507
Source documentation
Naturality against the cyclic maps from the structure module forces the affine endomorphism to be scalar multiplication on every module.
```
lemma preimage_apply (M : ModuleCat R) (m : M) :
    ((tilde.functor R).preimage (b.app (tilde M))) m = scalar R b • m := by
…
```
Mentions: OAI.AffineNaturalScalar.scalar
lemma OAI.AffineNaturalScalar.preimage_eq line 524
lemma OAI.AffineNaturalScalar.power_zero line 533
Source documentation
Uniform scalar nilpotence of an affine module implies nilpotence of the corresponding sheaf endomorphism.
```
lemma power_zero (M : ModuleCat R) (n : ℕ)
    (h : ∀ m : M, scalar R b ^ n • m = 0) :
    (End.of (b.app (tilde M)) ^ n).asHom = 0 := by
…
```
Mentions: OAI.AffineNaturalScalar.scalar
def OAI.ActualSheafTensor.trivialTensorIso line 580
Source documentation
The tensor functor trivialization of a trivial line.
```
def trivialTensorIso {L : SheafOfModules.{u} (ringSheaf R)}
    (e : L ≅ SheafOfModules.unit _) : tensorLeft R L ≅ 𝟭 _ :=
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.tensorLeft
lemma OAI.ActualSheafTensor.trivialTensorIso_pure line 584

lemma OAI.ActualSheafTensor.trivial_action_eq_smul line 597

Source documentation

Normalizing a line-ideal action by a trivialization is multiplication by the principal equation, on every section module.

lemma trivial_action_eq_smul {L : SheafOfModules.{u} (ringSheaf R)}
    (e : L ≅ SheafOfModules.unit _) (i : L ⟶ SheafOfModules.unit _)
    (M : SheafOfModules.{u} (ringSheaf R)) (U : Cᵒᵖ) (m : M.val.obj U) :
    (((trivialTensorIso R e).inv ≫ idealAction R i).app M).val.app U m =
      (i.val.app U (e.inv.val.app U (1 : R.obj.obj U))) • m := by
…

Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.trivialTensorIso, OAI.ActualSheafTensor.idealAction

lemma OAI.ActualSheafTensor.trivial_action_unit line 623
Source documentation
On the structure sheaf, the normalized tensor action is the trivialized ideal inclusion.
```
lemma trivial_action_unit {L : SheafOfModules.{u} (ringSheaf R)}
    (e : L ≅ SheafOfModules.unit _) (i : L ⟶ SheafOfModules.unit _) :
    ((trivialTensorIso R e).inv ≫ idealAction R i).app (SheafOfModules.unit _) =
      e.inv ≫ i := by
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.trivialTensorIso, OAI.ActualSheafTensor.idealAction
def OAI.CoherentK0.relations line 659
Source documentation
The two usual relations: isomorphic objects have the same class, and short exact sequences are additive.
```
def relations : Set (FreeAbelianGroup C) :=
…
```
def OAI.CoherentK0.Group line 665
Source documentation
Grothendieck group of the exact category underlying an abelian category.
```
def Group := FreeAbelianGroup C ⧸ AddSubgroup.closure (relations C)
```
Mentions: OAI.CoherentK0.relations
instance OAI.CoherentK0.(instance at line 667) line 667
def OAI.CoherentK0.cls line 672
lemma OAI.CoherentK0.cls_iso line 674
lemma OAI.CoherentK0.cls_shortExact line 680
lemma OAI.CoherentK0.cls_exact line 692
Source documentation
The class of an exact triple is the sum of the classes of its two images.
```
lemma cls_exact {S : ShortComplex C} (hS : S.Exact) :
    cls S.X₂ = cls (Abelian.image S.f) + cls (Abelian.image S.g) := by
…
```
Mentions: OAI.CoherentK0.cls
lemma OAI.CoherentK0.cls_image_of_mono line 705
lemma OAI.CoherentK0.cls_image_of_epi line 710

lemma OAI.CoherentK0.six_term_euler line 717

Source documentation

Six-term exactness gives the Euler identity for restriction minus first Tor.

lemma six_term_euler {A B K P Q T : C}
    (f : A ⟶ B) (g : B ⟶ K) (δ : K ⟶ P) (h : P ⟶ Q) (i : Q ⟶ T)
    [Mono f] [Epi i]
    (z₁ : f ≫ g = 0) (z₂ : g ≫ δ = 0) (z₃ : δ ≫ h = 0) (z₄ : h ≫ i = 0)
    (e₁ : (ShortComplex.mk f g z₁).Exact)
    (e₂ : (ShortComplex.mk g δ z₂).Exact)
    (e₃ : (ShortComplex.mk δ h z₃).Exact)
    (e₄ : (ShortComplex.mk h i z₄).Exact) :
    cls Q - cls B = (cls P - cls A) + (cls T - cls K) := by
…

Mentions: OAI.CoherentK0.cls

lemma OAI.CoherentK0.snake_euler line 738

Source documentation

The snake lemma gives the Euler identity for the kernel and cokernel rows.

lemma snake_euler (S : ShortComplex.SnakeInput C) [Mono S.L₁.f] [Epi S.L₂.g] :
    cls S.L₃.X₂ - cls S.L₀.X₂ =
      (cls S.L₃.X₁ - cls S.L₀.X₁) + (cls S.L₃.X₃ - cls S.L₀.X₃) :=
…

Mentions: OAI.CoherentK0.cls

lemma OAI.CoherentK0.snake_euler_in_divisor line 755

Source documentation

The snake Euler identity descends to the divisor category: fullness lifts the connecting morphism and faithfulness reflects exactness.

lemma snake_euler_in_divisor
    (J : D ⥤ C) [J.Full] [J.Faithful] [J.PreservesZeroMorphisms]
    [PreservesFiniteLimits J] [PreservesFiniteColimits J]
    (K Q : ShortComplex D) (S₁ S₂ : ShortComplex C)
    (i : K.map J ⟶ S₁) (m : S₁ ⟶ S₂) (p : S₂ ⟶ Q.map J)
    (wi : i ≫ m = 0) (wp : m ≫ p = 0)
    (hi : IsLimit (KernelFork.ofι i wi))
    (hp : IsColimit (CokernelCofork.ofπ p wp))
    (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) :
    cls Q.X₂ - cls K.X₂ =
      (cls Q.X₁ - cls K.X₁) + (cls Q.X₃ - cls K.X₃) := by
…

Mentions: OAI.CoherentK0.cls

lemma OAI.CoherentK0.cartier_restriction_additive line 813

Source documentation

Restriction minus first Tor is additive for a length-one Cartier resolution.

lemma cartier_restriction_additive
    (J : D ⥤ C) [J.Full] [J.Faithful] [J.PreservesZeroMorphisms]
    [PreservesFiniteLimits J] [PreservesFiniteColimits J]
    (T : C ⥤ C) [T.PreservesZeroMorphisms]
    [PreservesFiniteLimits T] [PreservesFiniteColimits T]
    (K Q : C ⥤ D) [K.PreservesZeroMorphisms] [Q.PreservesZeroMorphisms]
    (κ : K ⋙ J ⟶ T) (ε : T ⟶ 𝟭 C) (π : 𝟭 C ⟶ Q ⋙ J)
    (zK : κ ≫ ε = 0) (zQ : ε ≫ π = 0)
    (hK : ∀ X, IsLimit (KernelFork.ofι (κ.app X) (NatTrans.congr_app zK X)))
    (hQ : ∀ X, IsColimit (CokernelCofork.ofπ (π.app X) (NatTrans.congr_app zQ X)))
    {S : ShortComplex C} (hS : S.ShortExact) :
    cls (Q.obj S.X₂) - cls (K.obj S.X₂) =
…

Mentions: OAI.CoherentK0.cls

lemma OAI.CoherentK0.cls_zero line 860
lemma OAI.CoherentK0.cls_isZero line 869
def OAI.CoherentK0.lift line 875
Source documentation
The universal property of the Grothendieck group. In particular a Chern character must be invariant under isomorphism and additive on short exact sequences before this construction can be used.
```
noncomputable def lift {A : Type w} [AddCommGroup A] (f : C → A)
    (hi : ∀ {X Y : C}, (X ≅ Y) → f X = f Y)
    (he : ∀ {S : ShortComplex C}, S.ShortExact → f S.X₂ = f S.X₁ + f S.X₃) :
    Group C →+ A :=
…
```
Mentions: OAI.CoherentK0.Group
lemma OAI.CoherentK0.lift_cls line 891

inductive OAI.CoherentK0.FilteredBy line 899

Source documentation

A finite filtration specified by short exact sequences, with a list recording its successive quotients.

inductive FilteredBy : C → List C → Prop
  | zero (X : C) (hX : IsZero X) : FilteredBy X []
  | step {S : ShortComplex C} (hS : S.ShortExact) {qs : List C}
      (h : FilteredBy S.X₁ qs) : FilteredBy S.X₂ (S.X₃ :: qs)

lemma OAI.CoherentK0.cls_filteredBy line 904
lemma OAI.CoherentK0.map_cls_filteredBy line 914
Source documentation
The filtration theorem after any additive invariant.
```
lemma map_cls_filteredBy {A : Type w} [AddCommGroup A] (φ : Group C →+ A)
    {X : C} {qs : List C} (h : FilteredBy X qs) :
    φ (cls X) = (qs.map fun Q => φ (cls Q)).sum := by
…
```
Mentions: OAI.CoherentK0.Group, OAI.CoherentK0.FilteredBy, OAI.CoherentK0.cls