NYLL
Module

ModelOverlap.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.ModelOverlap
13 declarations indexed from sourceView source ↗

Module documentation

Pullback comparisons for coefficient-extended models

The total-space and overlap comparisons identify coefficient extension with iterated pullbacks and preserve the original projections and maps to the base.

Imports1
Imported by4

Declarations

abbrev

coefficientModelMap

L24 ↗
EtaleFundamentalGroups.coefficientModelMap
Documentation

The literal coefficient extension of a map to the base scheme.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
abbrev coefficientModelMap {A : Scheme.{u}} (a : A ⟶ S) :
    pullback φ (a ≫ f) ⟶ pullback φ f
def

modelTotalIso

L30 ↗
EtaleFundamentalGroups.modelTotalIso
Documentation

Compare the iterated total-space pullback with the literal coefficient extension.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
def modelTotalIso :
    pullback y (pullback.snd φ (u ≫ f)) ≅ pullback φ ((y ≫ u) ≫ f)
theorem

modelTotalIso_hom_fst

L36 ↗
EtaleFundamentalGroups.modelTotalIso_hom_fst
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
theorem modelTotalIso_hom_fst :
    (modelTotalIso φ f u y).hom ≫ pullback.fst φ ((y ≫ u) ≫ f) =
      pullback.snd y (pullback.snd φ (u ≫ f)) ≫ pullback.fst φ (u ≫ f)
theorem

modelTotalIso_hom_snd

L43 ↗
EtaleFundamentalGroups.modelTotalIso_hom_snd
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
theorem modelTotalIso_hom_snd :
    (modelTotalIso φ f u y).hom ≫ pullback.snd φ ((y ≫ u) ≫ f) =
      pullback.fst y (pullback.snd φ (u ≫ f))
theorem

modelTotalIso_hom_coefficientModelMap

L50 ↗
EtaleFundamentalGroups.modelTotalIso_hom_coefficientModelMap
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
theorem modelTotalIso_hom_coefficientModelMap :
    (modelTotalIso φ f u y).hom ≫ coefficientModelMap φ f (y ≫ u) =
      pullback.snd y (pullback.snd φ (u ≫ f)) ≫ coefficientModelMap φ f u
theorem

modelTotalIso_inv_coefficientModelMap

L60 ↗
EtaleFundamentalGroups.modelTotalIso_inv_coefficientModelMap
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
theorem modelTotalIso_inv_coefficientModelMap :
    (modelTotalIso φ f u y).inv ≫
        (pullback.snd y (pullback.snd φ (u ≫ f)) ≫ coefficientModelMap φ f u) =
      coefficientModelMap φ f (y ≫ u)
def

modelOverlapIso

L67 ↗
EtaleFundamentalGroups.modelOverlapIso
Documentation

Compare the literal coefficient overlap with the pullback of extended chart models.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
def modelOverlapIso :
    pullback φ ((pullback.fst (y ≫ u) v ≫ (y ≫ u)) ≫ f) ≅
      pullback (pullback.snd y (pullback.snd φ (u ≫ f)) ≫ coefficientModelMap φ f u)
        (coefficientModelMap φ f v)
theorem

modelOverlapIso_hom_first_original

L82 ↗
EtaleFundamentalGroups.modelOverlapIso_hom_first_original
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
theorem modelOverlapIso_hom_first_original :
    (modelOverlapIso φ f u v y).hom ≫
      pullback.fst (pullback.snd y (pullback.snd φ (u ≫ f)) ≫ coefficientModelMap φ f u)
        (coefficientModelMap φ f v) ≫
        pullback.fst y (pullback.snd φ (u ≫ f)) =
      pullback.snd φ ((pullback.fst (y ≫ u) v ≫ (y ≫ u)) ≫ f) ≫
        pullback.fst (y ≫ u) v
theorem

modelOverlapIso_hom_second_original

L99 ↗
EtaleFundamentalGroups.modelOverlapIso_hom_second_original
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
theorem modelOverlapIso_hom_second_original :
    (modelOverlapIso φ f u v y).hom ≫
      pullback.snd (pullback.snd y (pullback.snd φ (u ≫ f)) ≫ coefficientModelMap φ f u)
        (coefficientModelMap φ f v) ≫
        pullback.snd φ (v ≫ f) =
      pullback.snd φ ((pullback.fst (y ≫ u) v ≫ (y ≫ u)) ≫ f) ≫
        pullback.snd (y ≫ u) v
theorem

modelOverlapIso_hom_coefficient

L112 ↗
EtaleFundamentalGroups.modelOverlapIso_hom_coefficient
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
theorem modelOverlapIso_hom_coefficient :
    (modelOverlapIso φ f u v y).hom ≫
      pullback.fst (pullback.snd y (pullback.snd φ (u ≫ f)) ≫ coefficientModelMap φ f u)
        (coefficientModelMap φ f v) ≫
        pullback.snd y (pullback.snd φ (u ≫ f)) ≫ pullback.fst φ (u ≫ f) =
      pullback.fst φ ((pullback.fst (y ≫ u) v ≫ (y ≫ u)) ≫ f)
theorem

modelOverlapIso_hom_base

L127 ↗
EtaleFundamentalGroups.modelOverlapIso_hom_base
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
theorem modelOverlapIso_hom_base :
    (modelOverlapIso φ f u v y).hom ≫
      pullback.fst (pullback.snd y (pullback.snd φ (u ≫ f)) ≫ coefficientModelMap φ f u)
        (coefficientModelMap φ f v) ≫
        pullback.snd y (pullback.snd φ (u ≫ f)) ≫ coefficientModelMap φ f u =
      coefficientModelMap φ f (pullback.fst (y ≫ u) v ≫ (y ≫ u))
def

coefficientOverlapFirstMap

L141 ↗
EtaleFundamentalGroups.coefficientOverlapFirstMap
Documentation

The literal first projection of a coefficient-extended overlap.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
def coefficientOverlapFirstMap :
    pullback φ ((pullback.fst (y ≫ u) v ≫ (y ≫ u)) ≫ f) ⟶
      pullback φ ((y ≫ u) ≫ f)
theorem

modelOverlapIso_hom_first

L152 ↗
EtaleFundamentalGroups.modelOverlapIso_hom_first
Documentation

The overlap comparison identifies the first projection with literal coefficient extension of the original projection.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable {T T' S U V Y : Scheme.{u}}
variable (φ : T' ⟶ T) (f : S ⟶ T) (u : U ⟶ S) (v : V ⟶ S) (y : Y ⟶ U)
Lean source · statement
theorem modelOverlapIso_hom_first :
    (modelOverlapIso φ f u v y).hom ≫
        pullback.fst (pullback.snd y (pullback.snd φ (u ≫ f)) ≫ coefficientModelMap φ f u)
          (coefficientModelMap φ f v) ≫ (modelTotalIso φ f u y).hom =
      coefficientOverlapFirstMap φ f u v y

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.