case mp
C : Type u_2
inst✝⁴ : Category C
D : Type u_4
inst✝³ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
⊢ GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S) → ∃ T, Sieve.functorPullback G ↑T = S

case mpr
C : Type u_2
inst✝⁴ : Category C
D : Type u_4
inst✝³ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
⊢ (∃ T, Sieve.functorPullback G ↑T = S) → GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)
C : Type u_2
inst✝⁴ : Category C
D : Type u_4
inst✝³ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
⊢ GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S) ↔ ∃ T, Sieve.functorPullback G ↑T = S
constructor
case mp
C : Type u_2
inst✝⁴ : Category C
D : Type u_4
inst✝³ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)
⊢ ∃ T, Sieve.functorPullback G ↑T = S
case mp
C : Type u_2
inst✝⁴ : Category C
D : Type u_4
inst✝³ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
⊢ GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S) → ∃ T, Sieve.functorPullback G ↑T = S
intro hS
no goals
case mp
C : Type u_2
inst✝⁴ : Category C
D : Type u_4
inst✝³ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)
⊢ ∃ T, Sieve.functorPullback G ↑T = S
exact ⟨⟨_, hS⟩, (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S⟩
case mpr.intro
C : Type u_2
inst✝⁴ : Category C
D : Type u_4
inst✝³ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
⊢ GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))
case mpr
C : Type u_2
inst✝⁴ : Category C
D : Type u_4
inst✝³ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
⊢ (∃ T, Sieve.functorPullback G ↑T = S) → GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)
rintro ⟨T, rfl⟩
no goals
case mpr.intro
C : Type u_2
inst✝⁴ : Category C
D : Type u_4
inst✝³ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
⊢ GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))
exact Hld T