Declarations
JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.exists_sectionsOf_linearEquiv_of_iso
Source context 21 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.actR
DocumentationThe base-changed linear action of a scalar from the chart ring on the tensor module.
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.Intertwines
DocumentationA tensor-module map intertwines the chart-ring actions through the given scalar map.
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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]
JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.linearMap_square_of_span
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.pushEquiv
DocumentationBase change a tensor-module linear equivalence along the given algebra homomorphism.
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.orient
DocumentationReorder and cancel the algebra tensor factors to identify the chart-base-change module with its tensor module over the new base.
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.fromOrient
DocumentationExpress a linear map between chart-base-change modules in the reordered tensor coordinates.
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.toOrient
DocumentationLift an intertwining map in tensor coordinates to a linear map over the base-changed chart ring.
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.fromOrientEquiv
DocumentationTransport a chart-base-change linear equivalence to the reordered tensor coordinates.
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.toOrientEquiv
DocumentationTransport an intertwining tensor-coordinate equivalence to the base-changed chart modules.
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.exists_fg_le_forall_rTensor_inclusion_eq
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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 FG
variable {k : Type*} [CommRing k] {A : Type*} [CommRing A] [Algebra k A]
{N : Type*} [AddCommGroup N] [Module k N]
JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.exists_fg_linearEquiv_of_intertwines
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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 System
variable (k : Type u) [CommRing k] (A : Type u) [CommRing A] [Algebra k A]
(Γ : Type u) [CommRing Γ] [Algebra k Γ]
variable {k A Γ}
variable {P : Type w} [AddCommGroup P] [Module Γ P] [Module k P] [IsScalarTower k Γ P]
{Q : Type w} [AddCommGroup Q] [Module Γ Q] [Module k Q] [IsScalarTower k Γ Q]
JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.conjIn
DocumentationConjugate the chart-module equivalence into tensor coordinates using the two given comparison equivalences.
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.conjOut
DocumentationConjugate an intertwining tensor-coordinate equivalence to a chart-ring linear equivalence.
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.ChartBC
DocumentationTensor comparison equivalences on both affine charts and their overlap, compatible with restriction maps and scalar actions.
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.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.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.push_rel
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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 Descent
open TwoChartCech
variable {k : Type u} [CommRing k]
JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.pushEquiv_square_of_linearMap_square
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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 Descent
open TwoChartCech
variable {k : Type u} [CommRing k]
JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.push_square_of_span_of_rTensor_eq
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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 Descent
open TwoChartCech
variable {k : Type u} [CommRing k]
JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.pushEquiv_square_of_span_of_indexed_eq
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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 Descent
open TwoChartCech
variable {k : Type u} [CommRing k]
JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.exists_pushEquiv_of_commuting_triangle
Source context 23 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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 Descent
open TwoChartCech
variable {k : Type u} [CommRing k]
JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.exists_fg_descent
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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 Descent
open TwoChartCech
variable {k : Type u} [CommRing k]
variable {A : Type u} [CommRing A] [Algebra k A] {𝒰 : Cover.{u, u} k} {S S' : Sections.{u, u, w} 𝒰}
JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.fg_restrictScalars_of_fg
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.TwoChartCech
JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf.AlgebraicGeometry.RelPicard.LFP.exists_fg_le_nonempty_iso_pullbackAlong
Source context 22 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.TwoChartCech
AlgebraicGeometry.RelPicard.isLFPInj_relPicardPresheaf
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relPicardPresheaf
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.RelPicard.RepresentsRelSubPic.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
GoodReductionJacobian.RelativePic0Designation.mk.injEq
GoodReductionJacobian.schemeHomOverComp_coe NeronModelInfra.schemeHomOverEquivOverHom_apply
GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
NeronModelInfra.schemeHomOverEquivOverHom_symm_apply
NeronModelInfra.overHomToSchemeHomOver_coe GoodReductionJacobian.RelativeGroupLaw.mk.injEq
NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
NeronModelInfra.schemeHomOverToOverHom_left
NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
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