ExteriorChangeScalars.lean`

78 declarations, 0 contain sorry, 0 declared as axioms

Exterior powers under change of scalars.

def OAI.ActualExterior.changeScalarsEquiv line 17

Source documentation

Exterior powers commute with transport of the coefficient ring.

def changeScalarsEquiv :
    (ModuleCat.restrictScalars e.symm.toRingHom).obj (M.exteriorPower n) ≃ₗ[B]
      ((ModuleCat.restrictScalars e.symm.toRingHom).obj M).exteriorPower n where
…

lemma OAI.ActualExterior.changeScalarsEquiv_mk line 30

lemma OAI.ActualExterior.changeScalars_hom_ext line 37

Source documentation

Checking a map out of a transported exterior power on wedges suffices.

lemma changeScalars_hom_ext {P : ModuleCat.{u} B}
    {a b : (ModuleCat.restrictScalars e.symm.toRingHom).obj
      (M.exteriorPower n) ⟶ P}
    (h : ∀ z : Fin n → M, a (ModuleCat.exteriorPower.mk (M := M) z) =
…

def OAI.ActualExterior.reindex line 66
def OAI.ActualExterior.reindexObj line 74
Source documentation
A definitionally normalized presentation of restriction, with no second bundling of the module before taking its exterior power.
```
def reindexObj (M : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) :
    PresheafOfModules.{u} (S ⋙ forget₂ _ _) where
…
```
def OAI.ActualExterior.reindexComparison line 81
def OAI.ActualExterior.reindexPowerIso line 85
lemma OAI.ActualExterior.reindexObj_map_apply line 91
lemma OAI.ActualExterior.reindexPowerIso_mk line 95
def OAI.ActualExterior.directReindexIso line 101
def OAI.ActualExterior.reindexIso line 125
Source documentation
Sectionwise exterior powers commute with coefficient-ring and open-index isomorphisms, using exactly the standard pushforward functor.
```
def reindexIso (M : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) (n : ℕ) :
    (reindex F e).obj (presheaf (R := R) M n) ≅
…
```
Mentions: OAI.ActualExterior.reindex, OAI.ActualExterior.presheaf
lemma OAI.ActualExterior.reindexIso_apply_mk line 131
def OAI.ActualExterior.openRingIso line 152
def OAI.ActualExterior.openRingHom line 155
def OAI.ActualExterior.openSheafifyMap line 160
instance OAI.ActualExterior.openSheafifyMap_isIso line 165
def OAI.ActualExterior.openIso line 170
Source documentation
Sheafified exterior powers commute with open restriction without rank or freeness hypotheses.
```
def openIso (M : Y.Modules) (n : ℕ) :
    ((sheafFunctor Y n).obj M).restrict f ≅
      (sheafFunctor X n).obj (M.restrict f) :=
…
```
Mentions: OAI.ActualExterior.sheafFunctor
lemma OAI.ActualExterior.basis_map_locallyInjective line 192
lemma OAI.ActualExterior.basis_map_locallySurjective line 203
lemma OAI.ActualExterior.basis_map_W line 210
lemma OAI.ActualExterior.sheafification_map_isIso_of_basis line 220
lemma OAI.ActualExterior.sheafification_lift_isIso_of_basis line 232
abbrev OAI.AffineExterior.E line 271
abbrev OAI.AffineExterior.Ω line 272

def OAI.AffineExterior.basicEquiv line 383

Source documentation

The canonical comparison on each principal open.

def basicEquiv (r : R) :
    Γ(tilde (R := .of R) (E R M), PrimeSpectrum.basicOpen r) ≃ₗ[Γ(Spec (.of R),PrimeSpectrum.basicOpen r)]
…

Mentions: OAI.AffineExterior.E

def OAI.AffineExterior.basicMap line 397
Source documentation
Exterior comparison on sections of a principal open.
```
def basicMap (r : R) : (Ω R M).obj (.op (PrimeSpectrum.basicOpen r)) ⟶
    (tilde (R := .of R) (E R M)).val.obj (.op (PrimeSpectrum.basicOpen r)) :=
