Declarations
ModuleCat.cancelBaseChange_one_tmul_rTensor
DocumentationTensor cancellation on a unit outer tensor is the coefficient map induced by g.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace ModuleCat
open scoped ChangeOfRings
ModuleCat.exists_stage_iso_of_finitePresentation_compat
DocumentationA finite-presentation isomorphism descends as an isomorphism of scalar-extension objects, with the canonical cocone comparison square proved in ModuleCat. The stage owner's actual algebra hom is identified with the prescribed cocone map.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace ModuleCat
open scoped ChangeOfRings
ModuleCat.extendScalars_one_chart_pasting
DocumentationRaising both the chart stage and the overlap stage preserves the realization of a module. All four supplied squares are equalities of actual ring maps; the old realization square is derived from them.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace ModuleCat
open scoped ChangeOfRings
ModuleCat.finitePresentation_extendScalars
DocumentationFinite presentation is preserved by scalar extension along its prescribed ring map.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace ModuleCat
open scoped ChangeOfRings
ModuleCat.exists_stage_iso_of_finitePresentation_ring_compat
DocumentationThe finite-stage isomorphism descent owner applies to a directed system of ring maps, using only the canonical lifted-integer scalar actions internally.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace ModuleCat
open scoped ChangeOfRings
ModuleCat.exists_common_stage_clutching
DocumentationA clutching isomorphism between realizations of two finitely presented stage modules descends after raising both chart stages to one common index. The module pair and its realization maps are canonical scalar extensions, and the complete clutching realization equality is proved.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace ModuleCat
open scoped ChangeOfRings
Lean source · full declarationtheorem exists_common_stage_clutching
{ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
(B0 B1 C : ι → Type u)
[∀ i, CommRing (B0 i)] [∀ i, CommRing (B1 i)] [∀ i, CommRing (C i)]
(τ0 : ∀ i j, i ≤ j → B0 i →+* B0 j)
(τ1 : ∀ i j, i ≤ j → B1 i →+* B1 j)
(τC : ∀ i j, i ≤ j → C i →+* C j)
[DirectedSystem B0 (fun i j h => τ0 i j h)]
[DirectedSystem B1 (fun i j h => τ1 i j h)]
[DirectedSystem C (fun i j h => τC i j h)]
(U0 U1 U : Type u) [CommRing U0] [CommRing U1] [CommRing U]
(g0 : ∀ i, B0 i →+* U0) (g1 : ∀ i, B1 i →+* U1) (gC : ∀ i, C i →+* U)
(hg0 : ∀ i j (h : i ≤ j), (g0 j).comp (τ0 i j h) = g0 i)
(hg1 : ∀ i j (h : i ≤ j), (g1 j).comp (τ1 i j h) = g1 i)
(hgC : ∀ i j (h : i ≤ j), (gC j).comp (τC i j h) = gC i)
(hsurj : ∀ b : U, ∃ i x, gC i x = b)
(hzero : ∀ i (x : C i), gC i x = 0 → ∃ (j : ι) (h : i ≤ j), τC i j h x = 0)
(ρ0 : ∀ i, B0 i →+* C i) (ρ1 : ∀ i, B1 i →+* C i)
(hρ0 : ∀ i j (h : i ≤ j), (τC i j h).comp (ρ0 i) = (ρ0 j).comp (τ0 i j h))
(hρ1 : ∀ i j (h : i ≤ j), (τC i j h).comp (ρ1 i) = (ρ1 j).comp (τ1 i j h))
(v0 : U0 →+* U) (v1 : U1 →+* U)
(hlim0 : ∀ i, (gC i).comp (ρ0 i) = v0.comp (g0 i))
(hlim1 : ∀ i, (gC i).comp (ρ1 i) = v1.comp (g1 i))
(i0 i1 : ι) (P0 : ModuleCat.{u} (B0 i0)) (P1 : ModuleCat.{u} (B1 i1))
[Module.FinitePresentation (B0 i0) P0] [Module.FinitePresentation (B1 i1) P1]
(σlim : (extendScalars v0).obj ((extendScalars (g0 i0)).obj P0) ≅
(extendScalars v1).obj ((extendScalars (g1 i1)).obj P1)) :
∃ (j : ι) (h0 : i0 ≤ j) (h1 : i1 ≤ j),
let L0 : ModuleCat.{u} (B0 j) := (extendScalars (τ0 i0 j h0)).obj P0
let L1 : ModuleCat.{u} (B1 j) := (extendScalars (τ1 i1 j h1)).obj P1
let M0 : ModuleCat.{u} U0 := (extendScalars (g0 i0)).obj P0
let M1 : ModuleCat.{u} U1 := (extendScalars (g1 i1)).obj P1
let Q0 : ModuleCat.{u} (C j) := (extendScalars (ρ0 j)).obj L0
let Q1 : ModuleCat.{u} (C j) := (extendScalars (ρ1 j)).obj L1
∃ (E0 : (extendScalars (g0 j)).obj L0 ≅ M0)
(E1 : (extendScalars (g1 j)).obj L1 ≅ M1)
(F0 : (extendScalars (gC j)).obj Q0 ≅ (extendScalars v0).obj M0)
(F1 : (extendScalars (gC j)).obj Q1 ≅ (extendScalars v1).obj M1)
(σj : Q0 ≅ Q1),
(∀ x : L0,
F0.hom ((extendRestrictScalarsAdj (gC j)).unit.app Q0
(show Q0 from (extendRestrictScalarsAdj (ρ0 j)).unit.app L0 x)) =
(extendRestrictScalarsAdj v0).unit.app M0
(E0.hom ((extendRestrictScalarsAdj (g0 j)).unit.app L0 x))) ∧
(∀ x : L1,
F1.hom ((extendRestrictScalarsAdj (gC j)).unit.app Q1
(show Q1 from (extendRestrictScalarsAdj (ρ1 j)).unit.app L1 x)) =
(extendRestrictScalarsAdj v1).unit.app M1
(E1.hom ((extendRestrictScalarsAdj (g1 j)).unit.app L1 x))) ∧
(extendScalars (gC j)).mapIso σj ≪≫ F1 = F0 ≪≫ σlim := by
obtain ⟨i2, h02, h12⟩ := directed_of (· ≤ ·) i0 i1
let q0 : B0 i0 →+* C i2 := (ρ0 i2).comp (τ0 i0 i2 h02)
let Q0 : ModuleCat.{u} (C i2) := (extendScalars q0).obj P0
have : Module.FinitePresentation (C i2) Q0 := finitePresentation_extendScalars q0 P0
have hu0 : (gC i2).comp q0 = v0.comp (g0 i0) := by
calc
(gC i2).comp q0 = ((gC i2).comp (ρ0 i2)).comp (τ0 i0 i2 h02) := rfl
_ = (v0.comp (g0 i2)).comp (τ0 i0 i2 h02) :=
congrArg (fun t : B0 i2 →+* U => t.comp (τ0 i0 i2 h02)) (hlim0 i2)
_ = v0.comp (g0 i0) :=
congrArg (fun t : B0 i0 →+* U0 => v0.comp t) (hg0 i0 i2 h02)
let cOld0 : extendScalars (v0.comp (g0 i0)) ≅
extendScalars q0 ⋙ extendScalars (gC i2) :=
(eqToIso (congrArg (fun t : B0 i0 →+* U => extendScalars.{u, u, u} t) hu0)).symm ≪≫
extendScalarsComp q0 (gC i2)
let oldF0 : (extendScalars (gC i2)).obj Q0 ≅
(extendScalars v0).obj ((extendScalars (g0 i0)).obj P0) :=
cOld0.symm.app P0 ≪≫ (extendScalarsComp (g0 i0) v0).app P0 ≪≫
(extendScalars v0).mapIso (Iso.refl ((extendScalars (g0 i0)).obj P0))
let q1 : B1 i1 →+* C i2 := (ρ1 i2).comp (τ1 i1 i2 h12)
let Q1 : ModuleCat.{u} (C i2) := (extendScalars q1).obj P1
have : Module.FinitePresentation (C i2) Q1 := finitePresentation_extendScalars q1 P1
have hu1 : (gC i2).comp q1 = v1.comp (g1 i1) := by
calc
(gC i2).comp q1 = ((gC i2).comp (ρ1 i2)).comp (τ1 i1 i2 h12) := rfl
_ = (v1.comp (g1 i2)).comp (τ1 i1 i2 h12) :=
congrArg (fun t : B1 i2 →+* U => t.comp (τ1 i1 i2 h12)) (hlim1 i2)
_ = v1.comp (g1 i1) :=
congrArg (fun t : B1 i1 →+* U1 => v1.comp t) (hg1 i1 i2 h12)
let cOld1 : extendScalars (v1.comp (g1 i1)) ≅
extendScalars q1 ⋙ extendScalars (gC i2) :=
(eqToIso (congrArg (fun t : B1 i1 →+* U => extendScalars.{u, u, u} t) hu1)).symm ≪≫
extendScalarsComp q1 (gC i2)
let oldF1 : (extendScalars (gC i2)).obj Q1 ≅
(extendScalars v1).obj ((extendScalars (g1 i1)).obj P1) :=
cOld1.symm.app P1 ≪≫ (extendScalarsComp (g1 i1) v1).app P1 ≪≫
(extendScalars v1).mapIso (Iso.refl ((extendScalars (g1 i1)).obj P1))
let θ : (extendScalars (gC i2)).obj Q0 ≅ (extendScalars (gC i2)).obj Q1 :=
oldF0 ≪≫ σlim ≪≫ oldF1.symm
obtain ⟨j, h2j, β, hβ⟩ := exists_stage_iso_of_finitePresentation_ring_compat
C τC U gC hgC hsurj hzero i2 Q0 Q1 θ
have h0 : i0 ≤ j := le_trans h02 h2j
have h1 : i1 ≤ j := le_trans h12 h2j
let s : C i2 →+* C j := τC i2 j h2j
let cOverlap : extendScalars (gC i2) ≅ extendScalars s ⋙ extendScalars (gC j) :=
(eqToIso (congrArg (fun t : C i2 →+* U => extendScalars.{u, u, u} t)
(hgC i2 j h2j))).symm ≪≫ extendScalarsComp s (gC j)
change (extendScalars (gC j)).map β.hom ≫ cOverlap.inv.app Q1 =
cOverlap.inv.app Q0 ≫ θ.hom at hβ
let L0 : ModuleCat.{u} (B0 j) := (extendScalars (τ0 i0 j h0)).obj P0
let M0 : ModuleCat.{u} U0 := (extendScalars (g0 i0)).obj P0
let cChart0 : extendScalars (g0 i0) ≅
extendScalars (τ0 i0 j h0) ⋙ extendScalars (g0 j) :=
(eqToIso (congrArg (fun t : B0 i0 →+* U0 => extendScalars.{u, u, u} t)
(hg0 i0 j h0))).symm ≪≫ extendScalarsComp (τ0 i0 j h0) (g0 j)
let e0 : (extendScalars (g0 j)).obj L0 ≅ M0 :=
cChart0.symm.app P0 ≪≫ Iso.refl M0
let cNew0 : extendScalars (v0.comp (g0 j)) ≅
extendScalars (ρ0 j) ⋙ extendScalars (gC j) :=
(eqToIso (congrArg (fun t : B0 j →+* U => extendScalars.{u, u, u} t)
(hlim0 j))).symm ≪≫ extendScalarsComp (ρ0 j) (gC j)
let F0 : (extendScalars (gC j)).obj ((extendScalars (ρ0 j)).obj L0) ≅
(extendScalars v0).obj M0 :=
cNew0.symm.app L0 ≪≫ (extendScalarsComp (g0 j) v0).app L0 ≪≫
(extendScalars v0).mapIso e0
let L1 : ModuleCat.{u} (B1 j) := (extendScalars (τ1 i1 j h1)).obj P1
let M1 : ModuleCat.{u} U1 := (extendScalars (g1 i1)).obj P1
let cChart1 : extendScalars (g1 i1) ≅
extendScalars (τ1 i1 j h1) ⋙ extendScalars (g1 j) :=
(eqToIso (congrArg (fun t : B1 i1 →+* U1 => extendScalars.{u, u, u} t)
(hg1 i1 j h1))).symm ≪≫ extendScalarsComp (τ1 i1 j h1) (g1 j)
let e1 : (extendScalars (g1 j)).obj L1 ≅ M1 :=
cChart1.symm.app P1 ≪≫ Iso.refl M1
let cNew1 : extendScalars (v1.comp (g1 j)) ≅
extendScalars (ρ1 j) ⋙ extendScalars (gC j) :=
(eqToIso (congrArg (fun t : B1 j →+* U => extendScalars.{u, u, u} t)
(hlim1 j))).symm ≪≫ extendScalarsComp (ρ1 j) (gC j)
let F1 : (extendScalars (gC j)).obj ((extendScalars (ρ1 j)).obj L1) ≅
(extendScalars v1).obj M1 :=
cNew1.symm.app L1 ≪≫ (extendScalarsComp (g1 j) v1).app L1 ≪≫
(extendScalars v1).mapIso e1
have hd0 : (ρ0 j).comp (τ0 i0 j h0) = s.comp q0 := by
have ht : (τ0 i2 j h2j).comp (τ0 i0 i2 h02) = τ0 i0 j h0 :=
RingHom.ext fun x => DirectedSystem.map_map' τ0 h02 h2j x
calc
(ρ0 j).comp (τ0 i0 j h0) =
(ρ0 j).comp ((τ0 i2 j h2j).comp (τ0 i0 i2 h02)) :=
congrArg (fun t : B0 i0 →+* B0 j => (ρ0 j).comp t) ht.symm
_ = ((ρ0 j).comp (τ0 i2 j h2j)).comp (τ0 i0 i2 h02) := rfl
_ = ((τC i2 j h2j).comp (ρ0 i2)).comp (τ0 i0 i2 h02) :=
congrArg (fun t : B0 i2 →+* C j => t.comp (τ0 i0 i2 h02))
(hρ0 i2 j h2j).symm
_ = s.comp q0 := rfl
let cStage0 : extendScalars ((ρ0 j).comp (τ0 i0 j h0)) ≅
extendScalars q0 ⋙ extendScalars s :=
(eqToIso (congrArg (fun t : B0 i0 →+* C j => extendScalars.{u, u, u} t) hd0.symm)).symm ≪≫
extendScalarsComp q0 s
let lam0 : (extendScalars (ρ0 j)).obj L0 ≅ (extendScalars s).obj Q0 :=
(extendScalarsComp (τ0 i0 j h0) (ρ0 j)).symm.app P0 ≪≫ cStage0.app P0
have hpaste0 := extendScalars_one_chart_pasting
(τ0 i0 j h0) q0 (ρ0 j) s (g0 i0) (g0 j) (gC i2) (gC j) v0
(hg0 i0 j h0) (hgC i2 j h2j) hd0 (hlim0 j)
P0 M0 (Iso.refl M0)
change (extendScalars (gC j)).mapIso lam0 ≪≫ cOverlap.symm.app Q0 ≪≫ oldF0 = F0
at hpaste0
have hd1 : (ρ1 j).comp (τ1 i1 j h1) = s.comp q1 := by
have ht : (τ1 i2 j h2j).comp (τ1 i1 i2 h12) = τ1 i1 j h1 :=
RingHom.ext fun x => DirectedSystem.map_map' τ1 h12 h2j x
calc
(ρ1 j).comp (τ1 i1 j h1) =
(ρ1 j).comp ((τ1 i2 j h2j).comp (τ1 i1 i2 h12)) :=
congrArg (fun t : B1 i1 →+* B1 j => (ρ1 j).comp t) ht.symm
_ = ((ρ1 j).comp (τ1 i2 j h2j)).comp (τ1 i1 i2 h12) := rfl
_ = ((τC i2 j h2j).comp (ρ1 i2)).comp (τ1 i1 i2 h12) :=
congrArg (fun t : B1 i2 →+* C j => t.comp (τ1 i1 i2 h12))
(hρ1 i2 j h2j).symm
_ = s.comp q1 := rfl
let cStage1 : extendScalars ((ρ1 j).comp (τ1 i1 j h1)) ≅
extendScalars q1 ⋙ extendScalars s :=
(eqToIso (congrArg (fun t : B1 i1 →+* C j => extendScalars.{u, u, u} t) hd1.symm)).symm ≪≫
extendScalarsComp q1 s
let lam1 : (extendScalars (ρ1 j)).obj L1 ≅ (extendScalars s).obj Q1 :=
(extendScalarsComp (τ1 i1 j h1) (ρ1 j)).symm.app P1 ≪≫ cStage1.app P1
have hpaste1 := extendScalars_one_chart_pasting
(τ1 i1 j h1) q1 (ρ1 j) s (g1 i1) (g1 j) (gC i2) (gC j) v1
(hg1 i1 j h1) (hgC i2 j h2j) hd1 (hlim1 j)
P1 M1 (Iso.refl M1)
change (extendScalars (gC j)).mapIso lam1 ≪≫ cOverlap.symm.app Q1 ≪≫ oldF1 = F1
at hpaste1
let σj : (extendScalars (ρ0 j)).obj L0 ≅ (extendScalars (ρ1 j)).obj L1 :=
lam0 ≪≫ β ≪≫ lam1.symm
refine ⟨j, h0, h1, e0, e1, F0, F1, σj, ?_, ?_, ?_⟩
· intro x
exact extendScalars_realization_unit (ρ0 j) (g0 j) (gC j) v0 (hlim0 j) L0 M0 e0 x
· intro x
exact extendScalars_realization_unit (ρ1 j) (g1 j) (gC j) v1 (hlim1 j) L1 M1 e1 x
· change (extendScalars (gC j)).mapIso σj ≪≫ F1 = F0 ≪≫ σlim
have hβIso : (extendScalars (gC j)).mapIso β ≪≫ cOverlap.symm.app Q1 =
cOverlap.symm.app Q0 ≪≫ θ := by
apply CategoryTheory.Iso.ext
exact hβ
have hβRealized : (extendScalars (gC j)).mapIso β ≪≫ cOverlap.symm.app Q1 ≪≫ oldF1 =
cOverlap.symm.app Q0 ≪≫ oldF0 ≪≫ σlim := by
calc
(extendScalars (gC j)).mapIso β ≪≫ cOverlap.symm.app Q1 ≪≫ oldF1 =
((extendScalars (gC j)).mapIso β ≪≫ cOverlap.symm.app Q1) ≪≫ oldF1 :=
(Iso.trans_assoc _ _ _).symm
_ = (cOverlap.symm.app Q0 ≪≫ θ) ≪≫ oldF1 :=
congrArg (fun z => z ≪≫ oldF1) hβIso
_ = cOverlap.symm.app Q0 ≪≫ oldF0 ≪≫ σlim := by
simp only [θ, Iso.trans_assoc, Iso.symm_self_id, Iso.trans_refl]
clear_value F0 F1 oldF0 oldF1 lam0 lam1 cOverlap
calc
(extendScalars (gC j)).mapIso σj ≪≫ F1 =
(extendScalars (gC j)).mapIso lam0 ≪≫ (extendScalars (gC j)).mapIso β ≪≫
(extendScalars (gC j)).mapIso lam1.symm ≪≫ F1 := by
simp only [σj, Functor.mapIso_trans, Iso.trans_assoc]
_ = (extendScalars (gC j)).mapIso lam0 ≪≫ (extendScalars (gC j)).mapIso β ≪≫
(extendScalars (gC j)).mapIso lam1.symm ≪≫
(extendScalars (gC j)).mapIso lam1 ≪≫ cOverlap.symm.app Q1 ≪≫ oldF1 := by
rw [← hpaste1]
_ = (extendScalars (gC j)).mapIso lam0 ≪≫ (extendScalars (gC j)).mapIso β ≪≫
cOverlap.symm.app Q1 ≪≫ oldF1 := by
simp only [Functor.mapIso_symm, Iso.symm_self_id_assoc]
_ = (extendScalars (gC j)).mapIso lam0 ≪≫ cOverlap.symm.app Q0 ≪≫ oldF0 ≪≫ σlim :=
congrArg (fun z => (extendScalars (gC j)).mapIso lam0 ≪≫ z) hβRealized
_ = ((extendScalars (gC j)).mapIso lam0 ≪≫ cOverlap.symm.app Q0 ≪≫ oldF0) ≪≫ σlim := by
rw [Iso.trans_assoc, Iso.trans_assoc]
_ = F0 ≪≫ σlim := congrArg (fun z => z ≪≫ σlim) hpaste0
ModuleCat.extendScalars_square_unit_smul
DocumentationThe canonical comparison for a commuting scalar-extension square transports a chart coefficient through the restriction ring map.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace ModuleCat
open scoped ChangeOfRings
ModuleCat.exists_scalarExtension_realization
DocumentationExtend a chart realization through a supplied overlap realization. The resulting equivalence satisfies the restriction law on the canonical scalar-extension unit, using the original overlap law.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace ModuleCat
open scoped ChangeOfRings
universe w
universe w'
ModuleCat.invertible_extendScalars_of_invertible
DocumentationScalar extension along the specified ring map preserves invertibility. The categorical object uses that same map's restricted scalar action, so the existing tensor-base-change invertibility instance applies in a fixed context.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace ModuleCat
open scoped ChangeOfRings
universe w
universe w'
ModuleCat.realization_baseChange_compat
DocumentationA commuting scalar-extension diagram remains compatible with its specified realizations. The raw base-change map is interpreted with the same fixed ring-map action as the categorical scalar-extension functor.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace ModuleCat
open scoped ChangeOfRings
universe w
universe w'
ModuleCat.presented_overlap_generator
DocumentationEvaluate an overlap presentation on a chart generator, keeping both coordinate modules in their native scalar-extension carriers. The three primitive generator laws determine the realized value.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace ModuleCat
open scoped ChangeOfRings
universe w
universe w'
TensorProduct.exists_presentation_of_linearCoordinates
DocumentationExtend the actual coefficient-linear coordinates of a module and compose with its tensor presentation. The source scalar action is preserved through its supplied tower, and the elementary-tensor law is constructed together.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace TensorProduct
TensorProduct.exists_realized_presentation_of_linearCoordinates
DocumentationExtend coefficient-linear coordinates through a tensor presentation and its A-linear realization, constructing the final equivalence and its complete generator formula without rebuilding the coordinate restriction at the call site.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace TensorProduct
TensorProduct.realized_presentation_coordinate_transition
DocumentationCompose the supplied coordinate transition, tensor-presentation naturality, and realization comparison on every elementary outer tensor.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace TensorProduct
TensorProduct.scalar_compatibility_of_unit_presentation
DocumentationCompose the coordinate, presentation and realization scalar laws at the outer unit coefficient. No tensor action is reconstructed.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace TensorProduct
TensorProduct.baseChange_square_of_coordinate_generators
DocumentationA square of scalar-extended linear maps is determined by unit tensors in additive coordinates. The coefficient tensors span the coordinate module, and A-linearity then supplies every outer tensor coefficient.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace TensorProduct
TensorProduct.baseChange_square_of_presented_coordinates
DocumentationTransport a coordinate-generator square through supplied endpoint presentations and a source coordinate law. The overlap coordinate carrier requires no additional algebraic structure.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace TensorProduct
TensorProduct.baseChange_square_of_native_chart_coordinates
DocumentationProve the base-change restriction square from the actual chart and overlap coordinate presentations and their generated pure-tensor laws.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section CategoricalClutching
universe u v
open CategoryTheory TensorProduct
namespace TensorProduct
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.actR
DocumentationThe action of a chart scalar on the module after base extension.
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section ActR
variable (k : Type*) [CommRing k] {Γ : Type*} [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.actR_tmul
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section ActR
variable (k : Type*) [CommRing k] {Γ : Type*} [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.actR_one
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section ActR
variable (k : Type*) [CommRing k] {Γ : Type*} [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.actR_mul
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section ActR
variable (k : Type*) [CommRing k] {Γ : Type*} [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.actR_add
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section ActR
variable (k : Type*) [CommRing k] {Γ : Type*} [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.rTensor_actR
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section ActR
variable (k : Type*) [CommRing k] {Γ : Type*} [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.rTensor_smul'
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section ActR
variable (k : Type*) [CommRing k] {Γ : Type*} [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.tmul_eq_smul_one_tmul
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section ActR
variable (k : Type*) [CommRing k] {Γ : Type*} [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.Intertwines
DocumentationCompatibility of a linear map with the indicated actions of chart scalars.
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Intertwines
variable {k : Type*} [CommRing k] {Γ Γ' Γ'' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ']
[Algebra k Γ']
[CommRing Γ''] [Algebra k Γ'']
{A' : Type*} [CommRing A'] [Algebra k A']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module Γ'' N] [Module k N] [IsScalarTower k Γ'' N]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.Intertwines.comp
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Intertwines
variable {k : Type*} [CommRing k] {Γ Γ' Γ'' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ']
[Algebra k Γ']
[CommRing Γ''] [Algebra k Γ'']
{A' : Type*} [CommRing A'] [Algebra k A']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module Γ'' N] [Module k N] [IsScalarTower k Γ'' N]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.Intertwines.id
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Intertwines
variable {k : Type*} [CommRing k] {Γ Γ' Γ'' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ']
[Algebra k Γ']
[CommRing Γ''] [Algebra k Γ'']
{A' : Type*} [CommRing A'] [Algebra k A']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module Γ'' N] [Module k N] [IsScalarTower k Γ'' N]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.Intertwines.symm
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Intertwines
variable {k : Type*} [CommRing k] {Γ Γ' Γ'' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ']
[Algebra k Γ']
[CommRing Γ''] [Algebra k Γ'']
{A' : Type*} [CommRing A'] [Algebra k A']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module Γ'' N] [Module k N] [IsScalarTower k Γ'' N]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.Intertwines.baseChange
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Intertwines
variable {k : Type*} [CommRing k] {Γ Γ' Γ'' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ']
[Algebra k Γ']
[CommRing Γ''] [Algebra k Γ'']
{A' : Type*} [CommRing A'] [Algebra k A']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module Γ'' N] [Module k N] [IsScalarTower k Γ'' N]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.linearMap_ext_of_span
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Ext
variable {k : Type*} [CommRing k] {Γ : Type*} [CommRing Γ] [Algebra k Γ]
{A' : Type*} [CommRing A'] [Algebra k A']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{N : Type*} [AddCommGroup N] [Module A' N]
AlgebraicGeometry.RelPicard.LFP.push
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Push
variable {k : Type*} [CommRing k] {Γ Γ' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ'] [Algebra
k Γ']
{A' A'' : Type*} [CommRing A'] [Algebra k A'] [CommRing A''] [Algebra k A'']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module k N]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.push_tmul
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Push
variable {k : Type*} [CommRing k] {Γ Γ' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ'] [Algebra
k Γ']
{A' A'' : Type*} [CommRing A'] [Algebra k A'] [CommRing A''] [Algebra k A'']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module k N]
open _root_.AlgebraicGeometry.RelPicard.LFP
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.push_rTensor
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Push
variable {k : Type*} [CommRing k] {Γ Γ' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ'] [Algebra
k Γ']
{A' A'' : Type*} [CommRing A'] [Algebra k A'] [CommRing A''] [Algebra k A'']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module k N]
open _root_.AlgebraicGeometry.RelPicard.LFP
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.push_id
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Push
variable {k : Type*} [CommRing k] {Γ Γ' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ'] [Algebra
k Γ']
{A' A'' : Type*} [CommRing A'] [Algebra k A'] [CommRing A''] [Algebra k A'']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module k N]
open _root_.AlgebraicGeometry.RelPicard.LFP
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.push_comp
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Push
variable {k : Type*} [CommRing k] {Γ Γ' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ'] [Algebra
k Γ']
{A' A'' : Type*} [CommRing A'] [Algebra k A'] [CommRing A''] [Algebra k A'']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module k N]
open _root_.AlgebraicGeometry.RelPicard.LFP
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.Intertwines.push
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Push
variable {k : Type*} [CommRing k] {Γ Γ' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ'] [Algebra
k Γ']
{A' A'' : Type*} [CommRing A'] [Algebra k A'] [CommRing A''] [Algebra k A'']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module k N]
open _root_.AlgebraicGeometry.RelPicard.LFP
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.rTensor_baseChange
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Push
variable {k : Type*} [CommRing k] {Γ Γ' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ'] [Algebra
k Γ']
{A' A'' : Type*} [CommRing A'] [Algebra k A'] [CommRing A''] [Algebra k A'']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module k N]
open _root_.AlgebraicGeometry.RelPicard.LFP
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.push_square
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Push
variable {k : Type*} [CommRing k] {Γ Γ' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ'] [Algebra
k Γ']
{A' A'' : Type*} [CommRing A'] [Algebra k A'] [CommRing A''] [Algebra k A'']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module k N]
open _root_.AlgebraicGeometry.RelPicard.LFP
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.mem_span_range_of_algEquiv
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Push
variable {k : Type*} [CommRing k] {Γ Γ' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ'] [Algebra
k Γ']
{A' A'' : Type*} [CommRing A'] [Algebra k A'] [CommRing A''] [Algebra k A'']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module k N]
open _root_.AlgebraicGeometry.RelPicard.LFP
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.pushEquiv
DocumentationA tensor product equivalence extended along a homomorphism of base algebras.
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Push
variable {k : Type*} [CommRing k] {Γ Γ' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ'] [Algebra
k Γ']
{A' A'' : Type*} [CommRing A'] [Algebra k A'] [CommRing A''] [Algebra k A'']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module k N]
open _root_.AlgebraicGeometry.RelPicard.LFP
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.pushEquiv_apply
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Push
variable {k : Type*} [CommRing k] {Γ Γ' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ'] [Algebra
k Γ']
{A' A'' : Type*} [CommRing A'] [Algebra k A'] [CommRing A''] [Algebra k A'']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module k N]
open _root_.AlgebraicGeometry.RelPicard.LFP
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.pushEquiv_symm_apply
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Push
variable {k : Type*} [CommRing k] {Γ Γ' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ'] [Algebra
k Γ']
{A' A'' : Type*} [CommRing A'] [Algebra k A'] [CommRing A''] [Algebra k A'']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module k N]
open _root_.AlgebraicGeometry.RelPicard.LFP
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.coe_pushEquiv
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Push
variable {k : Type*} [CommRing k] {Γ Γ' : Type*} [CommRing Γ] [Algebra k Γ] [CommRing Γ'] [Algebra
k Γ']
{A' A'' : Type*} [CommRing A'] [Algebra k A'] [CommRing A''] [Algebra k A'']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module k Q] [IsScalarTower k Γ' Q]
{N : Type*} [AddCommGroup N] [Module k N]
open _root_.AlgebraicGeometry.RelPicard.LFP
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.orient
DocumentationThe equivalence reordering the tensor factors of a base extended module.
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.orient_tmul
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.orient_symm_tmul
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.orient_smul
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.orient_smul_left
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.orient_smul_right
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.orient_symm_smul
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.orient_symm_actR
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.orient_rTensor_map
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.fromOrient
DocumentationA linear map transported from the reordered tensor presentation.
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
variable {k Γ A' P}
variable {Q : Type*} [AddCommGroup Q] [Module Γ Q] [Module k Q] [IsScalarTower k Γ Q]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.fromOrient_apply
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
variable {k Γ A' P}
variable {Q : Type*} [AddCommGroup Q] [Module Γ Q] [Module k Q] [IsScalarTower k Γ Q]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.fromOrient_orient
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
variable {k Γ A' P}
variable {Q : Type*} [AddCommGroup Q] [Module Γ Q] [Module k Q] [IsScalarTower k Γ Q]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.intertwines_fromOrient
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
variable {k Γ A' P}
variable {Q : Type*} [AddCommGroup Q] [Module Γ Q] [Module k Q] [IsScalarTower k Γ Q]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.toOrient
DocumentationA linear map compatible with chart scalars transported to the reordered tensor presentation.
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
variable {k Γ A' P}
variable {Q : Type*} [AddCommGroup Q] [Module Γ Q] [Module k Q] [IsScalarTower k Γ Q]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.toOrient_apply
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
variable {k Γ A' P}
variable {Q : Type*} [AddCommGroup Q] [Module Γ Q] [Module k Q] [IsScalarTower k Γ Q]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.fromOrient_toOrient
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
variable {k Γ A' P}
variable {Q : Type*} [AddCommGroup Q] [Module Γ Q] [Module k Q] [IsScalarTower k Γ Q]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.toOrient_fromOrient
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
variable {k Γ A' P}
variable {Q : Type*} [AddCommGroup Q] [Module Γ Q] [Module k Q] [IsScalarTower k Γ Q]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.fromOrientEquiv
DocumentationAn equivalence transported from the reordered tensor presentation.
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
variable {k Γ A' P}
variable {Q : Type*} [AddCommGroup Q] [Module Γ Q] [Module k Q] [IsScalarTower k Γ Q]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.coe_fromOrientEquiv
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
variable {k Γ A' P}
variable {Q : Type*} [AddCommGroup Q] [Module Γ Q] [Module k Q] [IsScalarTower k Γ Q]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.fromOrientEquiv_apply
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
variable {k Γ A' P}
variable {Q : Type*} [AddCommGroup Q] [Module Γ Q] [Module k Q] [IsScalarTower k Γ Q]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.toOrientEquiv
DocumentationAn equivalence compatible with chart scalars transported to the reordered tensor presentation.
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
variable {k Γ A' P}
variable {Q : Type*} [AddCommGroup Q] [Module Γ Q] [Module k Q] [IsScalarTower k Γ Q]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.toOrientEquiv_apply
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Orient
variable (k : Type*) [CommRing k] (Γ : Type*) [CommRing Γ] [Algebra k Γ]
(A' : Type*) [CommRing A'] [Algebra k A']
(P : Type*) [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
variable {k Γ A' P}
variable {Q : Type*} [AddCommGroup Q] [Module Γ Q] [Module k Q] [IsScalarTower k Γ Q]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.smul_comm_of_tower
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section OneChart
variable {k : Type*} [CommRing k] {A' : Type*} [CommRing A'] [Algebra k A']
{Γ : Type*} [CommRing Γ] [Algebra k Γ] {Γ' : Type*} [CommRing Γ'] [Algebra A' Γ']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{P' : Type*} [AddCommGroup P'] [Module Γ P'] [Module k P'] [IsScalarTower k Γ P']
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module A' Q] [IsScalarTower A' Γ' Q]
{Q' : Type*} [AddCommGroup Q'] [Module Γ' Q'] [Module A' Q'] [IsScalarTower A' Γ' Q']
omit [Algebra k A'] in
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.apply_actR_of_semilinear
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section OneChart
variable {k : Type*} [CommRing k] {A' : Type*} [CommRing A'] [Algebra k A']
{Γ : Type*} [CommRing Γ] [Algebra k Γ] {Γ' : Type*} [CommRing Γ'] [Algebra A' Γ']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{P' : Type*} [AddCommGroup P'] [Module Γ P'] [Module k P'] [IsScalarTower k Γ P']
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module A' Q] [IsScalarTower A' Γ' Q]
{Q' : Type*} [AddCommGroup Q'] [Module Γ' Q'] [Module A' Q'] [IsScalarTower A' Γ' Q']
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.symm_apply_smul_of_semilinear
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section OneChart
variable {k : Type*} [CommRing k] {A' : Type*} [CommRing A'] [Algebra k A']
{Γ : Type*} [CommRing Γ] [Algebra k Γ] {Γ' : Type*} [CommRing Γ'] [Algebra A' Γ']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{P' : Type*} [AddCommGroup P'] [Module Γ P'] [Module k P'] [IsScalarTower k Γ P']
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module A' Q] [IsScalarTower A' Γ' Q]
{Q' : Type*} [AddCommGroup Q'] [Module Γ' Q'] [Module A' Q'] [IsScalarTower A' Γ' Q']
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.conjIn
DocumentationThe equivalence between tensor presentations induced by the two chart comparison equivalences.
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section OneChart
variable {k : Type*} [CommRing k] {A' : Type*} [CommRing A'] [Algebra k A']
{Γ : Type*} [CommRing Γ] [Algebra k Γ] {Γ' : Type*} [CommRing Γ'] [Algebra A' Γ']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{P' : Type*} [AddCommGroup P'] [Module Γ P'] [Module k P'] [IsScalarTower k Γ P']
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module A' Q] [IsScalarTower A' Γ' Q]
{Q' : Type*} [AddCommGroup Q'] [Module Γ' Q'] [Module A' Q'] [IsScalarTower A' Γ' Q']
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.conjIn_apply
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section OneChart
variable {k : Type*} [CommRing k] {A' : Type*} [CommRing A'] [Algebra k A']
{Γ : Type*} [CommRing Γ] [Algebra k Γ] {Γ' : Type*} [CommRing Γ'] [Algebra A' Γ']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{P' : Type*} [AddCommGroup P'] [Module Γ P'] [Module k P'] [IsScalarTower k Γ P']
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module A' Q] [IsScalarTower A' Γ' Q]
{Q' : Type*} [AddCommGroup Q'] [Module Γ' Q'] [Module A' Q'] [IsScalarTower A' Γ' Q']
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.intertwines_conjIn
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section OneChart
variable {k : Type*} [CommRing k] {A' : Type*} [CommRing A'] [Algebra k A']
{Γ : Type*} [CommRing Γ] [Algebra k Γ] {Γ' : Type*} [CommRing Γ'] [Algebra A' Γ']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{P' : Type*} [AddCommGroup P'] [Module Γ P'] [Module k P'] [IsScalarTower k Γ P']
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module A' Q] [IsScalarTower A' Γ' Q]
{Q' : Type*} [AddCommGroup Q'] [Module Γ' Q'] [Module A' Q'] [IsScalarTower A' Γ' Q']
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.conjOut
DocumentationThe chart scalar linear equivalence induced from a compatible equivalence of tensor presentations.
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section OneChart
variable {k : Type*} [CommRing k] {A' : Type*} [CommRing A'] [Algebra k A']
{Γ : Type*} [CommRing Γ] [Algebra k Γ] {Γ' : Type*} [CommRing Γ'] [Algebra A' Γ']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{P' : Type*} [AddCommGroup P'] [Module Γ P'] [Module k P'] [IsScalarTower k Γ P']
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module A' Q] [IsScalarTower A' Γ' Q]
{Q' : Type*} [AddCommGroup Q'] [Module Γ' Q'] [Module A' Q'] [IsScalarTower A' Γ' Q']
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.conjOut_apply
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section OneChart
variable {k : Type*} [CommRing k] {A' : Type*} [CommRing A'] [Algebra k A']
{Γ : Type*} [CommRing Γ] [Algebra k Γ] {Γ' : Type*} [CommRing Γ'] [Algebra A' Γ']
{P : Type*} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{P' : Type*} [AddCommGroup P'] [Module Γ P'] [Module k P'] [IsScalarTower k Γ P']
{Q : Type*} [AddCommGroup Q] [Module Γ' Q] [Module A' Q] [IsScalarTower A' Γ' Q]
{Q' : Type*} [AddCommGroup Q'] [Module Γ' Q'] [Module A' Q'] [IsScalarTower A' Γ' Q']
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.ChartBC
DocumentationChart section comparisons for base extension, compatible with restrictions and chart scalars.
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section TwoChart
open TwoChartCech
variable {k : Type u} [CommRing k] {A' : Type u} [CommRing A'] [Algebra k A']
{𝒰 : Cover.{u, u} k} {𝒰' : Cover.{u, u} A'}
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.ChartBC.exists_intertwines_of_chartIso
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section TwoChart
open TwoChartCech
variable {k : Type u} [CommRing k] {A' : Type u} [CommRing A'] [Algebra k A']
{𝒰 : Cover.{u, u} k} {𝒰' : Cover.{u, u} A'}
variable {φ0 : 𝒰.A0 → 𝒰'.A0} {φ1 : 𝒰.A1 → 𝒰'.A1} {φ01 : 𝒰.A01 → 𝒰'.A01}
{S S' : Sections.{u, u, w} 𝒰} {T T' : Sections.{u, u, w} 𝒰'}
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.ChartBC.exists_chartIso_of_intertwines
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section TwoChart
open TwoChartCech
variable {k : Type u} [CommRing k] {A' : Type u} [CommRing A'] [Algebra k A']
{𝒰 : Cover.{u, u} k} {𝒰' : Cover.{u, u} A'}
variable {φ0 : 𝒰.A0 → 𝒰'.A0} {φ1 : 𝒰.A1 → 𝒰'.A1} {φ01 : 𝒰.A01 → 𝒰'.A01}
{S S' : Sections.{u, u, w} 𝒰} {T T' : Sections.{u, u, w} 𝒰'}
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.exists_presentEquiv
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Present
variable (k : Type*) [CommRing k] (A' : Type*) [CommRing A'] [Algebra k A']
(S : Type*) [CommRing S] [Algebra k S] (S' : Type*) [CommRing S'] [Algebra k S'] [Algebra A' S']
[IsScalarTower k A' S']
(B : Type*) [CommRing B] [Algebra B S] [Algebra B S']
(L : Type*) [AddCommGroup L] [Module B L]
[SMulCommClass B k S] [SMulCommClass B A' S']
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.tensorPresentation_naturality
DocumentationA tensor presentation commutes with a map of its coefficient module. The evaluation map on the left coefficient need not itself be linear.
Source context 20 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.tensorPresentation_baseChange_naturality
DocumentationTensor presentations commute with the actual scalar-extension maps of an equivalence of coefficient modules. Only their pure-tensor presentation laws are required; no module comparison is assumed.
Source context 20 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.exists_presentEquivs_natural
DocumentationConstruct both coefficient-module presentations over one ring presentation, together with their scalar law and the actual base-change naturality law for the supplied coefficient equivalence.
Source context 20 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.vertex_comp
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Vertex
variable {ι : Type v} {B₀ : Type u} [CommRing B₀] {B : ι → Type u} [∀ i, CommRing (B i)] [∀ i,
Algebra B₀ (B i)]
{Bω : Type u} [CommRing Bω] [Algebra B₀ Bω] {Bω' : Type u} [CommRing Bω'] [Algebra B₀ Bω']
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.vertex_surj
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Vertex
variable {ι : Type v} {B₀ : Type u} [CommRing B₀] {B : ι → Type u} [∀ i, CommRing (B i)] [∀ i,
Algebra B₀ (B i)]
{Bω : Type u} [CommRing Bω] [Algebra B₀ Bω] {Bω' : Type u} [CommRing Bω'] [Algebra B₀ Bω']
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.vertex_zero
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Vertex
variable {ι : Type v} {B₀ : Type u} [CommRing B₀] {B : ι → Type u} [∀ i, CommRing (B i)] [∀ i,
Algebra B₀ (B i)]
{Bω : Type u} [CommRing Bω] [Algebra B₀ Bω] {Bω' : Type u} [CommRing Bω'] [Algebra B₀ Bω']
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.smulCommClass_of_algebras
Source context 20 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.one_tmul_tmul_tmul
Source context 20 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.finrank_baseChange_eq_one_of_invertible
Source context 20 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.Scheme.Hom.appLE_app_apply_of_comp_eq
Source context 16 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory Opposite
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Hom in
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.Scheme.Hom.appLE_apply_map
Source context 16 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory Opposite
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Hom in
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.Scheme.Hom.app_apply_map
Source context 16 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory Opposite
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Hom in
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.algebraOfPresent
DocumentationThe chart algebra structure transported through the tensor presentation.
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section VertexGeo
open _root_.AlgebraicGeometry.FGSubalgebra
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
(Γ : Type u) [CommRing Γ] [Algebra R Γ]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.vtxEquiv
DocumentationThe reversed tensor presentation of the chart algebra.
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section VertexGeo
open _root_.AlgebraicGeometry.FGSubalgebra
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
(Γ : Type u) [CommRing Γ] [Algebra R Γ]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.vtxHom
DocumentationThe chart algebra homomorphism from a finitely generated tensor stage to the limit.
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section VertexGeo
open _root_.AlgebraicGeometry.FGSubalgebra
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
(Γ : Type u) [CommRing Γ] [Algebra R Γ]
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.vtxHom_tmul
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section VertexGeo
open _root_.AlgebraicGeometry.FGSubalgebra
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
(Γ : Type u) [CommRing Γ] [Algebra R Γ]
variable (U : Type u) [CommRing U] [Algebra A U] (eU : A ⊗[R] Γ ≃ₐ[A] U)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.vtxHom_comp
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section VertexGeo
open _root_.AlgebraicGeometry.FGSubalgebra
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
(Γ : Type u) [CommRing Γ] [Algebra R Γ]
variable (U : Type u) [CommRing U] [Algebra A U] (eU : A ⊗[R] Γ ≃ₐ[A] U)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.vtxHom_surj
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section VertexGeo
open _root_.AlgebraicGeometry.FGSubalgebra
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
(Γ : Type u) [CommRing Γ] [Algebra R Γ]
variable (U : Type u) [CommRing U] [Algebra A U] (eU : A ⊗[R] Γ ≃ₐ[A] U)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.vtxHom_zero
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section VertexGeo
open _root_.AlgebraicGeometry.FGSubalgebra
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
(Γ : Type u) [CommRing Γ] [Algebra R Γ]
variable (U : Type u) [CommRing U] [Algebra A U] (eU : A ⊗[R] Γ ≃ₐ[A] U)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.stgHom
DocumentationThe ring homomorphism from a tensor stage to its chart presentation.
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section VertexGeo
open _root_.AlgebraicGeometry.FGSubalgebra
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
(Γ : Type u) [CommRing Γ] [Algebra R Γ]
variable (U : Type u) [CommRing U] [Algebra A U] (eU : A ⊗[R] Γ ≃ₐ[A] U)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.stgHom_tmul
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section VertexGeo
open _root_.AlgebraicGeometry.FGSubalgebra
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
(Γ : Type u) [CommRing Γ] [Algebra R Γ]
variable (U : Type u) [CommRing U] [Algebra A U] (eU : A ⊗[R] Γ ≃ₐ[A] U)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.stgHom_restriction
DocumentationCompatible stage presentations identify the chart restriction with the restriction of the tensor-stage rings.
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section VertexGeo
open _root_.AlgebraicGeometry.FGSubalgebra
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
(Γ : Type u) [CommRing Γ] [Algebra R Γ]
variable (U : Type u) [CommRing U] [Algebra A U] (eU : A ⊗[R] Γ ≃ₐ[A] U)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.vtxHom_eq_comp_stgHom
DocumentationCompatibility of two tensor presentations determines the factorization of the vertex map through the stage map. Only the two tensor-ring generators are needed, so the statement applies equally to a chart and to its overlap.
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section VertexGeo
open _root_.AlgebraicGeometry.FGSubalgebra
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
(Γ : Type u) [CommRing Γ] [Algebra R Γ]
variable (U : Type u) [CommRing U] [Algebra A U] (eU : A ⊗[R] Γ ≃ₐ[A] U)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.tensorStage_restriction_natural
DocumentationRestricting a tensor stage commutes with enlarging the finitely generated base subalgebra.
Source context 26 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section AbstractSurj
open _root_.TwoChartCech
open _root_.AlgebraicGeometry.FGSubalgebra
section NativeChartGeneratorNotation
open scoped ChangeOfRings
open _root_.ModuleCat
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.tensorStage_presentation_restriction
DocumentationA tensor presentation compatible with a chart restriction gives the corresponding commutative ring diagram from every finite stage to the limit.
Source context 26 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section AbstractSurj
open _root_.TwoChartCech
open _root_.AlgebraicGeometry.FGSubalgebra
section NativeChartGeneratorNotation
open scoped ChangeOfRings
open _root_.ModuleCat
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.exists_invertible_chart_and_overlap
DocumentationDescend an invertible chart and construct its overlap realization from its original tensor presentation and restriction law.
Source context 26 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section AbstractSurj
open _root_.TwoChartCech
open _root_.AlgebraicGeometry.FGSubalgebra
section NativeChartGeneratorNotation
open scoped ChangeOfRings
open _root_.ModuleCat
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.exists_fg_gluingData
Source context 26 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section AbstractSurj
open _root_.TwoChartCech
open _root_.AlgebraicGeometry.FGSubalgebra
section NativeChartGeneratorNotation
open scoped ChangeOfRings
open _root_.ModuleCat
Lean source · full declarationtheorem exists_fg_gluingData
(R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
(𝒰 : Cover.{u, u} R) (UA : Cover.{u, u} A) (T : Sections.{u, u, w} UA)
[Module.Invertible UA.A0 T.M0] [Module.Invertible UA.A1 T.M1]
(eU0 : A ⊗[R] 𝒰.A0 ≃ₐ[A] UA.A0) (eU1 : A ⊗[R] 𝒰.A1 ≃ₐ[A] UA.A1) (eU01 : A ⊗[R] 𝒰.A01 ≃ₐ[A]
UA.A01)
(hρU0 : ∀ (a : A) (γ : 𝒰.A0), UA.ρ0 (eU0 (a ⊗ₜ[R] γ)) = eU01 (a ⊗ₜ[R] 𝒰.ρ0 γ))
(hρU1 : ∀ (a : A) (γ : 𝒰.A1), UA.ρ1 (eU1 (a ⊗ₜ[R] γ)) = eU01 (a ⊗ₜ[R] 𝒰.ρ1 γ))
(rbc0 :
let _ : Algebra UA.A0 UA.A01 := UA.ρ0.toRingHom.toAlgebra
UA.A01 ⊗[UA.A0] T.M0 ≃ₗ[UA.A01] T.M01)
(hrbc0 :
let _ : Algebra UA.A0 UA.A01 := UA.ρ0.toRingHom.toAlgebra
∀ m, rbc0 ((1 : UA.A01) ⊗ₜ[UA.A0] m) = T.r0 m)
(rbc1 :
let _ : Algebra UA.A1 UA.A01 := UA.ρ1.toRingHom.toAlgebra
UA.A01 ⊗[UA.A1] T.M1 ≃ₗ[UA.A01] T.M01)
(hrbc1 :
let _ : Algebra UA.A1 UA.A01 := UA.ρ1.toRingHom.toAlgebra
∀ m, rbc1 ((1 : UA.A01) ⊗ₜ[UA.A1] m) = T.r1 m)
(V : ∀ D : FGSubalgebra R A, Cover.{u, u} ↥D.1)
(eV0 : ∀ D : FGSubalgebra R A, ↥D.1 ⊗[R] 𝒰.A0 ≃ₐ[↥D.1] (V D).A0)
(eV1 : ∀ D : FGSubalgebra R A, ↥D.1 ⊗[R] 𝒰.A1 ≃ₐ[↥D.1] (V D).A1)
(eV01 : ∀ D : FGSubalgebra R A, ↥D.1 ⊗[R] 𝒰.A01 ≃ₐ[↥D.1] (V D).A01)
(hρV0 : ∀ (D : FGSubalgebra R A) (d : ↥D.1) (γ : 𝒰.A0), (V D).ρ0 (eV0 D (d ⊗ₜ[R] γ)) = eV01 D
(d ⊗ₜ[R] 𝒰.ρ0 γ))
(hρV1 : ∀ (D : FGSubalgebra R A) (d : ↥D.1) (γ : 𝒰.A1), (V D).ρ1 (eV1 D (d ⊗ₜ[R] γ)) = eV01 D
(d ⊗ₜ[R] 𝒰.ρ1 γ))
(φ0 : ∀ D : FGSubalgebra R A, (V D).A0 →+* UA.A0) (φ1 : ∀ D : FGSubalgebra R A, (V D).A1 →+*
UA.A1)
(φ01 : ∀ D : FGSubalgebra R A, (V D).A01 →+* UA.A01)
(eφ0 : ∀ D : FGSubalgebra R A, A ⊗[↥D.1] (V D).A0 ≃ₐ[A] UA.A0)
(heφ0 : ∀ (D : FGSubalgebra R A) (s : (V D).A0), eφ0 D ((1 : A) ⊗ₜ[↥D.1] s) = φ0 D s)
(eφ1 : ∀ D : FGSubalgebra R A, A ⊗[↥D.1] (V D).A1 ≃ₐ[A] UA.A1)
(heφ1 : ∀ (D : FGSubalgebra R A) (s : (V D).A1), eφ1 D ((1 : A) ⊗ₜ[↥D.1] s) = φ1 D s)
(eφ01 : ∀ D : FGSubalgebra R A, A ⊗[↥D.1] (V D).A01 ≃ₐ[A] UA.A01)
(heφ01 : ∀ (D : FGSubalgebra R A) (s : (V D).A01), eφ01 D ((1 : A) ⊗ₜ[↥D.1] s) = φ01 D s)
(hφρ0 : ∀ (D : FGSubalgebra R A) (s : (V D).A0), φ01 D ((V D).ρ0 s) = UA.ρ0 (φ0 D s))
(hφρ1 : ∀ (D : FGSubalgebra R A) (s : (V D).A1), φ01 D ((V D).ρ1 s) = UA.ρ1 (φ1 D s))
(hφe0 : ∀ (D : FGSubalgebra R A) (d : ↥D.1) (γ : 𝒰.A0), φ0 D (eV0 D (d ⊗ₜ[R] γ)) = eU0 ((d :
A) ⊗ₜ[R] γ))
(hφe1 : ∀ (D : FGSubalgebra R A) (d : ↥D.1) (γ : 𝒰.A1), φ1 D (eV1 D (d ⊗ₜ[R] γ)) = eU1 ((d :
A) ⊗ₜ[R] γ))
(hφe01 : ∀ (D : FGSubalgebra R A) (d : ↥D.1) (γ : 𝒰.A01), φ01 D (eV01 D (d ⊗ₜ[R] γ)) = eU01
((d : A) ⊗ₜ[R] γ)) :
∃ (D : FGSubalgebra R A)
(P0 : Type u) (_ : AddCommGroup P0) (_ : Module (V D).A0 P0) (_ : Module.Finite (V D).A0 P0)
(_ : Module.Projective (V D).A0 P0)
(P1 : Type u) (_ : AddCommGroup P1) (_ : Module (V D).A1 P1) (_ : Module.Finite (V D).A1 P1)
(_ : Module.Projective (V D).A1 P1)
(_ : ∀ (K : Type u) [Field K] [Algebra (V D).A0 K], Module.finrank K (K ⊗[(V D).A0] P0) = 1)
(_ : ∀ (K : Type u) [Field K] [Algebra (V D).A1 K], Module.finrank K (K ⊗[(V D).A1] P1) = 1)
(σ :
let _ : Algebra (V D).A0 (V D).A01 := (V D).ρ0.toRingHom.toAlgebra
let _ : Algebra (V D).A1 (V D).A01 := (V D).ρ1.toRingHom.toAlgebra
(V D).A01 ⊗[(V D).A0] P0 ≃ₗ[(V D).A01] (V D).A01 ⊗[(V D).A1] P1),
∀ (S : Sections.{u, u, w} (V D)) (e0 : S.M0 ≃ₗ[(V D).A0] P0)
(e1 : S.M1 ≃ₗ[(V D).A1] P1)
(e01 :
let _ : Algebra (V D).A0 (V D).A01 := (V D).ρ0.toRingHom.toAlgebra
S.M01 ≃ₗ[(V D).A01] (V D).A01 ⊗[(V D).A0] P0),
(let _ : Algebra (V D).A0 (V D).A01 := (V D).ρ0.toRingHom.toAlgebra
∀ m, e01 (S.r0 m) = (1 : (V D).A01) ⊗ₜ[(V D).A0] e0 m) →
(let _ : Algebra (V D).A0 (V D).A01 := (V D).ρ0.toRingHom.toAlgebra
let _ : Algebra (V D).A1 (V D).A01 := (V D).ρ1.toRingHom.toAlgebra
∀ m, σ (e01 (S.r1 m)) = (1 : (V D).A01) ⊗ₜ[(V D).A1] e1 m) →
Nonempty (ChartBC (k := ↥D.1) (A' := A) (φ0 D) (φ1 D) (φ01 D) S T) := by
classical
have : IsDirectedOrder (FGSubalgebra R A) := ⟨IsDirected.directed⟩
let B0 : FGSubalgebra R A → Type u := tensorStage R A 𝒰.A0
let B1 : FGSubalgebra R A → Type u := tensorStage R A 𝒰.A1
let C : FGSubalgebra R A → Type u := tensorStage R A 𝒰.A01
let tau0 : ∀ i j : FGSubalgebra R A, i ≤ j → B0 i →+* B0 j :=
fun i j h => (tensorStageMap R A 𝒰.A0 i j h).toRingHom
let tau1 : ∀ i j : FGSubalgebra R A, i ≤ j → B1 i →+* B1 j :=
fun i j h => (tensorStageMap R A 𝒰.A1 i j h).toRingHom
let tauC : ∀ i j : FGSubalgebra R A, i ≤ j → C i →+* C j :=
fun i j h => (tensorStageMap R A 𝒰.A01 i j h).toRingHom
let g0 : ∀ D : FGSubalgebra R A, B0 D →+* UA.A0 := by
let : Algebra 𝒰.A0 UA.A0 := algebraOfPresent R A 𝒰.A0 UA.A0 eU0
exact fun D => (vtxHom R A 𝒰.A0 UA.A0 eU0 D).toRingHom
let g1 : ∀ D : FGSubalgebra R A, B1 D →+* UA.A1 := by
let : Algebra 𝒰.A1 UA.A1 := algebraOfPresent R A 𝒰.A1 UA.A1 eU1
exact fun D => (vtxHom R A 𝒰.A1 UA.A1 eU1 D).toRingHom
let gC : ∀ D : FGSubalgebra R A, C D →+* UA.A01 := by
let : Algebra 𝒰.A01 UA.A01 := algebraOfPresent R A 𝒰.A01 UA.A01 eU01
exact fun D => (vtxHom R A 𝒰.A01 UA.A01 eU01 D).toRingHom
let res0 : ∀ D : FGSubalgebra R A, B0 D →+* C D := fun D =>
(Algebra.TensorProduct.map 𝒰.ρ0 (AlgHom.id R ↥D.1)).toRingHom
let res1 : ∀ D : FGSubalgebra R A, B1 D →+* C D := fun D =>
(Algebra.TensorProduct.map 𝒰.ρ1 (AlgHom.id R ↥D.1)).toRingHom
have hg0 : ∀ i j (h : i ≤ j), (g0 j).comp (tau0 i j h) = g0 i := by
intro i j h
let : Algebra 𝒰.A0 UA.A0 := algebraOfPresent R A 𝒰.A0 UA.A0 eU0
exact congrArg (fun f : tensorStage R A 𝒰.A0 i →ₐ[𝒰.A0] UA.A0 => f.toRingHom)
(vtxHom_comp R A 𝒰.A0 UA.A0 eU0 i j h)
have hg1 : ∀ i j (h : i ≤ j), (g1 j).comp (tau1 i j h) = g1 i := by
intro i j h
let : Algebra 𝒰.A1 UA.A1 := algebraOfPresent R A 𝒰.A1 UA.A1 eU1
exact congrArg (fun f : tensorStage R A 𝒰.A1 i →ₐ[𝒰.A1] UA.A1 => f.toRingHom)
(vtxHom_comp R A 𝒰.A1 UA.A1 eU1 i j h)
have hgC : ∀ i j (h : i ≤ j), (gC j).comp (tauC i j h) = gC i := by
intro i j h
let : Algebra 𝒰.A01 UA.A01 := algebraOfPresent R A 𝒰.A01 UA.A01 eU01
exact congrArg (fun f : tensorStage R A 𝒰.A01 i →ₐ[𝒰.A01] UA.A01 => f.toRingHom)
(vtxHom_comp R A 𝒰.A01 UA.A01 eU01 i j h)
have hres0 : ∀ i j (h : i ≤ j),
(tauC i j h).comp (res0 i) = (res0 j).comp (tau0 i j h) := by
exact fun i j h => tensorStage_restriction_natural R A 𝒰.A0 𝒰.A01 𝒰.ρ0 i j h
have hlim0 : ∀ D, (gC D).comp (res0 D) = UA.ρ0.toRingHom.comp (g0 D) := by
exact fun D => tensorStage_presentation_restriction R A 𝒰.A0 𝒰.A01
UA.A0 UA.A01 𝒰.ρ0 eU0 eU01 UA.ρ0 hρU0 D
obtain ⟨i0, oldP0, hInv0, hFP0, oldI0Native, smallOverlap0, hSmallOverlap0⟩ :=
exists_invertible_chart_and_overlap R A 𝒰.A0 UA.A0 UA.A01 eU0
UA.ρ0.toRingHom rbc0 T.r0 hrbc0
have : Module.Invertible (tensorStage R A 𝒰.A0 i0) oldP0 := hInv0
let smallM0 : ModuleCat.{u} UA.A0 := (extendScalars (g0 i0)).obj oldP0
have : Module.FinitePresentation (B0 i0) oldP0 := hFP0
have hres1 : ∀ i j (h : i ≤ j),
(tauC i j h).comp (res1 i) = (res1 j).comp (tau1 i j h) := by
exact fun i j h => tensorStage_restriction_natural R A 𝒰.A1 𝒰.A01 𝒰.ρ1 i j h
have hlim1 : ∀ D, (gC D).comp (res1 D) = UA.ρ1.toRingHom.comp (g1 D) := by
exact fun D => tensorStage_presentation_restriction R A 𝒰.A1 𝒰.A01
UA.A1 UA.A01 𝒰.ρ1 eU1 eU01 UA.ρ1 hρU1 D
obtain ⟨i1, oldP1, hInv1, hFP1, oldI1Native, smallOverlap1, hSmallOverlap1⟩ :=
exists_invertible_chart_and_overlap R A 𝒰.A1 UA.A1 UA.A01 eU1
UA.ρ1.toRingHom rbc1 T.r1 hrbc1
have : Module.Invertible (tensorStage R A 𝒰.A1 i1) oldP1 := hInv1
let smallM1 : ModuleCat.{u} UA.A1 := (extendScalars (g1 i1)).obj oldP1
have : Module.FinitePresentation (B1 i1) oldP1 := hFP1
let sigmaLimit : (extendScalars UA.ρ0.toRingHom).obj smallM0 ≅
(extendScalars UA.ρ1.toRingHom).obj smallM1 :=
(smallOverlap0 ≪≫ₗ smallOverlap1.symm).toModuleIso
have hSigmaLimit : ∀ z : (extendScalars UA.ρ0.toRingHom).obj smallM0,
smallOverlap1 (sigmaLimit.hom z) = smallOverlap0 z :=
fun z => smallOverlap1.apply_symm_apply (smallOverlap0 z)
obtain ⟨D, h0, h1, E0, E1, F0, F1, stageIso, hF0unit, hF1unit, hreal⟩ :=
exists_common_stage_clutching
B0 B1 C tau0 tau1 tauC UA.A0 UA.A1 UA.A01 g0 g1 gC hg0 hg1 hgC
(vtxHom_surj R A 𝒰.A01 UA.A01 eU01)
(vtxHom_zero R A 𝒰.A01 UA.A01 eU01)
res0 res1 hres0 hres1 UA.ρ0.toRingHom UA.ρ1.toRingHom hlim0 hlim1
i0 i1 oldP0 oldP1 sigmaLimit
let t0 : B0 D →+* (V D).A0 := stgHom R A 𝒰.A0 D (V D).A0 (eV0 D)
let t1 : B1 D →+* (V D).A1 := stgHom R A 𝒰.A1 D (V D).A1 (eV1 D)
let tC : C D →+* (V D).A01 := stgHom R A 𝒰.A01 D (V D).A01 (eV01 D)
have hCompat0 : g0 D = (φ0 D).comp t0 :=
vtxHom_eq_comp_stgHom R A 𝒰.A0 UA.A0 eU0 D (V D).A0
(eV0 D) (φ0 D) (hφe0 D)
have hCompat1 : g1 D = (φ1 D).comp t1 :=
vtxHom_eq_comp_stgHom R A 𝒰.A1 UA.A1 eU1 D (V D).A1
(eV1 D) (φ1 D) (hφe1 D)
have hCompatC : gC D = (φ01 D).comp tC :=
vtxHom_eq_comp_stgHom R A 𝒰.A01 UA.A01 eU01 D (V D).A01
(eV01 D) (φ01 D) (hφe01 D)
let L0 : ModuleCat.{u} (B0 D) := (extendScalars (tau0 i0 D h0)).obj oldP0
let Q0 : ModuleCat.{u} (C D) := (extendScalars (res0 D)).obj L0
have : Module.Invertible (B0 D) L0 :=
invertible_extendScalars_of_invertible (tau0 i0 D h0) oldP0
obtain ⟨newI0, Xi0, Xi0Native, hXi0real, hXi0Native, hXi0gen⟩ :=
exists_algebraTensor_realization_of_maps (g0 D) (res0 D) (gC D) UA.ρ0.toRingHom
L0 smallM0 E0 F0 oldI0Native smallOverlap0 T.r0 hF0unit hSmallOverlap0
let L1 : ModuleCat.{u} (B1 D) := (extendScalars (tau1 i1 D h1)).obj oldP1
let Q1 : ModuleCat.{u} (C D) := (extendScalars (res1 D)).obj L1
have : Module.Invertible (B1 D) L1 :=
invertible_extendScalars_of_invertible (tau1 i1 D h1) oldP1
obtain ⟨newI1, Xi1, Xi1Native, hXi1real, hXi1Native, hXi1gen⟩ :=
exists_algebraTensor_realization_of_maps (g1 D) (res1 D) (gC D) UA.ρ1.toRingHom
L1 smallM1 E1 F1 oldI1Native smallOverlap1 T.r1 hF1unit hSmallOverlap1
let P0 : ModuleCat.{u} (V D).A0 := algebraTensorObj t0 L0
have hSquare0 : (V D).ρ0.toRingHom.comp t0 = tC.comp (res0 D) := by
exact stgHom_restriction R A 𝒰.A0 𝒰.A01 𝒰.ρ0 D (V D).A0 (V D).A01
(eV0 D) (eV01 D) (V D).ρ0 (hρV0 D)
let P1 : ModuleCat.{u} (V D).A1 := algebraTensorObj t1 L1
have hSquare1 : (V D).ρ1.toRingHom.comp t1 = tC.comp (res1 D) := by
exact stgHom_restriction R A 𝒰.A1 𝒰.A01 𝒰.ρ1 D (V D).A1 (V D).A01
(eV1 D) (eV01 D) (V D).ρ1 (hρV1 D)
let algB0V0 : Algebra (B0 D) (V D).A0 := t0.toAlgebra
let algB1V1 : Algebra (B1 D) (V D).A1 := t1.toAlgebra
let algB0U0 : Algebra (B0 D) UA.A0 := (g0 D).toAlgebra
let algB1U1 : Algebra (B1 D) UA.A1 := (g1 D).toAlgebra
let algV0V01 : Algebra (V D).A0 (V D).A01 := (V D).ρ0.toRingHom.toAlgebra
let algV1V01 : Algebra (V D).A1 (V D).A01 := (V D).ρ1.toRingHom.toAlgebra
let algCV01 : Algebra (C D) (V D).A01 := tC.toAlgebra
let algCU01 : Algebra (C D) UA.A01 := (gC D).toAlgebra
have : Module.Invertible (V D).A0 P0 :=
invertible_algebraTensorObj_of_invertible t0 L0
have : Module.Invertible (V D).A1 P1 :=
invertible_algebraTensorObj_of_invertible t1 L1
obtain ⟨kappa0, kappa1, sigmaV, hKappa0, hKappa1, hKappaSigma⟩ :=
exists_algebraTensor_clutching_of_commuting_squares t0 t1 (res0 D) (res1 D)
(V D).ρ0.toRingHom (V D).ρ1.toRingHom tC hSquare0 hSquare1 L0 L1 stageIso
let sigmaV' : (V D).A01 ⊗[C D] Q0 ≃ₗ[(V D).A01] (V D).A01 ⊗[C D] Q1 :=
LinearEquiv.baseChange (C D) (V D).A01 Q0 Q1 stageIso.toLinearEquiv
change ∀ z : (V D).A01 ⊗[(V D).A0] P0,
kappa1 (sigmaV z) = sigmaV' (kappa0 z) at hKappaSigma
let sigmaU : UA.A01 ⊗[C D] Q0 ≃ₗ[UA.A01] UA.A01 ⊗[C D] Q1 :=
LinearEquiv.baseChange (C D) UA.A01 Q0 Q1 stageIso.toLinearEquiv
have hXiSigmaNative := realization_extendScalars_compat (gC D) Q0 Q1
((extendScalars UA.ρ0.toRingHom).obj smallM0) ((extendScalars UA.ρ1.toRingHom).obj smallM1)
stageIso F0 F1 sigmaLimit Xi0Native Xi1Native smallOverlap0 smallOverlap1
hXi0real hXi1real hSigmaLimit hreal
have hXiSigma : ∀ z : UA.A01 ⊗[C D] Q0, Xi1 (sigmaU z) = Xi0 z := by
exact algebraTensor_realization_baseChange_compat (gC D) Q0 Q1 stageIso
Xi0Native Xi1Native Xi0 Xi1 hXi0Native hXi1Native hXiSigmaNative
have : SMulCommClass (B0 D) ↥D.1 (V D).A0 := smulCommClass_of_algebras _ _ _
have : SMulCommClass (B1 D) ↥D.1 (V D).A1 := smulCommClass_of_algebras _ _ _
have : SMulCommClass (V D).A0 ↥D.1 (V D).A01 := smulCommClass_of_algebras _ _ _
have : SMulCommClass (V D).A1 ↥D.1 (V D).A01 :=
smulCommClass_of_algebras (V D).A1 ↥D.1 (V D).A01
have : SMulCommClass (B0 D) A UA.A0 := smulCommClass_of_algebras _ _ _
have : SMulCommClass (B1 D) A UA.A1 := smulCommClass_of_algebras _ _ _
have : SMulCommClass (C D) ↥D.1 (V D).A01 := smulCommClass_of_algebras _ _ _
have : SMulCommClass (C D) A UA.A01 := smulCommClass_of_algebras _ _ _
refine ⟨D, (P0 : Type u), inferInstance, inferInstance, inferInstance, inferInstance,
(P1 : Type u), inferInstance, inferInstance, inferInstance, inferInstance,
finrank_baseChange_eq_one_of_invertible (A := (V D).A0) (P0 : Type u),
finrank_baseChange_eq_one_of_invertible (A := (V D).A1) (P1 : Type u),
sigmaV, fun S e0 e1 e01 hC0 hC1 => ?_⟩
obtain ⟨Z0', hZ0', hZ0's⟩ := exists_presentEquiv ↥D.1 A (V D).A0 UA.A0 (B0 D) L0
(φ0 D) (eφ0 D) (heφ0 D) (fun b => RingHom.congr_fun hCompat0 b)
obtain ⟨Z1', hZ1', hZ1's⟩ := exists_presentEquiv ↥D.1 A (V D).A1 UA.A1 (B1 D) L1
(φ1 D) (eφ1 D) (heφ1 D) (fun b => RingHom.congr_fun hCompat1 b)
obtain ⟨present0, present1, hPresent0, hPresent0s, hPresent1, hPresentSigma⟩ :=
exists_presentEquivs_natural ↥D.1 A (V D).A01 UA.A01 (C D) Q0 Q1
(φ01 D) (eφ01 D) (heφ01 D) (fun b => RingHom.congr_fun hCompatC b) stageIso.toLinearEquiv
obtain ⟨H0, hH0, hH0s⟩ := TensorProduct.exists_realized_tensorPresentation_with_scalar
↥D.1 A UA.A0 (S := (V D).A0) (P := (V D).A0 ⊗[B0 D] L0)
(Q := UA.A0 ⊗[B0 D] L0) (N := T.M0) (φ0 D) Z0'
(show UA.A0 ⊗[B0 D] L0 ≃ₗ[UA.A0] T.M0 from newI0) (hZ0's (1 : A))
obtain ⟨Z0, hZ0, hZ0s⟩ := TensorProduct.exists_coordinate_realization_with_scalar
↥D.1 A (V D).A0 (M := S.M0) (P := (V D).A0 ⊗[B0 D] L0)
(N := T.M0) (U := UA.A0) (X := UA.A0 ⊗[B0 D] L0)
(φ0 D) (show S.M0 ≃ₗ[(V D).A0] (V D).A0 ⊗[B0 D] L0 from e0) H0 Z0' newI0 hH0 hH0s
obtain ⟨H1, hH1, hH1s⟩ := TensorProduct.exists_realized_tensorPresentation_with_scalar
↥D.1 A UA.A1 (S := (V D).A1) (P := (V D).A1 ⊗[B1 D] L1)
(Q := UA.A1 ⊗[B1 D] L1) (N := T.M1) (φ1 D) Z1'
(show UA.A1 ⊗[B1 D] L1 ≃ₗ[UA.A1] T.M1 from newI1) (hZ1's (1 : A))
obtain ⟨Z1, hZ1, hZ1s⟩ := TensorProduct.exists_coordinate_realization_with_scalar
↥D.1 A (V D).A1 (M := S.M1) (P := (V D).A1 ⊗[B1 D] L1)
(N := T.M1) (U := UA.A1) (X := UA.A1 ⊗[B1 D] L1)
(φ1 D) (show S.M1 ≃ₗ[(V D).A1] (V D).A1 ⊗[B1 D] L1 from e1) H1 Z1' newI1 hH1 hH1s
obtain ⟨H01, hH01, hH01s⟩ := TensorProduct.exists_realized_tensorPresentation_with_scalar
↥D.1 A UA.A01 (S := (V D).A01) (P := (V D).A01 ⊗[C D] Q0)
(Q := UA.A01 ⊗[C D] Q0) (N := T.M01) (φ01 D) present0
(show UA.A01 ⊗[C D] Q0 ≃ₗ[UA.A01] T.M01 from Xi0) (hPresent0s (1 : A))
obtain ⟨Z01, hZ01, hZ01s⟩ := TensorProduct.exists_coordinate_realization_with_scalar
↥D.1 A (V D).A01 (M := S.M01) (P := (V D).A01 ⊗[C D] Q0)
(N := T.M01) (U := UA.A01) (X := UA.A01 ⊗[C D] Q0)
(φ01 D) (e01 ≪≫ₗ kappa0) H01 present0 Xi0 hH01 hH01s
simp only [LinearEquiv.trans_apply] at hZ01
have htransition := TensorProduct.realized_presentation_coordinate_transition
↥D.1 A (V D).A01 (C D) Q0 Q1 stageIso.toLinearEquiv
kappa0 kappa1 sigmaV present0 present1 sigmaU Xi0 Xi1
hKappaSigma hPresentSigma hXiSigma
have hZ01_1 : ∀ (a : A) (m : S.M01),
Z01 (a ⊗ₜ[↥D.1] m) = Xi1 (present1 (a ⊗ₜ[↥D.1] kappa1 (sigmaV (e01 m)))) := by
intro a m
exact (hZ01 a m).trans (htransition a (e01 m)).symm
refine ⟨{ β0 := Z0, β1 := Z1, β01 := Z01, hr0 := ?_, hr1 := ?_, hs0 := hZ0s, hs1 := hZ1s, hs01
:= hZ01s }⟩
· exact TensorProduct.baseChange_square_of_native_chart_coordinates
(k := ↥D.1) (A := A) (B := B0 D) (J := (V D).A0)
(C := C D) (D := (V D).A01) (U := UA.A0) (V := UA.A01)
(algBJ := algB0V0) (algBU := algB0U0)
(algJD := algV0V01) (algCD := algCV01) (algCV := algCU01)
(X := L0) (Q := Q0) (M := S.M0) (N := S.M01)
(T0 := T.M0) (T1 := T.M01)
e0.toAddEquiv S.r0 T.r0 Z0 Z01 e01 kappa0 newI0 Xi0
(fun p : (V D).A0 ⊗[B0 D] L0 => Z0' ((1 : A) ⊗ₜ[↥D.1] p))
(fun q : (V D).A01 ⊗[C D] Q0 => present0 ((1 : A) ⊗ₜ[↥D.1] q))
(fun x : L0 =>
(show Q0 from (extendRestrictScalarsAdj (res0 D)).unit.app L0 x))
(V D).ρ0.toRingHom UA.ρ0.toRingHom (φ0 D) (φ01 D)
hKappa0 (hPresent0 (1 : A)) hXi0gen (hZ0' (1 : A))
(hZ01 (1 : A)) (hZ0 (1 : A)) hC0 T.r0_smul (hφρ0 D)
· exact TensorProduct.baseChange_square_of_native_chart_coordinates
(k := ↥D.1) (A := A) (B := B1 D) (J := (V D).A1)
(C := C D) (D := (V D).A01) (U := UA.A1) (V := UA.A01)
(algBJ := algB1V1) (algBU := algB1U1)
(algJD := algV1V01) (algCD := algCV01) (algCV := algCU01)
(X := L1) (Q := Q1) (M := S.M1) (N := S.M01)
(T0 := T.M1) (T1 := T.M01)
e1.toAddEquiv S.r1 T.r1 Z1 Z01 (fun n : S.M01 => sigmaV (e01 n)) kappa1 newI1 Xi1
(fun p : (V D).A1 ⊗[B1 D] L1 => Z1' ((1 : A) ⊗ₜ[↥D.1] p))
(fun q : (V D).A01 ⊗[C D] Q1 => present1 ((1 : A) ⊗ₜ[↥D.1] q))
(fun x : L1 =>
(show Q1 from (extendRestrictScalarsAdj (res1 D)).unit.app L1 x))
(V D).ρ1.toRingHom UA.ρ1.toRingHom (φ1 D) (φ01 D)
hKappa1 (hPresent1 (1 : A)) hXi1gen (hZ1' (1 : A))
(hZ01_1 (1 : A)) (hZ1 (1 : A)) hC1 T.r1_smul (hφρ1 D)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.cover_ρ0_present
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section GeoDict
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of
R))
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.cover_ρ1_present
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section GeoDict
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of
R))
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.φU0
DocumentationThe ring map from first chart sections at a finite stage to the limit chart sections.
Source context 25 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section GeoDict
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of
R))
variable (A : Type u) [CommRing A] [Algebra R A] (D : Subalgebra R A)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.φU1
DocumentationThe ring map from second chart sections at a finite stage to the limit chart sections.
Source context 25 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section GeoDict
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of
R))
variable (A : Type u) [CommRing A] [Algebra R A] (D : Subalgebra R A)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.φU01
DocumentationThe ring map from overlap sections at a finite stage to the limit overlap sections.
Source context 25 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section GeoDict
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of
R))
variable (A : Type u) [CommRing A] [Algebra R A] (D : Subalgebra R A)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.φU01_ρ0
Source context 25 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section GeoDict
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of
R))
variable (A : Type u) [CommRing A] [Algebra R A] (D : Subalgebra R A)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.φU01_ρ1
Source context 25 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section GeoDict
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of
R))
variable (A : Type u) [CommRing A] [Algebra R A] (D : Subalgebra R A)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.φU0_present
Source context 25 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section GeoDict
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of
R))
variable (A : Type u) [CommRing A] [Algebra R A] (D : Subalgebra R A)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.φU1_present
Source context 25 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section GeoDict
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of
R))
variable (A : Type u) [CommRing A] [Algebra R A] (D : Subalgebra R A)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.φU01_present
Source context 25 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section GeoDict
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of
R))
variable (A : Type u) [CommRing A] [Algebra R A] (D : Subalgebra R A)
JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard.LFP.exists_fg_nonempty_iso_pullbackAlong
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace LFP
open _root_.AlgebraicGeometry.RelPicard.LFP
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
section Final
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.TwoChartCech
open _root_.AlgebraicGeometry.FGSubalgebra
AlgebraicGeometry.RelPicard.LFP.exists_fg_nonempty_iso_pullbackAlong
Source context 13 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LFP_exists_fg_nonempty_iso_pullbackAlong
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u v w
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.TensorProduct
open LFP_exists_fg_nonempty_iso_pullbackAlong.AlgebraicGeometry.RelPicard in