…
```
Mentions: OAI.AffineExterior.Ω, OAI.AffineExterior.E
lemma OAI.AffineExterior.basicMap_mk line 410

def OAI.AffineExterior.overBase line 423

Source documentation

Underlying R-modules of any module presheaf on Spec R.

def overBase (P : PresheafOfModules.{u} (Spec (.of R)).ringCatSheaf.obj) :
    (Opens (Spec (.of R)))ᵒᵖ ⥤ ModuleCat.{u} R :=
…

lemma OAI.AffineExterior.basicMap_natural line 470
def OAI.AffineExterior.basicAdditive line 533
def OAI.AffineExterior.additive line 544
Source documentation
Compatible principal-open comparison, extended by sheaf gluing.
```
def additive : (Ω R M).presheaf ⟶ (tilde (R := .of R) (E R M)).presheaf :=
…
```
Mentions: OAI.AffineExterior.Ω, OAI.AffineExterior.E
lemma OAI.AffineExterior.additive_basic line 549
lemma OAI.AffineExterior.additive_res line 559
lemma OAI.AffineExterior.additive_smul line 564
def OAI.AffineExterior.moduleMap line 584
Source documentation
Comparison as a morphism over the structure sheaf.
```
def moduleMap : Ω R M ⟶ (tilde (R := .of R) (E R M)).val where
…
```
Mentions: OAI.AffineExterior.Ω, OAI.AffineExterior.E
lemma OAI.AffineExterior.moduleMap_basic_bijective line 594
def OAI.AffineExterior.affineMap line 604
instance OAI.AffineExterior.affineMap_isIso line 609
def OAI.AffineExterior.affineIso line 620
Source documentation
The intrinsic exterior sheaf on an affine scheme is the tilde of its exterior module, constructed without local-rank or coherence assumptions.
```
def affineIso : (ActualExterior.sheafFunctor (Spec (.of R)) 2).obj (tilde (R := .of R) M) ≅
…
```
Mentions: OAI.ActualExterior.sheafFunctor
def OAI.SourceSymmetry.canonicalSheaf line 634
Source documentation
The intrinsic top exterior power of the cotangent sheaf over the complex field on the source Proj.
```
def canonicalSheaf : projectiveSurface.Modules :=
…
```
def OAI.SourceSymmetry.coefficientCanonicalIso line 639
Source documentation
The sheaf/module comparison on the twelve smooth coefficient charts.
```
def coefficientCanonicalIso (t : SectionIndex) (ht : Good t) :
    canonicalSheaf.restrict (coefficientIota t ht) ≅
      tilde (R := .of (coefficientChart t))
…
```
Mentions: OAI.SourceSymmetry.SectionIndex, OAI.SourceSymmetry.Good, OAI.SourceSymmetry.coefficientIota, OAI.SourceSymmetry.coefficientChart
def OAI.SourceSymmetry.coefficientCanonicalUnitIso line 652
Source documentation
The canonical line is intrinsically trivial on each coefficient chart by the explicitly computed top differential.
```
def coefficientCanonicalUnitIso (t : SectionIndex) (ht : Good t) :
    canonicalSheaf.restrict (coefficientIota t ht) ≅
      SheafOfModules.unit (Spec (.of (coefficientChart t))).ringCatSheaf :=
…
```
Mentions: OAI.SourceSymmetry.SectionIndex, OAI.SourceSymmetry.Good, OAI.SourceSymmetry.coefficientIota, OAI.SourceSymmetry.coefficientChart
lemma OAI.SourceSymmetry.coefficientIota_opensRange line 659
lemma OAI.SourceSymmetry.coefficientIota_cover line 666
def OAI.SourceSymmetry.canonicalLine line 673
Source documentation
Invertibility is proved for the real intrinsic canonical sheaf by the chart cover of the source.
```
def canonicalLine : ActualSheafTensor.LineTrivialization projectiveSurface.sheaf canonicalSheaf :=
…
```
Mentions: OAI.ActualSheafTensor.LineTrivialization, OAI.SourceSymmetry.canonicalSheaf
def OAI.FieldPrincipalOpen.overlapAlgebra line 688
theorem OAI.FieldPrincipalOpen.overlapLocalization line 689
theorem OAI.FieldPrincipalOpen.overlapTower line 690
theorem OAI.FieldPrincipalOpen.overlapFieldTower line 692
lemma OAI.FieldPrincipalOpen.smooth_away line 694
def OAI.SourceSymmetry.chartRatio line 703
Source documentation
The section ratio determining the overlap in chart s.
```
def chartRatio (s t : SectionIndex) : coefficientChart s :=
…
```
Mentions: OAI.SourceSymmetry.SectionIndex, OAI.SourceSymmetry.coefficientChart
lemma OAI.SourceSymmetry.chartRatio_ne_zero line 707
def OAI.SourceSymmetry.coefficientOverlap line 712
Source documentation
The common principal open inside the same fixed function field.
```
def coefficientOverlap (s t : SectionIndex) : Subalgebra ℂ L :=
…
```
Mentions: OAI.SourceSymmetry.SectionIndex
lemma OAI.SourceSymmetry.coefficientChart_le_overlap_left line 715
lemma OAI.SourceSymmetry.coefficientChart_le_overlap_right line 719
lemma OAI.SourceSymmetry.coefficientOverlap_eq_sup line 736
lemma OAI.SourceSymmetry.coefficientOverlap_symm line 748
instance OAI.SourceSymmetry.(instance at line 752) line 752
instance OAI.SourceSymmetry.(instance at line 754) line 754
lemma OAI.SourceSymmetry.coefficientOverlap_smooth line 756
def OAI.CanonicalCoordinates.alternatingRestrictScalars line 773
def OAI.CanonicalCoordinates.topDifferentialMap line 788
Source documentation
The canonical map on the second exterior power of differentials.
```
def topDifferentialMap : (⋀[A]^2 Ω[A⁄k]) →ₗ[A] (⋀[B]^2 Ω[B⁄k]) :=
…
```
lemma OAI.CanonicalCoordinates.topDifferentialMap_volume line 793
lemma OAI.CanonicalCoordinates.topDifferentialMap_coe line 801
lemma OAI.CanonicalCoordinates.determinantMap_natural line 826
def OAI.Subalgebra.inclusionAlgebra line 855
theorem OAI.Subalgebra.inclusionTower line 857
theorem OAI.Subalgebra.inclusionFieldTower line 862
lemma OAI.Subalgebra.isFractionRing_of_le line 868
def OAI.CanonicalCoordinates.topInclusion line 884
Source documentation
restriction along an inclusion of affine coordinate subrings.
```
def topInclusion : (⋀[A]^2 Ω[A⁄k]) →ₗ[k] (⋀[B]^2 Ω[B⁄k]) := by
…
```
lemma OAI.CanonicalCoordinates.topInclusion_natural line 889
lemma OAI.CanonicalCoordinates.topInclusion_eq_smul_of_rational line 899
def OAI.CanonicalCoordinates.invertibleTwo line 918
instance OAI.SourceSymmetry.(instance at line 942) line 942
def OAI.SourceSymmetry.canonicalOverlapRatio line 947
Source documentation
The transition value is an element of the intersection ring.
```
def canonicalOverlapRatio (s t : SectionIndex) : coefficientOverlap s t :=
…
```
Mentions: OAI.SourceSymmetry.SectionIndex, OAI.SourceSymmetry.coefficientOverlap
def OAI.SourceSymmetry.coefficientTopInclusion line 954
Source documentation
Restriction of top forms along an inclusion of coefficient rings.
```
def coefficientTopInclusion (A B : Subalgebra ℂ L) (h : A ≤ B)
    (m : ⋀[A]^2 Ω[A⁄ℂ]) : ⋀[B]^2 Ω[B⁄ℂ] := by
…
```
Mentions: OAI.SourceSymmetry.A
lemma OAI.SourceSymmetry.coefficientTopInclusion_natural line 970
Source documentation
Restriction to an included affine ring preserves the associated rational top form.
```
lemma coefficientTopInclusion_natural (A B : Subalgebra ℂ L) (h : A ≤ B)
    (m : ⋀[A]^2 Ω[A⁄ℂ]) :
    determinantMap ℂ B L (coefficientTopInclusion A B h m) = determinantMap ℂ A L m := by
…
```
Mentions: OAI.SourceSymmetry.A, OAI.SourceSymmetry.coefficientTopInclusion
lemma OAI.SourceSymmetry.canonical_overlap_transition line 987
Source documentation
Equality in the top differential module of the common open. Together with the frames, this is the canonical line's weight-five transition.
```
lemma canonical_overlap_transition (s t : SectionIndex) (hs : Good s) (ht : Good t) :
    coefficientTopInclusion (coefficientChart s) (coefficientOverlap s t)
        (coefficientChart_le_overlap_left s t) (coefficientCanonicalGenerator s hs) =
      canonicalOverlapRatio s t •
      coefficientTopInclusion (coefficientChart t) (coefficientOverlap s t)
        (coefficientChart_le_overlap_right s t) (coefficientCanonicalGenerator t ht) := by
…
```
Mentions: OAI.SourceSymmetry.SectionIndex, OAI.SourceSymmetry.Good, OAI.SourceSymmetry.coefficientTopInclusion, OAI.SourceSymmetry.coefficientChart, OAI.SourceSymmetry.coefficientOverlap, OAI.SourceSymmetry.coefficientChart_le_overlap_left, OAI.SourceSymmetry.coefficientCanonicalGenerator, OAI.SourceSymmetry.canonicalOverlapRatio, OAI.SourceSymmetry.coefficientChart_le_overlap_right